change GridStructure and TileStructure

Carleson/DiscreteCarleson.lean

@@ -13,7 +13,7 @@ variable {X : Type*} {a q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ}
   [MetricSpace X]
 
 /- The constant used in Proposition 2.0.2 -/
-def C2_0_2 (a : ℝ) (q : ℝ) : ℝ := 2 ^ (440 * a ^ 3) / (q - 1) ^ 4
+def C2_0_2 (a : ℝ) (q : ℝ) : ℝ := 2 ^ (440 * a ^ 3) / (q - 1) ^ 5
 
 lemma C2_0_2_pos {a q : ℝ} : C2_0_2 a q > 0 := sorry
 

Carleson/FinitaryCarleson.lean

@@ -30,7 +30,7 @@ theorem tile_sum_operator [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D 
   sorry
 
 /- The constant used in Proposition 2.0.1 -/
-def C2_0_1 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := 2 ^ (440 * a ^ 3) / (q - 1) ^ 4
+def C2_0_1 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := 2 ^ (440 * a ^ 3) / (q - 1) ^ 5
 
 lemma C2_0_1_pos {a : ℝ} {q : ℝ≥0} : C2_0_1 a q > 0 := sorry
 

Carleson/GridStructure.lean

@@ -28,16 +28,19 @@ class GridStructure
   /-- Center functions -/
   c : 𝓓 → X
   range_s_subset : range s ⊆ Icc (-S) S
+  topCube : 𝓓
+  s_topCube : s topCube = S
+  c_topCube : c topCube = o
+  subset_topCube {i} : coe𝓓 i ⊆ coe𝓓 topCube
   𝓓_subset_biUnion {i} : ∀ k ∈ Ico (-S) (s i), coe𝓓 i ⊆ ⋃ j ∈ s ⁻¹' {k}, coe𝓓 j
   fundamental_dyadic' {i j} : s i ≤ s j → coe𝓓 i ⊆ coe𝓓 j ∨ Disjoint (coe𝓓 i) (coe𝓓 j)
-  ball_subset_biUnion : ∀ k ∈ Icc (-S) S, ball o (D ^ S) ⊆ ⋃ i ∈ s ⁻¹' {k}, coe𝓓 i
   ball_subset_𝓓 {i} : ball (c i) (D ^ s i / 4) ⊆ coe𝓓 i --2.0.10
   𝓓_subset_ball {i} : coe𝓓 i ⊆ ball (c i) (4 * D ^ s i) --2.0.10
   small_boundary {i} {t : ℝ} (ht : D ^ (- S - s i) ≤ t) :
     volume.real { x ∈ coe𝓓 i | infDist x (coe𝓓 i)ᶜ ≤ t * D ^ s i } ≤ D * t ^ κ * volume.real (coe𝓓 i)
 
-export GridStructure (range_s_subset 𝓓_subset_biUnion
-  ball_subset_biUnion ball_subset_𝓓 𝓓_subset_ball small_boundary)
+export GridStructure (range_s_subset 𝓓_subset_biUnion ball_subset_𝓓 𝓓_subset_ball small_boundary
+  topCube s_topCube c_topCube subset_topCube) -- should `X` be explicit in topCube?
 
 variable {D κ C : ℝ} {S : ℤ} {o : X}
 
@@ -47,6 +50,7 @@ variable [GridStructure X D κ S o]
 
 variable (X) in
 abbrev 𝓓 : Type u := GridStructure.𝓓 X A
+
 instance : Fintype (𝓓 X) := GridStructure.fintype_𝓓
 
 instance : SetLike (𝓓 X) X where
@@ -65,13 +69,19 @@ instance : HasSSubset (𝓓 X) := ⟨fun i j ↦ (i : Set X) ⊂ (j : Set X)⟩
 def s : 𝓓 X → ℤ := GridStructure.s
 def c : 𝓓 X → X := GridStructure.c
 
-lemma GridStructure.fundamental_dyadic {i j : 𝓓 X A} :
+lemma fundamental_dyadic {i j : 𝓓 X} :
     s i ≤ s j → (i : Set X) ⊆ (j : Set X) ∨ Disjoint (i : Set X) (j : Set X) :=
   GridStructure.fundamental_dyadic'
-export GridStructure (fundamental_dyadic)
 
 namespace 𝓓
 
+lemma le_topCube {i : 𝓓 X} : i ≤ topCube := subset_topCube
+lemma isTop_topCube : IsTop (topCube : 𝓓 X) := fun _ ↦ le_topCube
+
+lemma isMax_iff {i : 𝓓 X} : IsMax i ↔ i = topCube :=
+  isTop_topCube.isMax_iff
+
+
 /-- The set `I ↦ Iᵒ` in the blueprint. -/
 def int (i : 𝓓 X) : Set X := ball (c i) (D ^ s i / 4)
 
@@ -113,18 +123,19 @@ end GridStructure
 /- The datain a tile structure, and some basic properties.
 This is mostly separated out so that we can nicely define the notation `d_𝔭`.
 Note: compose `𝓘` with `𝓓` to get the `𝓘` of the paper. -/
-class PreTileStructure [FunctionDistances 𝕜 X]
+class PreTileStructure [FunctionDistances 𝕜 X] (Q : outParam (SimpleFunc X (Θ X)))
   (D κ : outParam ℝ) (S : outParam ℤ) (o : outParam X) extends GridStructure X D κ S o where
   protected 𝔓 : Type u
   fintype_𝔓 : Fintype 𝔓
   protected 𝓘 : 𝔓 → 𝓓
   surjective_𝓘 : Surjective 𝓘
   𝒬 : 𝔓 → Θ X
+  range_𝒬 : range 𝒬 ⊆ range Q
 
-export PreTileStructure (𝒬)
+export PreTileStructure (𝒬 range_𝒬)
 
 section
-variable {Q : X → C(X, ℂ)} [FunctionDistances 𝕜 X] [PreTileStructure D κ S o]
+variable [FunctionDistances 𝕜 X]  {Q : SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o]
 
 variable (X) in
 def 𝔓 := PreTileStructure.𝔓 𝕜 X A
@@ -138,9 +149,9 @@ end
 local notation "ball_(" D "," 𝔭 ")" => @ball (WithFunctionDistance (𝔠 𝔭) (D ^ 𝔰 𝔭 / 4)) _
 
 /-- A tile structure. -/
-class TileStructure [FunctionDistances ℝ X] (Q : outParam (X → Θ X))
+class TileStructure [FunctionDistances ℝ X] (Q : outParam (SimpleFunc X (Θ X)))
     (D κ : outParam ℝ) (S : outParam ℤ) (o : outParam X)
-    extends PreTileStructure D κ S o where
+    extends PreTileStructure Q D κ S o where
   Ω : 𝔓 → Set (Θ X)
   biUnion_Ω {i} : range Q ⊆ ⋃ p ∈ 𝓘 ⁻¹' {i}, Ω p
   disjoint_Ω {p p'} (h : p ≠ p') (hp : 𝓘 p = 𝓘 p') : Disjoint (Ω p) (Ω p')

Carleson/HardyLittlewood.lean

@@ -28,10 +28,7 @@ def maximalFunction (μ : Measure X) (𝓑 : Set (X × ℝ)) (p : ℝ) (u : X 
 
 abbrev MB (μ : Measure X) (𝓑 : Set (X × ℝ)) (u : X → E) (x : X) := maximalFunction μ 𝓑 1 u x
 
-/-! The following results probably require a doubling measure,
-and maybe some properties from `ProofData`.
-They are the statements from the blueprint.
-We probably want a more general version first. -/
+/-! Maybe we can generalize some of the hypotheses? (e.g. remove `DoublingMeasure`)? -/
 
 theorem measure_biUnion_le_lintegral {l : ℝ≥0} (hl : 0 < l)
     {u : X → ℝ≥0} (hu : AEStronglyMeasurable u μ)
@@ -41,7 +38,7 @@ theorem measure_biUnion_le_lintegral {l : ℝ≥0} (hl : 0 < l)
   sorry
 
 theorem maximalFunction_le_snorm {p : ℝ≥0}
-    (hp₁ : 1 ≤ p) {u : X → E} (hu : Memℒp u p μ) {x : X} :
+    (hp₁ : 1 ≤ p) {u : X → E} (hu : AEStronglyMeasurable u μ) {x : X} :
     maximalFunction μ 𝓑 p u x ≤ snorm u p μ := by
   sorry
 

Carleson/MetricCarleson.lean

@@ -7,7 +7,7 @@ open scoped ENNReal
 noncomputable section
 
 /- The constant used in `metric_carleson` -/
-def C1_2 (a q : ℝ) : ℝ := 2 ^ (450 * a ^ 3) / (q - 1) ^ 5
+def C1_2 (a q : ℝ) : ℝ := 2 ^ (450 * a ^ 3) / (q - 1) ^ 6
 
 lemma C1_2_pos {a q : ℝ} (hq : 1 < q) : 0 < C1_2 a q := by
   rw [C1_2]

Carleson/RealInterpolation.lean

@@ -28,9 +28,9 @@ def trunc (f : α → E) (t : ℝ) (x : α) : E := if ‖f x‖ ≤ t then f x e
 lemma aestronglyMeasurable_trunc (hf : AEStronglyMeasurable f μ) :
     AEStronglyMeasurable (trunc f t) μ := sorry
 
-/-- The `t`-truncation of `f : α →ₘ[μ] E`. -/
-def AEEqFun.trunc (f : α →ₘ[μ] E) (t : ℝ) : α →ₘ[μ] E :=
-  AEEqFun.mk (MeasureTheory.trunc f t) (aestronglyMeasurable_trunc f.aestronglyMeasurable)
+-- /-- The `t`-truncation of `f : α →ₘ[μ] E`. -/
+-- def AEEqFun.trunc (f : α →ₘ[μ] E) (t : ℝ) : α →ₘ[μ] E :=
+--   AEEqFun.mk (MeasureTheory.trunc f t) (aestronglyMeasurable_trunc f.aestronglyMeasurable)
 
 -- /-- A set of measurable functions is closed under truncation. -/
 -- class IsClosedUnderTruncation (U : Set (α →ₘ[μ] E)) : Prop where
@@ -43,8 +43,12 @@ def Sublinear (T : (α → E₁) → α' → E₂) : Prop :=
   Subadditive T ∧ ∀ (f : α → E₁) (c : ℝ), T (c • f) = c • T f
 
 /-- Marcinkiewicz real interpolation theorem. -/
--- feel free to assume that T also respect a.e.-equality.
-theorem exists_lnorm_le_of_subadditive_of_lbounded {p₀ p₁ q₀ q₁ p q : ℝ≥0∞}
+-- feel free to assume that T also respect a.e.-equality if needed.
+/- For the proof, see
+Folland, Real Analysis. Modern Techniques and Their Applications, section 6.4, theorem 6.28.
+You want to use `trunc f A` when the book uses `h_A`.
+Minkowski's inequality is `ENNReal.lintegral_Lp_add_le` -/
+theorem exists_hasStrongType_real_interpolation {p₀ p₁ q₀ q₁ p q : ℝ≥0∞}
     (hp₀ : p₀ ∈ Icc 1 q₀) (hp₁ : p₁ ∈ Icc 1 q₁) (hq : q₀ ≠ q₁)
     {C₀ C₁ t : ℝ≥0} (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)
     (hp : p⁻¹ = (1 - t) / p₀ + t / p₁) (hq : q⁻¹ = (1 - t) / q₀ + t / q₁)

Carleson/TileExistence.lean

@@ -239,15 +239,13 @@ variable [GridStructure X D κ S o] {I : 𝓓 X}
 
 
 /-- Use Zorn's lemma to define this. -/
--- Note: we might want to adapt the construction so that 𝓩 is a subset of `range Q`.
--- We only need to cover `range Q`, not all the balls of radius 1 around it. If that works, that
--- should simplify it, and might mean that we don't need Lemma 2.1.1 here.
+-- Note: 𝓩 I is a subset of finite set range Q.
 def 𝓩 (I : 𝓓 X) : Set (Θ X) := sorry
 
 /-- The constant appearing in 4.2.2. -/
 @[simp] def C𝓩 : ℝ := 3 / 10
 
-lemma 𝓩_subset : 𝓩 I ⊆ ⋃ f ∈ range Q, ball_{I} f 1 := sorry
+lemma 𝓩_subset : 𝓩 I ⊆ range Q := sorry
 lemma 𝓩_disj {f g : Θ X} (hf : f ∈ 𝓩 I) (hg : g ∈ 𝓩 I) (hfg : f ≠ g) :
     Disjoint (ball_{I} f C𝓩) (ball_{I} g C𝓩) :=
   sorry
@@ -261,13 +259,12 @@ lemma card_𝓩_le :
 /-- Note: we might only need that `𝓩` is maximal, not that it has maximal cardinality.
 So maybe we don't need this. -/
 lemma maximal_𝓩_card {𝓩' : Set (Θ X)}
-    (h𝓩' : 𝓩' ⊆ ⋃ f ∈ range Q, ball_{I} f 1)
+    (h𝓩' : 𝓩' ⊆ range Q)
     (h2𝓩' : ∀ {f g : Θ X} (hf : f ∈ 𝓩') (hg : g ∈ 𝓩') (hfg : f ≠ g),
       Disjoint (ball_{I} f C𝓩) (ball_{I} g C𝓩)) : Nat.card 𝓩' ≤ Nat.card (𝓩 I) := by
   sorry
 
-lemma maximal_𝓩 {𝓩' : Set (Θ X)}
-    (h𝓩' : 𝓩' ⊆ ⋃ f ∈ range Q, ball_{I} f 1)
+lemma maximal_𝓩 {𝓩' : Set (Θ X)} (h𝓩' : 𝓩' ⊆ range Q)
     (h2𝓩' : ∀ {f g : Θ X} (hf : f ∈ 𝓩') (hg : g ∈ 𝓩') (hfg : f ≠ g),
       Disjoint (ball_{I} f C𝓩) (ball_{I} g C𝓩)) (h𝓩 : 𝓩 I ⊆ 𝓩') : 𝓩 I = 𝓩' := by
   sorry
@@ -278,7 +275,7 @@ instance : Inhabited (𝓩 I) := sorry
 def C4_2_1 : ℝ := 7 / 10 /- 0.6 also works? -/
 
 lemma frequency_ball_cover :
-    ⋃ x : X, ball_{I} (Q x) 1 ⊆ ⋃ z ∈ 𝓩 I, ball_{I} z C4_2_1 := by
+    range Q ⊆ ⋃ z ∈ 𝓩 I, ball_{I} z C4_2_1 := by
   intro θ hθ
   have : ∃ z, z ∈ 𝓩 I ∧ ¬ Disjoint (ball_{I} z C𝓩) (ball_{I} θ C𝓩) := by
     by_contra! h
@@ -288,7 +285,7 @@ lemma frequency_ball_cover :
       simp only [C𝓩, disjoint_self, bot_eq_empty, ball_eq_empty] at this
       norm_num at this
     let 𝓩' := insert θ (𝓩 I)
-    have h𝓩' : 𝓩' ⊆ ⋃ f ∈ range Q, ball_{I} f 1 := by
+    have h𝓩' : 𝓩' ⊆ range Q := by
       rw [insert_subset_iff]
       exact ⟨by simpa using hθ, 𝓩_subset⟩
     have h2𝓩' : 𝓩'.PairwiseDisjoint (ball_{I} · C𝓩) := by
@@ -304,15 +301,19 @@ lemma frequency_ball_cover :
   rw [Set.not_disjoint_iff] at hz'
   obtain ⟨z', h₁z', h₂z'⟩ := hz'
   simp only [mem_iUnion, mem_ball, exists_prop, C𝓩, C4_2_1] at h₁z' h₂z' ⊢
-  exact ⟨z, hz, by linarith [dist_triangle_left θ z z']⟩
+  exact ⟨z, hz, by linarith
+    [dist_triangle_left (α := (WithFunctionDistance (c I) (D ^ s I / 4))) θ z z']⟩
 
 local instance tileData_existence [GridStructure X D κ S o] :
-    PreTileStructure D κ S o where
+    PreTileStructure Q D κ S o where
   𝔓 := Σ I : 𝓓 X, 𝓩 I
   fintype_𝔓 := Sigma.instFintype
   𝓘 p := p.1
   surjective_𝓘 I := ⟨⟨I, default⟩, rfl⟩
   𝒬 p := p.2
+  range_𝒬 := by
+    rintro _ ⟨p, rfl⟩
+    exact 𝓩_subset p.2.2
 
 namespace Construction
 

Carleson/ToMathlib/Misc.lean

@@ -15,8 +15,11 @@ open Function Set
 open scoped ENNReal
 attribute [gcongr] Metric.ball_subset_ball
 
+lemma IsTop.isMax_iff {α} [PartialOrder α] {i j : α} (h : IsTop i) : IsMax j ↔ j = i := by
+  simp_rw [le_antisymm_iff, h j, true_and]
+  refine ⟨(· (h j)), swap (fun _ ↦ h · |>.trans ·)⟩
+
 
--- move
 theorem Int.floor_le_iff (c : ℝ) (z : ℤ) : ⌊c⌋ ≤ z ↔ c < z + 1 := by
   rw_mod_cast [← Int.floor_le_sub_one_iff, add_sub_cancel_right]
 

Carleson/WeakType.lean

@@ -8,6 +8,7 @@ noncomputable section
 
 open NNReal ENNReal NormedSpace MeasureTheory Set Filter Topology Function
 
+
 variable {α α' 𝕜 E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m : MeasurableSpace α'}
   {p p' q : ℝ≥0∞} {c : ℝ≥0}
   {μ : Measure α} {ν : Measure α'} [NontriviallyNormedField 𝕜]
@@ -23,11 +24,14 @@ variable {α α' 𝕜 E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m : Me
   {f g : α → E} (hf : AEMeasurable f) {t s x y : ℝ≥0∞}
   {T : (α → E₁) → (α' → E₂)}
 
-#check meas_ge_le_mul_pow_snorm -- Chebyshev's inequality
+-- #check meas_ge_le_mul_pow_snorm -- Chebyshev's inequality
 
 namespace MeasureTheory
 /- If we need more properties of `E`, we can add `[RCLike E]` *instead of* the above type-classes-/
-#check _root_.RCLike
+-- #check _root_.RCLike
+
+/- Proofs for this file can be found in
+Folland, Real Analysis. Modern Techniques and Their Applications, section 6.3. -/
 
 /-! # The distribution function `d_f` -/
 
@@ -53,13 +57,16 @@ lemma distribution_smul_left {c : 𝕜} (hc : c ≠ 0) :
 lemma distribution_add_le :
     distribution (f + g) (t + s) μ ≤ distribution f t μ + distribution g s μ := sorry
 
+lemma continuousWithinAt_distribution (t₀ : ℝ≥0∞) :
+    ContinuousWithinAt (distribution f · μ) (Ioi t₀) t₀ := sorry
+
 lemma _root_.ContinuousLinearMap.distribution_le {f : α → E₁} {g : α → E₂} :
     distribution (fun x ↦ L (f x) (g x)) (‖L‖₊ * t * s) μ ≤
     distribution f t μ + distribution g s μ := sorry
 
 
 /- A version of the layer-cake theorem already exists, but the need the versions below. -/
-#check MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul
+-- #check MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul
 
 /-- The layer-cake theorem, or Cavalieri's principle for functions into `ℝ≥0∞` -/
 lemma lintegral_norm_pow_eq_measure_lt {f : α → ℝ≥0∞} (hf : AEMeasurable f μ)