Merge branch 'master' into MR-cleanup3

CONTRIBUTING.md

@@ -37,6 +37,8 @@ Below, I will try to give a translation of some notation/conventions. We use mat
 | `T_Q f(x)`       | `linearizedCarlesonOperator Q K f x` | The linearized generalized Carleson operator        |
 | `T_𝓝^θ f(x)`       | `nontangentialMaximalFunction θ f x` |   |
 | `Tₚ f(x)`       | `carlesonOn p f x`       |         |
+| `T_ℭ f(x)`       | `carlesonSum ℭ f x`       | The sum of Tₚ f(x) for p ∈ ℭ. In the blueprint only used in chapter 7, but in the formalization we will use it more.        |
+| `Tₚ* f(x)`       | `adjointCarleson p f x`       |         |
 | `e(x)`       | `Complex.exp (Complex.I * x)` |         |
 | `𝔓(I)`       | `𝓘 ⁻¹' {I}` |         |
 | `I ⊆ J`         | `I ≤ J`      | We noticed recently that we cannot (easily) assume that the coercion `Grid X → Set X` is injective. Therefore, Lean introduces two orders on `Grid X`: `I ⊆ J` means that the underlying sets satisfy this relation, and `I ≤ J` means *additionally* that `s I ≤ s J`. The order is what you should use in (almost?) all cases. |
@@ -48,8 +50,12 @@ Below, I will try to give a translation of some notation/conventions. We use mat
 | `M`        | `globalMaximalFunction volume 1` |     |
 | `I_i(x)`        | `cubeOf i x` |     |
 | `R_Q(θ, x)`        | `upperRadius Q θ x` |     |
-| `S_{1,𝔲} f(x)`        | `boundaryOperator1 t u f x` |     |
-| `S_{2,𝔲} g(x)`        | `boundaryOperator2 t u g x` |     |
-| ``        | `` |     |
-| ``        | `` |     |
-| ``        | `` |     |
+| `S_{1,𝔲} f(x)`        | `boundaryOperator t u f x` |     |
+| `S_{2,𝔲} g(x)`        | `adjointBoundaryOperator t u g x` |     |
+| `𝔘`        | `t` | `t` is the (implicit) forest, sometimes `(t : Set (𝔓 X))` is required. It is equivalent to `t.𝔘` |
+| `u ∈ 𝔘`        | `u ∈ t` | `t` is the (implicit) forest, and this notation is equivalent to `u ∈ t.𝔘` |
+| `𝔗(u)`        | `t u` | `t` is the (implicit) forest, and this notation is equivalent to `t.𝔗 u`  |
+| `𝔘ⱼ`        | `rowDecomp t j` | sometimes `(rowDecomp t j : Set (𝔓 X))`    |
+| `𝔗ⱼ(u)`        | `rowDecomp t j u` |     |
+| `E`        | `E` |     |
+| `Eⱼ`        | `rowSupport t j` |     |

Carleson/Classical/ClassicalCarleson.lean

@@ -12,7 +12,7 @@ noncomputable section
 local notation "S_" => partialFourierSum
 
 /- Theorem 1.1 (Classical Carleson) -/
-theorem classical_carleson {f : ℝ → ℂ}
+theorem exceptional_set_carleson {f : ℝ → ℂ}
     (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π))
     {ε : ℝ} (εpos : 0 < ε) :
     ∃ E ⊆ Set.Icc 0 (2 * π), MeasurableSet E ∧ volume.real E ≤ ε ∧
@@ -105,8 +105,8 @@ theorem carleson_interval {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f
     rw [one_mul]
     norm_num
 
-  -- Main step: Apply classical_carleson to get a family of exceptional sets parameterized by ε.
-  choose Eε hEε_subset _ hEε_measure hEε using (@classical_carleson f cont_f periodic_f)
+  -- Main step: Apply exceptional_set_carleson to get a family of exceptional sets parameterized by ε.
+  choose Eε hEε_subset _ hEε_measure hEε using (@exceptional_set_carleson f cont_f periodic_f)
 
   have Eεmeasure {ε : ℝ} (hε : 0 < ε) : volume (Eε hε) ≤ ENNReal.ofReal ε := by
     rw [ENNReal.le_ofReal_iff_toReal_le _ hε.le]
@@ -204,7 +204,7 @@ lemma Function.Periodic.ae_of_ae_restrict {T : ℝ} (hT : 0 < T) {a : ℝ} {P :
 end section
 
 /- Carleson's theorem asserting a.e. convergence of the partial Fourier sums for continous functions. -/
-theorem carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)) :
+theorem classical_carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)) :
     ∀ᵐ x, Filter.Tendsto (S_ · f x) Filter.atTop (nhds (f x)) := by
   -- Reduce to a.e. convergence on [0,2π]
   apply @Function.Periodic.ae_of_ae_restrict _ Real.two_pi_pos 0

Carleson/Discrete/Defs.lean

@@ -1,4 +1,3 @@
-import Carleson.Forest
 import Carleson.MinLayerTiles
 
 open MeasureTheory Measure NNReal Metric Set

Carleson/Discrete/Forests.lean

@@ -1,4 +1,5 @@
 import Carleson.Discrete.ExceptionalSet
+import Carleson.Forest
 
 open MeasureTheory Measure NNReal Metric Complex Set
 open scoped ENNReal
@@ -128,13 +129,13 @@ lemma dens1_le_dens' {P : Set (𝔓 X)} (hP : P ⊆ TilesAt k) : dens₁ P ≤ d
     apply absurd _ this.2; use J, sl.1.trans lJ
 
 /-- Lemma 5.3.12 -/
-lemma dens1_le {A : Set (𝔓 X)} (hA : A ⊆ ℭ k n) : dens₁ A ≤ 2 ^ (4 * a - n + 1 : ℤ) :=
+lemma dens1_le {A : Set (𝔓 X)} (hA : A ⊆ ℭ k n) : dens₁ A ≤ 2 ^ (4 * (a : ℝ) - n + 1) :=
   calc
     _ ≤ dens' k A := dens1_le_dens' (hA.trans ℭ_subset_TilesAt)
     _ ≤ dens' k (ℭ (X := X) k n) := iSup_le_iSup_of_subset hA
     _ ≤ _ := by
       rw [dens'_iSup, iSup₂_le_iff]; intro p mp
-      rw [ℭ, mem_setOf] at mp; exact mp.2.2
+      rw [ℭ, mem_setOf] at mp; exact_mod_cast mp.2.2
 
 /-! ## Section 5.4 and Lemma 5.1.2 -/
 
@@ -584,14 +585,14 @@ variable (k n j l) in
 def forest : Forest X n where
   𝔘 := 𝔘₄ k n j l
   𝔗 := 𝔗₂ k n j
-  nonempty {u} hu := sorry
-  ordConnected {u} hu := forest_convex
-  𝓘_ne_𝓘 hu hp := sorry
-  smul_four_le {u} hu := forest_geometry <| 𝔘₄_subset_𝔘₃ hu
-  stackSize_le {x} := stackSize_𝔘₄_le x
-  dens₁_𝔗_le {u} hu := dens1_le <| 𝔗₂_subset_ℭ₆.trans ℭ₆_subset_ℭ
-  lt_dist hu hu' huu' p hp := forest_separation (𝔘₄_subset_𝔘₃ hu) (𝔘₄_subset_𝔘₃ hu') huu' hp
-  ball_subset hu p hp := forest_inner (𝔘₄_subset_𝔘₃ hu) hp
+  nonempty' {u} hu := sorry
+  ordConnected' {u} hu := forest_convex
+  𝓘_ne_𝓘' hu hp := sorry
+  smul_four_le' {u} hu := forest_geometry <| 𝔘₄_subset_𝔘₃ hu
+  stackSize_le' {x} := stackSize_𝔘₄_le x
+  dens₁_𝔗_le' {u} hu := dens1_le <| 𝔗₂_subset_ℭ₆.trans ℭ₆_subset_ℭ
+  lt_dist' hu hu' huu' p hp := forest_separation (𝔘₄_subset_𝔘₃ hu) (𝔘₄_subset_𝔘₃ hu') huu' hp
+  ball_subset' hu p hp := forest_inner (𝔘₄_subset_𝔘₃ hu) hp
 
 /-- The constant used in Lemma 5.1.2, with value `2 ^ (235 * a ^ 3) / (q - 1) ^ 4` -/
 -- todo: redefine in terms of other constants
@@ -600,7 +601,7 @@ def C5_1_2 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := 2 ^ (235 * a ^ 3) / (q - 1) ^ 4
 lemma C5_1_2_pos : C5_1_2 a nnq > 0 := sorry
 
 lemma forest_union {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
-  ∫⁻ x in G \ G', ‖∑ p ∈ { p | p ∈ 𝔓₁ }, carlesonOn p f x‖₊ ≤
+  ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ f x‖₊ ≤
     C5_1_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹  := by
   sorry
 
@@ -944,8 +945,8 @@ def C5_1_3 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := 2 ^ (210 * a ^ 3) / (q - 1) ^ 5
 lemma C5_1_3_pos : C5_1_3 a nnq > 0 := sorry
 
 lemma forest_complement {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
-  ∫⁻ x in G \ G', ‖∑ p ∈ { p | p ∉ 𝔓₁ }, carlesonOn p f x‖₊ ≤
-    C5_1_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹  := by
+  ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ᶜ f x‖₊ ≤
+    C5_1_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ := by
   sorry
 
 /-! ## Proposition 2.0.2 -/
@@ -960,5 +961,5 @@ variable (X) in
 theorem discrete_carleson :
     ∃ G', MeasurableSet G' ∧ 2 * volume G' ≤ volume G ∧
     ∀ f : X → ℂ, Measurable f → (∀ x, ‖f x‖ ≤ F.indicator 1 x) →
-    ∫⁻ x in G \ G', ‖∑ p, carlesonOn p f x‖₊ ≤
+    ∫⁻ x in G \ G', ‖carlesonSum univ f x‖₊ ≤
     C2_0_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ := by sorry

Carleson/DoublingMeasure.lean

@@ -111,7 +111,7 @@ lemma measure_ball_le_pow_two {x : X} {r : ℝ} {n : ℕ} :
       _ ≤ A * μ.real (ball x (2 ^ m * r)) := by
         rw[mul_assoc]; norm_cast; exact measure_real_ball_two_le_same _ _
       _ ≤ A * (↑(A ^ m) * μ.real (ball x r)) := by
-        exact mul_le_mul_of_nonneg_left hm (by exact zero_le_coe)
+        exact mul_le_mul_of_nonneg_left hm zero_le_coe
       _ = A^(m.succ) * μ.real (ball x r) := by rw [NNReal.coe_pow,← mul_assoc, pow_succ']
 
 lemma measure_ball_le_pow_two' {x : X} {r : ℝ} {n : ℕ} :

Carleson/FinitaryCarleson.lean

@@ -40,7 +40,7 @@ private lemma 𝔓_biUnion : @Finset.univ (𝔓 X) _ = (Icc (-S : ℤ) S).toFins
 
 private lemma sum_eq_zero_of_nmem_Icc {f : X → ℂ} {x : X} (s : ℤ)
     (hs : s ∈ (Icc (-S : ℤ) S).toFinset.filter (fun t ↦ t ∉ Icc (σ₁ x) (σ₂ x))) :
-    ∑ i ∈ Finset.filter (fun p ↦ 𝔰 p = s) Finset.univ, carlesonOn i f x = 0 := by
+    ∑ i ∈ Finset.univ.filter (fun p ↦ 𝔰 p = s), carlesonOn i f x = 0 := by
   refine Finset.sum_eq_zero (fun p hp ↦ ?_)
   simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hp
   simp only [mem_Icc, not_and, not_le, toFinset_Icc, Finset.mem_filter, Finset.mem_Icc] at hs
@@ -111,7 +111,8 @@ theorem finitary_carleson : ∃ G', MeasurableSet G' ∧ 2 * volume G' ≤ volum
   rcases discrete_carleson X with ⟨G', hG', h2G', hfG'⟩
   refine ⟨G', hG', h2G', fun f meas_f h2f ↦ le_of_eq_of_le ?_ (hfG' f meas_f h2f)⟩
   refine setLIntegral_congr_fun (measurableSet_G.diff hG') (ae_of_all volume fun x hx ↦ ?_)
-  simp_rw [tile_sum_operator hx, mul_sub, exp_sub, mul_div, div_eq_mul_inv,
+  simp_rw [carlesonSum, mem_univ, Finset.filter_True, tile_sum_operator hx, mul_sub, exp_sub,
+    mul_div, div_eq_mul_inv,
     ← smul_eq_mul (a' := _⁻¹), integral_smul_const, ← Finset.sum_smul, nnnorm_smul]
   suffices ‖(cexp (I * ((Q x) x : ℂ)))⁻¹‖₊ = 1 by rw [this, mul_one]
   simp [← coe_eq_one, mul_comm I]

Carleson/Forest.lean

@@ -7,52 +7,9 @@ noncomputable section
 open scoped ShortVariables
 variable {X : Type*} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ}
   {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G]
-variable [TileStructure Q D κ S o] {p p' : 𝔓 X} {f g : Θ X}
+variable [TileStructure Q D κ S o] {u u' p p' : 𝔓 X} {f g : Θ X}
   {C C' : Set (𝔓 X)} {x x' : X}
 
-/-- The number of tiles `p` in `s` whose underlying cube `𝓘 p` contains `x`. -/
-def stackSize (C : Set (𝔓 X)) (x : X) : ℕ :=
-  ∑ p ∈ { p | p ∈ C }, (𝓘 p : Set X).indicator 1 x
-
-lemma stackSize_setOf_add_stackSize_setOf_not {P : 𝔓 X → Prop} :
-    stackSize {p ∈ C | P p} x + stackSize {p ∈ C | ¬ P p} x = stackSize C x := by
-  classical
-  simp_rw [stackSize]
-  conv_rhs => rw [← Finset.sum_filter_add_sum_filter_not _ P]
-  simp_rw [Finset.filter_filter]
-  congr
-
-lemma stackSize_congr (h : ∀ p ∈ C, x ∈ (𝓘 p : Set X) ↔ x' ∈ (𝓘 p : Set X)) :
-    stackSize C x = stackSize C x' := by
-  refine Finset.sum_congr rfl fun p hp ↦ ?_
-  simp_rw [Finset.mem_filter, Finset.mem_univ, true_and] at hp
-  simp_rw [indicator, h p hp, Pi.one_apply]
-
-lemma stackSize_mono (h : C ⊆ C') : stackSize C x ≤ stackSize C' x := by
-  apply Finset.sum_le_sum_of_subset (fun x ↦ ?_)
-  simp [iff_true_intro (@h x)]
-
--- Simplify the cast of `stackSize C x` from `ℕ` to `ℝ`
-lemma stackSize_real (C : Set (𝔓 X)) (x : X) : (stackSize C x : ℝ) =
-    ∑ p ∈ { p | p ∈ C }, (𝓘 p : Set X).indicator (1 : X → ℝ) x := by
-  rw [stackSize, Nat.cast_sum]
-  refine Finset.sum_congr rfl (fun u _ ↦ ?_)
-  by_cases hx : x ∈ (𝓘 u : Set X) <;> simp [hx]
-
-lemma stackSize_measurable : Measurable fun x ↦ (stackSize C x : ℝ≥0∞) := by
-  simp_rw [stackSize, Nat.cast_sum, indicator, Nat.cast_ite]
-  refine Finset.measurable_sum _ fun _ _ ↦ Measurable.ite coeGrid_measurable ?_ ?_ <;> simp
-
-/-! We might want to develop some API about partitioning a set.
-But maybe `Set.PairwiseDisjoint` and `Set.Union` are enough.
-Related, but not quite useful: `Setoid.IsPartition`. -/
-
--- /-- `u` is partitioned into subsets in `C`. -/
--- class Set.IsPartition {α ι : Type*} (u : Set α) (s : Set ι) (C : ι → Set α) : Prop :=
---   pairwiseDisjoint : s.PairwiseDisjoint C
---   iUnion_eq : ⋃ (i ∈ s), C i = u
-
-
 namespace TileStructure
 -- variable (X) in
 -- structure Tree where
@@ -71,73 +28,59 @@ variable (X) in
 /-- An `n`-forest -/
 structure Forest (n : ℕ) where
   𝔘 : Set (𝔓 X)
-  𝔗 : 𝔓 X → Set (𝔓 X) -- Is it a problem that we totalized this function?
-  nonempty {u} (hu : u ∈ 𝔘) : (𝔗 u).Nonempty
-  ordConnected {u} (hu : u ∈ 𝔘) : OrdConnected (𝔗 u) -- (2.0.33)
-  𝓘_ne_𝓘 {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : 𝓘 p ≠ 𝓘 u
-  smul_four_le {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : smul 4 p ≤ smul 1 u -- (2.0.32)
-  stackSize_le {x} : stackSize 𝔘 x ≤ 2 ^ n -- (2.0.34), we formulate this a bit differently.
-  dens₁_𝔗_le {u} (hu : u ∈ 𝔘) : dens₁ (𝔗 u : Set (𝔓 X)) ≤ 2 ^ (4 * a - n + 1 : ℤ) -- (2.0.35)
-  lt_dist {u u'} (hu : u ∈ 𝔘) (hu' : u' ∈ 𝔘) (huu' : u ≠ u') {p} (hp : p ∈ 𝔗 u')
+  /-- The value of `𝔗 u` only matters when `u ∈ 𝔘`. -/
+  𝔗 : 𝔓 X → Set (𝔓 X)
+  nonempty' {u} (hu : u ∈ 𝔘) : (𝔗 u).Nonempty
+  ordConnected' {u} (hu : u ∈ 𝔘) : OrdConnected (𝔗 u) -- (2.0.33)
+  𝓘_ne_𝓘' {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : 𝓘 p ≠ 𝓘 u
+  smul_four_le' {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : smul 4 p ≤ smul 1 u -- (2.0.32)
+  stackSize_le' {x} : stackSize 𝔘 x ≤ 2 ^ n -- (2.0.34), we formulate this a bit differently.
+  dens₁_𝔗_le' {u} (hu : u ∈ 𝔘) : dens₁ (𝔗 u) ≤ 2 ^ (4 * (a : ℝ) - n + 1) -- (2.0.35)
+  lt_dist' {u u'} (hu : u ∈ 𝔘) (hu' : u' ∈ 𝔘) (huu' : u ≠ u') {p} (hp : p ∈ 𝔗 u')
     (h : 𝓘 p ≤ 𝓘 u) : 2 ^ (Z * (n + 1)) < dist_(p) (𝒬 p) (𝒬 u) -- (2.0.36)
-  ball_subset {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : ball (𝔠 p) (8 * D ^ 𝔰 p) ⊆ 𝓘 u -- (2.0.37)
-  -- old conditions
-  -- disjoint_I : ∀ {𝔗 𝔗'}, 𝔗 ∈ I → 𝔗' ∈ I → Disjoint 𝔗.carrier 𝔗'.carrier
-  -- top_finite (x : X) : {𝔗 ∈ I | x ∈ Grid (𝓘 𝔗.top)}.Finite
-  -- card_top_le (x : X) : Nat.card {𝔗 ∈ I | x ∈ Grid (𝓘 𝔗.top) } ≤ 2 ^ n * Real.log (n + 1)
-  -- density_le {𝔗} (h𝔗 : 𝔗 ∈ I) : density G Q 𝔗 ≤ (2 : ℝ) ^ (-n : ℤ)
-  -- delta_gt {j j'} (hj : j ∈ I) (hj' : j' ∈ I) (hjj' : j ≠ j') {p : 𝔓 X} (hp : p ∈ j)
-  --   (h2p : Grid (𝓘 p) ⊆ Grid (𝓘 j'.top)) : Δ p (Q j.top) > (2 : ℝ) ^ (3 * n / δ)
-
-end TileStructure
-
---below is old
-
--- class Tree.IsThin (𝔗 : Tree X) : Prop where
---   thin {p : 𝔓 X} (hp : p ∈ 𝔗) : ball (𝔠 p) (8 * a/-fix-/ * D ^ 𝔰 p) ⊆ Grid (𝓘 𝔗.top)
+  ball_subset' {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : ball (𝔠 p) (8 * D ^ 𝔰 p) ⊆ 𝓘 u -- (2.0.37)
 
--- alias Tree.thin := Tree.IsThin.thin
+namespace Forest
 
--- def Δ (p : 𝔓 X) (Q' : C(X, ℝ)) : ℝ := localOscillation (Grid (𝓘 p)) (𝒬 p) Q' + 1
+variable {n : ℕ} (t : Forest X n)
 
--- namespace Forest
+instance : CoeHead (Forest X n) (Set (𝔓 X)) := ⟨Forest.𝔘⟩
+instance : Membership (𝔓 X) (Forest X n) := ⟨fun t x ↦ x ∈ (t : Set (𝔓 X))⟩
+instance : CoeFun (Forest X n) (fun _ ↦ 𝔓 X → Set (𝔓 X)) := ⟨fun t x ↦ t.𝔗 x⟩
 
-/- Do we want to treat a forest as a set of trees, or a set of elements from `𝔓 X`? -/
+@[simp] lemma mem_𝔘 : u ∈ t.𝔘 ↔ u ∈ t := .rfl
+@[simp] lemma mem_𝔗 : p ∈ t.𝔗 u ↔ p ∈ t u := .rfl
 
--- instance : SetLike (Forest G Q δ n) (Tree X) where
---   coe s := s.I
---   coe_injective' p q h := by cases p; cases q; congr
+lemma nonempty (hu : u ∈ t) : (t u).Nonempty := t.nonempty' hu
+lemma ordConnected (hu : u ∈ t) : OrdConnected (t u) := t.ordConnected' hu
+lemma 𝓘_ne_𝓘 (hu : u ∈ t) (hp : p ∈ t u) : 𝓘 p ≠ 𝓘 u := t.𝓘_ne_𝓘' hu hp
+lemma smul_four_le (hu : u ∈ t) (hp : p ∈ t u) : smul 4 p ≤ smul 1 u := t.smul_four_le' hu hp
+lemma stackSize_le : stackSize t x ≤ 2 ^ n := t.stackSize_le'
+lemma dens₁_𝔗_le (hu : u ∈ t) : dens₁ (t u) ≤ 2 ^ (4 * (a : ℝ) - n + 1) := t.dens₁_𝔗_le' hu
+lemma lt_dist (hu : u ∈ t) (hu' : u' ∈ t) (huu' : u ≠ u') {p} (hp : p ∈ t u') (h : 𝓘 p ≤ 𝓘 u) :
+    2 ^ (Z * (n + 1)) < dist_(p) (𝒬 p) (𝒬 u) := t.lt_dist' hu hu' huu' hp h
+lemma ball_subset (hu : u ∈ t) (hp : p ∈ t u) : ball (𝔠 p) (8 * D ^ 𝔰 p) ⊆ 𝓘 u :=
+  t.ball_subset' hu hp
 
--- instance : PartialOrder (Forest G Q δ n) := PartialOrder.lift (↑) SetLike.coe_injective
+end Forest
 
--- class IsThin (𝔉 : Forest G Q δ n) : Prop where
---   thin {𝔗} (h𝔗 : 𝔗 ∈ 𝔉.I) : 𝔗.IsThin
-
--- alias thin := Forest.IsThin.thin
-
--- /-- The union of all the trees in the forest. -/
--- def carrier (𝔉 : Forest G Q δ n) : Set (𝔓 X) := ⋃ 𝔗 ∈ 𝔉.I, 𝔗
+variable (X) in
+/-- An `n`-row -/
+structure Row (n : ℕ) extends Forest X n where
+  pairwiseDisjoint' : 𝔘.PairwiseDisjoint 𝔗
 
---end Forest
+namespace Row
 
--- set_option linter.unusedVariables false in
--- variable (X) in
--- class SmallBoundaryProperty (η : ℝ) : Prop where
---   volume_diff_le : ∃ (C : ℝ) (hC : C > 0), ∀ (x : X) r (δ : ℝ), 0 < r → 0 < δ → δ < 1 →
---     volume.real (ball x ((1 + δ) * r) \ ball x ((1 - δ) * r)) ≤ C * δ ^ η * volume.real (ball x r)
+variable {n : ℕ} (t : Row X n)
 
---def boundedTiles (F : Set X) (t : ℝ) : Set (𝔓 X) :=
---  { p : 𝔓 X | ∃ x ∈ 𝓘 p, maximalFunction volume (Set.indicator F (1 : X → ℂ)) x ≤ t }
+instance : CoeHead (Row X n) (Set (𝔓 X)) := ⟨fun t ↦ t.𝔘⟩
+instance : Membership (𝔓 X) (Row X n) := ⟨fun t x ↦ x ∈ (t : Set (𝔓 X))⟩
+instance : CoeFun (Row X n) (fun _ ↦ 𝔓 X → Set (𝔓 X)) := ⟨fun t x ↦ t.𝔗 x⟩
 
--- set_option linter.unusedVariables false in
--- variable (X) in
--- class SmallBoundaryProperty (η : ℝ) : Prop where
---   volume_diff_le : ∃ (C : ℝ) (hC : C > 0), ∀ (x : X) r (δ : ℝ), 0 < r → 0 < δ → δ < 1 →
---     volume.real (ball x ((1 + δ) * r) \ ball x ((1 - δ) * r)) ≤ C * δ ^ η * volume.real (ball x r)
+@[simp] lemma mem_𝔘 : u ∈ t.𝔘 ↔ u ∈ t := .rfl
+@[simp] lemma mem_𝔗 : p ∈ t.𝔗 u ↔ p ∈ t u := .rfl
 
-/- This is defined to live in `ℝ≥0∞`. Use `ENNReal.toReal` to get a real number. -/
-/- def MB_p {ι : Type*} [Fintype ι] (p : ℝ) (ℬ : ι → X × ℝ) (u : X → ℂ) (x : X) : ℝ≥0∞ :=
-  ⨆ (i : ι) , indicator (ball (ℬ i).1 (ℬ i).2) (1 : X → ℝ≥0∞) x / volume (ball (ℬ i).1 (ℬ i).2) *
-    (∫⁻ y in (ball (ℬ i).1 (ℬ i).2), ‖u y‖₊^p)^(1/p)
+lemma pairwiseDisjoint : Set.PairwiseDisjoint t t := t.pairwiseDisjoint'
 
-abbrev MB {ι : Type*} [Fintype ι] (ℬ : ι → X × ℝ) (u : X → ℂ) (x : X) := MB_p 1 ℬ u x -/
+end Row
+end TileStructure