Skip to content

Commit

Permalink
Prove MeasureTheory.SublinearOn.maximalFunction (#107)
Browse files Browse the repository at this point in the history
- The definition of `SublinearOn` was missing the requirement `c ≥ 0`.
- The statement of `MeasureTheory.SublinearOn.maximalFunction` had a
spurious `p`; `MB` is defined with p=1, so there's no need for a general
`p`.
- The blueprint says that `𝓑` is finite, so I used that assumption even
though several theorems in the file assume `𝓑` is countable instead. I
also changed the assumption in `hasStrongType_MB`.
  • Loading branch information
js2357 authored Aug 7, 2024
1 parent b732845 commit 6ae9c49
Show file tree
Hide file tree
Showing 3 changed files with 236 additions and 13 deletions.
103 changes: 91 additions & 12 deletions Carleson/HardyLittlewood.lean
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,71 @@ M_𝓑 in the blueprint. -/
abbrev MB (μ : Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι → ℝ) (u : X → E) (x : X) :=
maximalFunction μ 𝓑 c r 1 u x

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

variable (μ) in
private def P (f : X → E) : Prop := Memℒp f ∞ μ ∨ Memℒp f 1 μ

variable (μ) in
private def P' (f : X → E) : Prop :=
AEStronglyMeasurable f μ ∧ ∀ (c : X) (r : ℝ), ∫⁻ (y : X) in ball c r, ‖f y‖₊ ∂μ < ⊤

private lemma P'_of_P {u : X → E} (hu : P μ u) : P' μ u := by
refine ⟨hu.elim Memℒp.aestronglyMeasurable Memℒp.aestronglyMeasurable, fun c r ↦ ?_⟩
refine hu.elim (fun hu ↦ ?_) (fun hu ↦ ?_)
· have hfg : ∀ᵐ (x : X) ∂μ, x ∈ ball c r → ‖u x‖₊ ≤ snormEssSup u μ :=
(coe_nnnorm_ae_le_snormEssSup u μ).mono (by tauto)
apply lt_of_le_of_lt (MeasureTheory.setLIntegral_mono_ae' measurableSet_ball hfg)
rw [MeasureTheory.setLIntegral_const (ball c r) (snormEssSup u μ)]
refine ENNReal.mul_lt_top ?_ (measure_ball_ne_top c r)
exact snorm_exponent_top (f := u) ▸ hu.snorm_lt_top |>.ne
· have := hu.snorm_lt_top
simp [snorm, one_ne_zero, reduceIte, ENNReal.one_ne_top, snorm', ENNReal.one_toReal,
ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self] at this
exact lt_of_le_of_lt (setLIntegral_le_lintegral _ _) this

private lemma P'.add {f : X → E} {g : X → E} (hf : P' μ f) (hg : P' μ g) : P' μ (f + g) := by
constructor
· exact AEStronglyMeasurable.add hf.1 hg.1
· intro c r
apply lt_of_le_of_lt (lintegral_mono_nnreal fun y ↦ Pi.add_apply f g y ▸ nnnorm_add_le _ _)
simp_rw [ENNReal.coe_add, lintegral_add_left' <| aemeasurable_coe_nnreal_ennreal_iff.mpr
hf.1.aemeasurable.nnnorm.restrict]
exact ENNReal.add_lt_top.mpr ⟨hf.2 c r, hg.2 c r⟩

private lemma P'.smul {f : X → E} (hf : P' μ f) (s : ℝ) : P' μ (s • f) := by
refine ⟨AEStronglyMeasurable.const_smul hf.1 s, fun c r ↦ ?_⟩
simp_rw [Pi.smul_apply, nnnorm_smul, ENNReal.coe_mul, lintegral_const_mul' _ _ ENNReal.coe_ne_top]
exact ENNReal.mul_lt_top ENNReal.coe_ne_top (hf.2 c r).ne

-- The average that appears in the definition of `MB`
variable (μ) (c) (r) in
private def T (i : ι) (u : X → E) := (⨍⁻ (y : X) in ball (c i) (r i), ‖u y‖₊ ∂μ).toReal

private lemma T.add_le (i : ι) {f g : X → E} (hf : P' μ f) (hg : P' μ g) :
‖T μ c r i (f + g)‖ ≤ ‖T μ c r i f‖ + ‖T μ c r i g‖ := by
simp only [T, Pi.add_apply, Real.norm_eq_abs, ENNReal.abs_toReal]
rw [← ENNReal.toReal_add (laverage_lt_top (hf.2 _ _).ne).ne (laverage_lt_top (hg.2 _ _).ne).ne]
rw [ENNReal.toReal_le_toReal]
· rw [← setLaverage_add_left' hf.1.ennnorm]
exact setLaverage_mono' measurableSet_ball (fun x _ ↦ ENNNorm_add_le (f x) (g x))
· exact (laverage_lt_top ((P'.add hf hg).2 _ _).ne).ne
· exact (ENNReal.add_lt_top.2 ⟨laverage_lt_top (hf.2 _ _).ne, (laverage_lt_top (hg.2 _ _).ne)⟩).ne

private lemma T.smul (i : ι) : ∀ {f : X → E} {d : ℝ}, P' μ f → d ≥ 0
T μ c r i (d • f) = d • T μ c r i f := by
intro f d _ hd
simp_rw [T, Pi.smul_apply, smul_eq_mul]
nth_rewrite 2 [← (ENNReal.toReal_ofReal hd)]
rw [← ENNReal.toReal_mul]
congr
rw [setLaverage_const_mul' ENNReal.ofReal_ne_top]
congr
ext x
simp only [nnnorm_smul, ENNReal.coe_mul, ← Real.toNNReal_eq_nnnorm_of_nonneg hd]
congr

lemma covering_separable_space (X : Type*) [PseudoMetricSpace X] [SeparableSpace X] :
∃ 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 @@ -132,14 +197,28 @@ protected theorem HasStrongType.MB_top (h𝓑 : 𝓑.Countable) :
refine ENNReal.coe_toNNReal_le_self |>.trans ?_
apply MB_le_snormEssSup

/- Prove this by proving that
* suprema of sublinear maps are sublinear,
* the indicator of a sublinear map is sublinear
* constant maps are sublinear -/
protected theorem MeasureTheory.SublinearOn.maximalFunction {p : ℝ} (hp₁ : 1 ≤ p) :
protected theorem MeasureTheory.SublinearOn.maximalFunction (h𝓑 : 𝓑.Finite) :
SublinearOn (fun (u : X → E) (x : X) ↦ MB μ 𝓑 c r u x |>.toReal)
(fun f ↦ Memℒp f ∞ μ ∨ Memℒp f 1 μ) 1 := by
sorry
(fun f ↦ Memℒp f ∞ μ ∨ Memℒp f 1 μ) 1 := by
apply SublinearOn.antitone P'_of_P
simp only [MB, maximalFunction, ENNReal.rpow_one, inv_one]
apply SublinearOn.biSup 𝓑 _ _ P'.add (fun hf _ ↦ P'.smul hf _)
· intro i _
let B := ball (c i) (r i)
have (u : X → E) (x : X) : (B.indicator (fun _ ↦ ⨍⁻ y in B, ‖u y‖₊ ∂μ) x).toReal =
(B.indicator (fun _ ↦ (⨍⁻ y in B, ‖u y‖₊ ∂μ).toReal) x) := by
by_cases hx : x ∈ B <;> simp [hx]
simp_rw [this]
apply (SublinearOn.const (T μ c r i) (P' μ) (T.add_le i) (fun f d ↦ T.smul i)).indicator
· intro f x hf
by_cases h𝓑' : 𝓑.Nonempty; swap
· simp [not_nonempty_iff_eq_empty.mp h𝓑']
have ⟨i, _, hi⟩ := h𝓑.biSup_eq h𝓑' (fun i ↦ (ball (c i) (r i)).indicator
(fun _ ↦ ⨍⁻ y in ball (c i) (r i), ‖f y‖₊ ∂μ) x)
rw [hi]
by_cases hx : x ∈ ball (c i) (r i)
· simpa [hx] using (laverage_lt_top (hf.2 (c i) (r i)).ne).ne
· simp [hx]

/- The proof is roughly between (9.0.12)-(9.0.22). -/
variable (μ) in
Expand All @@ -154,7 +233,7 @@ irreducible_def CMB (A p : ℝ≥0) : ℝ≥0 := sorry

/- The proof is given between (9.0.12)-(9.0.34).
Use the real interpolation theorem instead of following the blueprint. -/
lemma hasStrongType_MB (h𝓑 : 𝓑.Countable) {p : ℝ≥0}
lemma hasStrongType_MB (h𝓑 : 𝓑.Finite) {p : ℝ≥0}
(hp : 1 < p) {u : X → E} (hu : AEStronglyMeasurable u μ) :
HasStrongType (fun (u : X → E) (x : X) ↦ MB μ 𝓑 c r u x |>.toReal)
p p μ μ (CMB A p) := by
Expand All @@ -165,10 +244,10 @@ lemma hasStrongType_MB (h𝓑 : 𝓑.Countable) {p : ℝ≥0}
zero_lt_one (pow_pos (A_pos μ) 2)
(p := p) (q := p) (A := 1)
(by simp [ENNReal.coe_inv h2p.ne']) (by simp [ENNReal.coe_inv h2p.ne'])
(fun f hf ↦ AEStronglyMeasurable.maximalFunction_toReal h𝓑)
(.maximalFunction hp.le)
(HasStrongType.MB_top h𝓑 |>.hasWeakType le_top)
(HasWeakType.MB_one μ h𝓑)
(fun f hf ↦ AEStronglyMeasurable.maximalFunction_toReal h𝓑.countable)
(.maximalFunction h𝓑)
(HasStrongType.MB_top h𝓑.countable |>.hasWeakType le_top)
(HasWeakType.MB_one μ h𝓑.countable)
convert this using 1
sorry -- let's deal with the constant later

Expand Down
105 changes: 104 additions & 1 deletion Carleson/RealInterpolation.lean
Original file line number Diff line number Diff line change
Expand Up @@ -40,9 +40,112 @@ lemma aestronglyMeasurable_trunc (hf : AEStronglyMeasurable f μ) :
def SubadditiveOn (T : (α → E₁) → α' → E₂) (P : (α → E₁) → Prop) (A : ℝ) : Prop :=
∀ (f g : α → E₁) (x : α'), P f → P g → ‖T (f + g) x‖ ≤ A * (‖T f x‖ + ‖T g x‖)

namespace SubadditiveOn

def antitone {T : (α → E₁) → α' → E₂} {P P' : (α → E₁) → Prop}
(h : ∀ {u : α → E₁}, P u → P' u) {A : ℝ} (sa : SubadditiveOn T P' A) : SubadditiveOn T P A :=
fun f g x hf hg ↦ sa f g x (h hf) (h hg)

lemma neg (P : (α → E₁) → Prop) {A : ℝ} (hA : A < 0) (h : SubadditiveOn T P A)
(f : α → E₁) (hf : P f) : T f = 0 :=
funext fun x ↦ norm_le_zero_iff.mp (by nlinarith [norm_nonneg (T (f + f) x), h f f x hf hf])

lemma zero {P : (α → E₁) → Prop} (hP : ∀ {f g : α → E₁}, P f → P g → P (f + g))
(A : ℝ) (h : ∀ u, P u → T u = 0) : SubadditiveOn T P A :=
fun f g x hf hg ↦ by simp [h f hf, h g hg, h (f + g) (hP hf hg)]

lemma biSup {ι : Type*} (𝓑 : Set ι) {T : ι → (α → E₁) → α' → ℝ≥0∞}
{P : (α → E₁) → Prop} (hT : ∀ (u : α → E₁) (x : α'), P u → ⨆ i ∈ 𝓑, T i u x ≠ ∞)
(hP : ∀ {f g : α → E₁}, P f → P g → P (f + g))
(A : ℝ) (h : ∀ i ∈ 𝓑, SubadditiveOn (fun u x ↦ (T i u x).toReal) P A) :
SubadditiveOn (fun u x ↦ (⨆ i ∈ 𝓑, T i u x).toReal) P A := by
have hT' : ∀ i ∈ 𝓑, ∀ (x : α') (u : α → E₁), P u → T i u x ≠ ∞ :=
fun i hi x f hf h ↦ hT f x hf <| eq_top_iff.mpr <| h ▸ le_biSup (fun i ↦ T i f x) hi
by_cases A0 : A < 0
· refine SubadditiveOn.zero hP A (fun f hf ↦ funext fun x ↦ ?_)
suffices ⨆ i ∈ 𝓑, T i f x = 0 by simp [this]
simp only [iSup_eq_zero]
intro i hi
have := (toReal_eq_zero_iff _).mp (congr_fun ((h i hi).neg P A0 f hf) x)
exact this.resolve_right (hT' i hi x f hf)
push_neg at A0
intro f g x hf hg
simp only [Real.norm_eq_abs, abs_toReal]
rw [← toReal_add (hT f x hf) (hT g x hg), ← toReal_ofReal A0, ← toReal_mul]
apply toReal_mono <| mul_ne_top ofReal_ne_top (add_ne_top.mpr ⟨hT f x hf, hT g x hg⟩)
simp only [iSup_le_iff]
intro i hi
specialize h i hi f g x hf hg
simp only [Real.norm_eq_abs, abs_toReal] at h
rw [← toReal_add (hT' i hi x f hf) (hT' i hi x g hg), ← toReal_ofReal A0, ← toReal_mul,
toReal_le_toReal (hT' i hi x (f + g) (hP hf hg)) <| mul_ne_top ofReal_ne_top <|
add_ne_top.mpr ⟨hT' i hi x f hf, hT' i hi x g hg⟩] at h
apply h.trans
gcongr <;> apply le_biSup _ hi

lemma indicator {T : (α → E₁) → α' → E₂} {P : (α → E₁) → Prop} {A : ℝ}
(sa : SubadditiveOn T P A) (S : Set α') :
SubadditiveOn (fun u x ↦ (S.indicator (fun y ↦ T u y) x)) P A := by
intro f g x hf hg
by_cases hx : x ∈ S <;> simp [hx, sa f g x hf hg]

-- If `T` is constant in the second argument (but not necessarily the first) and satisfies
-- a subadditivity criterion, then `SubadditiveOn T P 1`
lemma const (t : (α → E₁) → E₂) (P : (α → E₁) → Prop)
(h_add : ∀ {f g}, P f → P g → ‖t (f + g)‖ ≤ ‖t f‖ + ‖t g‖) :
SubadditiveOn (fun u (_ : α') ↦ t u) P 1 := by
intro f g x hf hg
simpa using h_add hf hg

end SubadditiveOn

/-- The operator is sublinear on functions satisfying `P` with constant `A`. -/
def SublinearOn (T : (α → E₁) → α' → E₂) (P : (α → E₁) → Prop) (A : ℝ) : Prop :=
SubadditiveOn T P A ∧ ∀ (f : α → E₁) (c : ℝ), P f → T (c • f) = c • T f
SubadditiveOn T P A ∧ ∀ (f : α → E₁) (c : ℝ), P f → c ≥ 0 → T (c • f) = c • T f

namespace SublinearOn

lemma antitone {T : (α → E₁) → α' → E₂} {P P' : (α → E₁) → Prop}
(h : ∀ {u : α → E₁}, P u → P' u) {A : ℝ} (sl : SublinearOn T P' A) : SublinearOn T P A :=
⟨sl.1.antitone (fun hu ↦ h hu), fun u c hu hc ↦ sl.2 u c (h hu) hc⟩

lemma biSup {ι : Type*} (𝓑 : Set ι) (T : ι → (α → E₁) → α' → ℝ≥0∞)
{P : (α → E₁) → Prop} (hT : ∀ (u : α → E₁) (x : α'), P u → ⨆ i ∈ 𝓑, T i u x ≠ ∞)
(h_add : ∀ {f g : α → E₁}, P f → P g → P (f + g))
(h_smul : ∀ {f : α → E₁} {c : ℝ}, P f → c ≥ 0 → P (c • f))
{A : ℝ} (h : ∀ i ∈ 𝓑, SublinearOn (fun u x ↦ (T i u x).toReal) P A) :
SublinearOn (fun u x ↦ (⨆ i ∈ 𝓑, T i u x).toReal) P A := by
have hT' : ∀ i ∈ 𝓑, ∀ (x : α') (u : α → E₁), P u → T i u x ≠ ∞ :=
fun i hi x f hf h ↦ hT f x hf <| eq_top_iff.mpr <| h ▸ le_biSup (fun i ↦ T i f x) hi
refine ⟨SubadditiveOn.biSup 𝓑 hT h_add A (fun i hi ↦ (h i hi).1), ?_⟩
intro f c hf hc
ext x
rw [Pi.smul_apply, ← ENNReal.toReal_ofReal hc, smul_eq_mul]
simp only [← toReal_mul, ENNReal.mul_iSup]
congr 1
refine biSup_congr (fun i hi ↦ ?_)
have := congr_fun ((h i hi).2 f c hf hc) x
simp only [Pi.smul_apply, smul_eq_mul, ← toReal_ofReal_mul c (T i f x) hc] at this
rw [ENNReal.toReal_eq_toReal (hT' i hi x (c • f) (h_smul hf hc))
(mul_lt_top ofReal_ne_top (hT' i hi x f hf)).ne] at this
rwa [toReal_ofReal hc]

lemma indicator {T : (α → E₁) → α' → E₂} {P : (α → E₁) → Prop} {A : ℝ} (S : Set α')
(sl : SublinearOn T P A) :
SublinearOn (fun u x ↦ (S.indicator (fun y ↦ T u y) x)) P A := by
refine ⟨SubadditiveOn.indicator sl.1 S, fun f c hf hc ↦ funext (fun x ↦ ?_)⟩
by_cases hx : x ∈ S <;> simp [hx, congr_fun (sl.2 f c hf hc) x]

-- If `T` is constant in the second argument (but not necessarily the first) and satisfies
-- certain requirements, then `SublinearOn T P 1`
lemma const (t : (α → E₁) → E₂) (P : (α → E₁) → Prop)
(h_add : ∀ {f g}, P f → P g → ‖t (f + g)‖ ≤ ‖t f‖ + ‖t g‖)
(h_smul : ∀ f {c : ℝ}, P f → c ≥ 0 → t (c • f) = c • t f) :
SublinearOn (fun u (_ : α') ↦ t u) P 1 := by
refine ⟨SubadditiveOn.const t P h_add, fun f c hf hc ↦ funext (fun x ↦ ?_)⟩
simpa using h_smul f hf hc

end SublinearOn

/-- The constant occurring in the real interpolation theorem. -/
-- todo: remove unused variables
Expand Down
41 changes: 41 additions & 0 deletions Carleson/ToMathlib/Misc.lean
Original file line number Diff line number Diff line change
Expand Up @@ -185,6 +185,27 @@ lemma lintegral_Ioc_partition {a b : ℕ} {c : ℝ} {f : ℝ → ℝ≥0∞} (hc
Nat.Ico_succ_right_eq_insert_Ico h, Finset.sum_insert Finset.right_not_mem_Ico,
add_comm (lintegral ..), ih]

/-! ## Averaging -/

-- Named for consistency with `lintegral_add_left'`
-- Maybe add laverage/setLaverage theorems for all the other lintegral_add statements?
lemma setLaverage_add_left' {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
{s : Set α} {f g : α → ENNReal} (hf : AEMeasurable f μ) :
⨍⁻ x in s, (f x + g x) ∂μ = ⨍⁻ x in s, f x ∂μ + ⨍⁻ x in s, g x ∂μ := by
simp_rw [setLaverage_eq, ENNReal.div_add_div_same, lintegral_add_left' hf.restrict]

-- Named for consistency with `setLintegral_mono'`
lemma setLaverage_mono' {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
{s : Set α} (hs : MeasurableSet s) {f g : α → ENNReal} (h : ∀ x ∈ s, f x ≤ g x) :
⨍⁻ x in s, f x ∂μ ≤ ⨍⁻ x in s, g x ∂μ := by
simp_rw [setLaverage_eq]
exact ENNReal.div_le_div_right (setLIntegral_mono' hs h) (μ s)

lemma setLaverage_const_mul' {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
{s : Set α} {f : α → ENNReal} {c : ENNReal} (hc : c ≠ ⊤) :
c * ⨍⁻ x in s, f x ∂μ = ⨍⁻ x in s, c * f x ∂μ := by
simp_rw [setLaverage_eq, ← mul_div_assoc c, lintegral_const_mul' c f hc]

end MeasureTheory

namespace MeasureTheory
Expand Down Expand Up @@ -299,3 +320,23 @@ lemma reprs_inj (hx : x ∈ hr.reprs) (hy : y ∈ hr.reprs) (h : r x y) : x = y
exact out_inj' hx hy h

end EquivalenceOn

namespace Set.Finite

lemma biSup_eq {α : Type*} {ι : Type*} [CompleteLinearOrder α] {s : Set ι}
(hs : s.Finite) (hs' : s.Nonempty) (f : ι → α) :
∃ i ∈ s, ⨆ j ∈ s, f j = f i := by
induction' s, hs using dinduction_on with a s _ _ ihs hf
· simp at hs'
rw [iSup_insert]
by_cases hs : s.Nonempty
· by_cases ha : f a ⊔ ⨆ x ∈ s, f x = f a
· use a, mem_insert a s
· obtain ⟨i, hi⟩ := ihs hs
use i, Set.mem_insert_of_mem a hi.1
rw [← hi.2, sup_eq_right]
simp only [sup_eq_left, not_le] at ha
exact ha.le
· simpa using Or.inl fun i hi ↦ (hs (nonempty_of_mem hi)).elim

end Set.Finite

0 comments on commit 6ae9c49

Please sign in to comment.