Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Task 61 #134

Merged
merged 1 commit into from
Sep 25, 2024
Merged

Task 61 #134

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
68 changes: 47 additions & 21 deletions Carleson/HardyLittlewood.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,11 @@ noncomputable section

/-! This should roughly contain the contents of chapter 9. -/

-- #check VitaliFamily
-- Note: Lemma 9.0.2 is roughly Vitali.exists_disjoint_covering_ae

section Prelude

variable (X : Type*) [PseudoMetricSpace X] [SeparableSpace X]

/-- Lemma 9.0.2 -/
lemma covering_separable_space :
∃ C : Set X, C.Countable ∧ ∀ r > 0, ⋃ c ∈ C, ball c r = univ := by
simp_rw [← Metric.dense_iff_iUnion_ball, exists_countable_dense]
Expand Down Expand Up @@ -42,6 +40,13 @@ M_𝓑 in the blueprint. -/
abbrev MB (μ : Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι → ℝ) (u : X → E) (x : X) : ℝ≥0∞ :=
maximalFunction μ 𝓑 c r 1 u x

lemma maximalFunction_eq_MB
{μ : Measure X} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} {p : ℝ} {u : X → E} {x : X} (hp : 0 ≤ p) :
maximalFunction μ 𝓑 c r p u x = (MB μ 𝓑 c r (‖u ·‖ ^ p) x) ^ p⁻¹ := by
unfold MB maximalFunction; rw [← ENNReal.rpow_mul, inv_one, one_mul]; congr! 8
rw [ENNReal.rpow_one, ← ENNReal.coe_rpow_of_nonneg _ hp, ENNReal.coe_inj,
Real.nnnorm_rpow_of_nonneg (by simp), nnnorm_norm]

-- We will replace the criterion `P` used in `MeasureTheory.SublinearOn.maximalFunction` with the
-- weaker criterion `LocallyIntegrable` that is closed under addition and scalar multiplication.

Expand Down Expand Up @@ -308,7 +313,7 @@ protected theorem HasWeakType.MB_one [BorelSpace X] (h𝓑 : 𝓑.Countable)
/-- The constant factor in the statement that `M_𝓑` has strong type. -/
irreducible_def CMB (A p : ℝ≥0) : ℝ≥0 := C_realInterpolation ⊤ 1 ⊤ 1 p 1 (A ^ 2) 1 p⁻¹

/- The proof is given between (9.0.12)-(9.0.34).
/-- Special case of equation (2.0.44). The proof is given between (9.0.12) and (9.0.34).
Use the real interpolation theorem instead of following the blueprint. -/
lemma hasStrongType_MB [BorelSpace X] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
[IsFiniteMeasureOnCompacts μ] [ProperSpace X] [Nonempty X] [μ.IsOpenPosMeasure]
Expand All @@ -326,15 +331,36 @@ lemma hasStrongType_MB [BorelSpace X] [NormedSpace ℝ E] [MeasurableSpace E] [B
(HasWeakType.MB_one μ h𝓑.countable (h𝓑.exists_image_le r).choose_spec)

/-- The constant factor in the statement that `M_{𝓑, p}` has strong type. -/
irreducible_def C2_0_6 (A p₁ p₂ : ℝ≥0) : ℝ≥0 := sorry -- todo: define in terms of `CMB`.
irreducible_def C2_0_6 (A p₁ p₂ : ℝ≥0) : ℝ≥0 := CMB A (p₂ / p₁) ^ (p₁⁻¹ : ℝ)

/- The proof is given between (9.0.34)-(9.0.36). -/
theorem hasStrongType_maximalFunction {p₁ p₂ : ℝ≥0}
(hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ < p₂)
{u : X → E} (hu : AEStronglyMeasurable u μ) :
/-- Equation (2.0.44). The proof is given between (9.0.34) and (9.0.36). -/
theorem hasStrongType_maximalFunction
[BorelSpace X] [IsFiniteMeasureOnCompacts μ] [ProperSpace X] [Nonempty X] [μ.IsOpenPosMeasure]
{p₁ p₂ : ℝ≥0} (h𝓑 : 𝓑.Finite) (hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ < p₂) :
HasStrongType (fun (u : X → E) (x : X) ↦ maximalFunction μ 𝓑 c r p₁ u x |>.toReal)
p₂ p₂ μ μ (C2_0_6 A p₁ p₂) := by
sorry
p₂ p₂ μ μ (C2_0_6 A p₁ p₂) := fun v mlpv ↦ by
dsimp only
constructor; · exact AEStronglyMeasurable.maximalFunction_toReal h𝓑.countable
have cp₁p : 0 < (p₁ : ℝ) := zero_lt_one.trans_le hp₁
have p₁n : p₁ ≠ 0 := by exact_mod_cast cp₁p.ne'
conv_lhs =>
enter [1, x]
rw [maximalFunction_eq_MB (by exact zero_le_one.trans hp₁), ← ENNReal.toReal_rpow,
← ENNReal.abs_toReal, ← Real.norm_eq_abs]
rw [eLpNorm_norm_rpow _ (by positivity), ENNReal.ofReal_inv_of_pos cp₁p,
ENNReal.ofReal_coe_nnreal, ← div_eq_mul_inv, ← ENNReal.coe_div p₁n]
calc
_ ≤ (CMB A (p₂ / p₁) * eLpNorm (fun y ↦ ‖v y‖ ^ (p₁ : ℝ)) (p₂ / p₁) μ) ^ p₁.toReal⁻¹ := by
apply ENNReal.rpow_le_rpow _ (by positivity)
convert (hasStrongType_MB h𝓑 (μ := μ) _ (fun x ↦ ‖v x‖ ^ (p₁ : ℝ)) _).2
· exact (ENNReal.coe_div p₁n).symm
· rwa [NNReal.lt_div_iff p₁n, one_mul]
· rw [ENNReal.coe_div p₁n]; exact Memℒp.norm_rpow_div mlpv p₁
_ ≤ _ := by
rw [ENNReal.mul_rpow_of_nonneg _ _ (by positivity), eLpNorm_norm_rpow _ cp₁p,
ENNReal.ofReal_coe_nnreal, ENNReal.div_mul_cancel (by positivity) (by simp),
ENNReal.rpow_rpow_inv (by positivity), ← ENNReal.coe_rpow_of_nonneg _ (by positivity),
C2_0_6]

section GMF

Expand All @@ -346,20 +372,20 @@ variable (μ) in
@[nolint unusedArguments]
def globalMaximalFunction [μ.IsDoubling A] (p : ℝ) (u : X → E) (x : X) : ℝ≥0∞ :=
A ^ 2 * maximalFunction μ ((covering_separable_space X).choose ×ˢ (univ : Set ℤ))
(fun z ↦ z.1) (fun z ↦ 2 ^ z.2) p u x
(·.1) (2 ^ ·.2) p u x

-- prove only if needed. Use `MB_le_eLpNormEssSup`
theorem globalMaximalFunction_lt_top {p : ℝ≥0} (hp₁ : 1 ≤ p)
{u : X → E} (hu : AEStronglyMeasurable u μ) (hu : IsBounded (range u)) {x : X} :
globalMaximalFunction μ p u x < ∞ := by
globalMaximalFunction μ p u x < ∞ := by
sorry

protected theorem MeasureTheory.AEStronglyMeasurable.globalMaximalFunction
[BorelSpace X] {p : ℝ} {u : X → E} : AEStronglyMeasurable (globalMaximalFunction μ p u) μ :=
aestronglyMeasurable_iff_aemeasurable.mpr <|
AEStronglyMeasurable.maximalFunction
(countable_globalMaximalFunction X) |>.aemeasurable.const_mul _
AEStronglyMeasurable.maximalFunction (countable_globalMaximalFunction X)
|>.aemeasurable.const_mul _ |>.aestronglyMeasurable

/-- Equation (2.0.45). -/
theorem laverage_le_globalMaximalFunction {u : X → E} (hu : AEStronglyMeasurable u μ)
(hu : IsBounded (range u)) {z x : X} {r : ℝ} (h : dist x z < r) :
⨍⁻ y, ‖u y‖₊ ∂μ.restrict (ball z r) ≤ globalMaximalFunction μ 1 u x := by
Expand All @@ -368,12 +394,12 @@ theorem laverage_le_globalMaximalFunction {u : X → E} (hu : AEStronglyMeasurab
/-- The constant factor in the statement that `M` has strong type. -/
def C2_0_6' (A p₁ p₂ : ℝ≥0) : ℝ≥0 := A ^ 2 * C2_0_6 A p₁ p₂

/- easy from `hasStrongType_maximalFunction`. Ideally prove separately
/-- Equation (2.0.46).

easy from `hasStrongType_maximalFunction`. Ideally prove separately
`HasStrongType.const_smul` and `HasStrongType.const_mul`. -/
theorem hasStrongType_globalMaximalFunction {p₁ p₂ : ℝ≥0}
(hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ < p₂)
{u : X → ℂ} (hu : AEStronglyMeasurable u μ) (hu : IsBounded (range u))
{z x : X} {r : ℝ} :
theorem hasStrongType_globalMaximalFunction {p₁ p₂ : ℝ≥0} (hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ < p₂)
{u : X → ℂ} (hu : AEStronglyMeasurable u μ) (h2u : IsBounded (range u)) :
HasStrongType (fun (u : X → E) (x : X) ↦ globalMaximalFunction μ p₁ u x |>.toReal)
p₂ p₂ μ μ (C2_0_6' A p₁ p₂) := by
sorry
Expand Down