From 81521079e5877cc12d8b08b8c22b3dbf29a86a22 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 12 Jul 2024 21:44:19 +0200 Subject: [PATCH] prepare section 5.4 --- CONTRIBUTING.md | 4 +- Carleson/DiscreteCarleson.lean | 240 ++++++++++++++++++++++++--------- Carleson/Forest.lean | 75 ++++++++--- Carleson/ForestOperator.lean | 5 +- Carleson/ToMathlib/Misc.lean | 79 +++++++++++ blueprint/src/chapter/main.tex | 22 ++- 6 files changed, 341 insertions(+), 84 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 2f364913..c39b31bc 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -37,4 +37,6 @@ Below, I will try to give a translation of some notation/conventions. We use mat | `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. | -| `𝓓` | `Grid` | The unicode characters were causing issues with Overleaf and leanblueprint (on Windows) | \ No newline at end of file +| `𝓓` | `Grid` | The unicode characters were causing issues with Overleaf and leanblueprint (on Windows) | +| `𝔓_{G\G'}` | `𝔓pos` | | +| `𝔓₂` | `π”“β‚αΆœ` | | \ No newline at end of file diff --git a/Carleson/DiscreteCarleson.lean b/Carleson/DiscreteCarleson.lean index adc2a4d1..a8c82bba 100644 --- a/Carleson/DiscreteCarleson.lean +++ b/Carleson/DiscreteCarleson.lean @@ -72,9 +72,7 @@ def 𝔏₀ (k n : β„•) : Set (𝔓 X) := def 𝔏₁ (k n j l : β„•) : Set (𝔓 X) := minimals (·≀·) (ℭ₁ k n j \ ⋃ (l' < l), 𝔏₁ k n j l') -/-- The subset `β„­β‚‚(k, n, j)` of `ℭ₁(k, n, j)`, given in (5.1.13). -To check: the current definition assumes that `𝔏₁ k n j (Z * (n + 1)) = βˆ…`, -otherwise we need to add an upper bound. -/ +/-- The subset `β„­β‚‚(k, n, j)` of `ℭ₁(k, n, j)`, given in (5.1.13). -/ def β„­β‚‚ (k n j : β„•) : Set (𝔓 X) := ℭ₁ k n j \ ⋃ (l ≀ Z * (n + 1)), 𝔏₁ k n j l @@ -101,11 +99,9 @@ lemma ℭ₃_subset_β„­β‚‚ {k n j : β„•} : ℭ₃ k n j βŠ† β„­β‚‚ (X := X) k n def 𝔏₃ (k n j l : β„•) : Set (𝔓 X) := maximals (·≀·) (ℭ₃ k n j \ ⋃ (l' < l), 𝔏₃ k n j l') -/-- The subset `β„­β‚„(k, n, j)` of `ℭ₃(k, n, j)`, given in (5.1.19). -To check: the current definition assumes that `𝔏₃ k n j (Z * (n + 1)) = βˆ…`, -otherwise we need to add an upper bound. -/ +/-- The subset `β„­β‚„(k, n, j)` of `ℭ₃(k, n, j)`, given in (5.1.19). -/ def β„­β‚„ (k n j : β„•) : Set (𝔓 X) := - ℭ₃ k n j \ ⋃ (l : β„•), 𝔏₃ k n j l + ℭ₃ k n j \ ⋃ (l ≀ Z * (n + 1)), 𝔏₃ k n j l lemma β„­β‚„_subset_ℭ₃ {k n j : β„•} : β„­β‚„ k n j βŠ† ℭ₃ (X := X) k n j := fun t mt ↦ by rw [β„­β‚„, mem_diff] at mt; exact mt.1 @@ -137,12 +133,11 @@ def G₁ : Set X := ⋃ (p : 𝔓 X) (_ : p ∈ highDensityTiles), π“˜ p /-- The set `A(Ξ», k, n)`, defined in (5.1.26). -/ def setA (l k n : β„•) : Set X := - {x : X | l * 2 ^ (n + 1) < βˆ‘ p ∈ Finset.univ.filter (Β· ∈ 𝔐 (X := X) k n), - (π“˜ p : Set X).indicator 1 x } + {x : X | l * 2 ^ (n + 1) < stackSize (𝔐 (X := X) k n) x } lemma setA_subset_iUnion_𝓒 {l k n : β„•} : setA (X := X) l k n βŠ† ⋃ i ∈ 𝓒 (X := X) k, ↑i := fun x mx ↦ by - simp_rw [setA, mem_setOf, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id, + simp_rw [setA, mem_setOf, stackSize, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id, Finset.filter_filter] at mx replace mx := (zero_le _).trans_lt mx rw [Finset.card_pos] at mx @@ -178,7 +173,7 @@ def G' : Set X := G₁ βˆͺ Gβ‚‚ βˆͺ G₃ /-- The set `𝔓₁`, defined in (5.1.30). -/ def 𝔓₁ : Set (𝔓 X) := ⋃ (n : β„•) (k ≀ n) (j ≀ 2 * n + 3), β„­β‚… k n j -variable {k n j l : β„•} {p p' : 𝔓 X} {x : X} +variable {k n j l : β„•} {p p' u u' : 𝔓 X} {x : X} /-! ## Section 5.2 and Lemma 5.1.1 -/ @@ -231,7 +226,7 @@ lemma pairwiseDisjoint_E1 : (𝔐 (X := X) k n).PairwiseDisjoint E₁ := fun p m /-- Lemma 5.2.4 -/ lemma dyadic_union (hx : x ∈ setA l k n) : βˆƒ i : Grid X, x ∈ i ∧ (i : Set X) βŠ† setA l k n := by let M : Finset (𝔓 X) := Finset.univ.filter (fun p ↦ p ∈ 𝔐 k n ∧ x ∈ π“˜ p) - simp_rw [setA, mem_setOf, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id, + simp_rw [setA, mem_setOf, stackSize, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id, Finset.filter_filter] at hx ⊒ obtain ⟨b, memb, minb⟩ := M.exists_min_image 𝔰 (Finset.card_pos.mp (zero_le'.trans_lt hx)) simp_rw [M, Finset.mem_filter, Finset.mem_univ, true_and] at memb minb @@ -250,27 +245,24 @@ lemma iUnion_MsetA_eq_setA : ⋃ i ∈ MsetA (X := X) l k n, ↑i = setA (X := X /-- Equation (5.2.7) in the proof of Lemma 5.2.5. -/ lemma john_nirenberg_aux1 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n)) (mx : x ∈ setA (l + 1) k n) (mxβ‚‚ : x ∈ L) : 2 ^ (n + 1) ≀ - βˆ‘ q ∈ Finset.univ.filter (fun q ↦ q ∈ 𝔐 (X := X) k n ∧ π“˜ q ≀ L), - (π“˜ q : Set X).indicator 1 x := by + stackSize { q ∈ 𝔐 (X := X) k n | π“˜ q ≀ L} x := by -- LHS of equation (5.2.6) is strictly greater than `(l + 1) * 2 ^ (n + 1)` - rw [setA, mem_setOf, ← Finset.sum_filter_add_sum_filter_not (p := fun p' ↦ π“˜ p' ≀ L), - Finset.filter_filter, Finset.filter_filter] at mx + rw [setA, mem_setOf, ← stackSize_setOf_add_stackSize_setOf_not (P := fun p' ↦ π“˜ p' ≀ L)] at mx -- Rewrite second sum of RHS of (5.2.6) so that it sums over tiles `q` satisfying `L < π“˜ q` - nth_rw 2 [← Finset.sum_filter_add_sum_filter_not (p := fun p' ↦ Disjoint (π“˜ p' : Set X) L)] at mx - rw [Finset.filter_filter, Finset.filter_filter] at mx - have mid0 : βˆ‘ q ∈ Finset.univ.filter - (fun p' ↦ (p' ∈ 𝔐 k n ∧ Β¬π“˜ p' ≀ L) ∧ Disjoint (π“˜ p' : Set X) L), - (π“˜ q : Set X).indicator 1 x = 0 := by - simp_rw [Finset.sum_eq_zero_iff, indicator_apply_eq_zero, imp_false, Finset.mem_filter, - Finset.mem_univ, true_and] - rintro y ⟨-, dj⟩ - exact disjoint_right.mp dj mxβ‚‚ + nth_rw 2 [← stackSize_setOf_add_stackSize_setOf_not (P := fun p' ↦ Disjoint (π“˜ p' : Set X) L)] + at mx + simp_rw [mem_setOf_eq, and_assoc] at mx + have mid0 : stackSize { p' ∈ 𝔐 k n | Β¬π“˜ p' ≀ L ∧ Disjoint (π“˜ p' : Set X) L} x = 0 := by + simp_rw [stackSize, Finset.sum_eq_zero_iff, indicator_apply_eq_zero, imp_false, + Finset.mem_filter, Finset.mem_univ, true_and] + rintro y ⟨-, -, dj2⟩ + exact disjoint_right.mp dj2 mxβ‚‚ rw [mid0, zero_add] at mx have req : - Finset.univ.filter (fun p' ↦ (p' ∈ 𝔐 k n ∧ Β¬π“˜ p' ≀ L) ∧ Β¬Disjoint (π“˜ p' : Set X) L) = - Finset.univ.filter (fun p' ↦ p' ∈ 𝔐 k n ∧ L < π“˜ p') := by + { p' | p' ∈ 𝔐 k n ∧ Β¬π“˜ p' ≀ L ∧ Β¬Disjoint (π“˜ p' : Set X) L } = + { p' | p' ∈ 𝔐 k n ∧ L < π“˜ p' } := by ext q - simp_rw [Finset.mem_filter, Finset.mem_univ, true_and, and_assoc, and_congr_right_iff] + simp_rw [mem_setOf_eq, and_congr_right_iff] refine fun _ ↦ ⟨fun h ↦ ?_, ?_⟩ Β· apply lt_of_le_of_ne <| (le_or_ge_or_disjoint.resolve_left h.1).resolve_right h.2 by_contra k; subst k; simp at h @@ -278,19 +270,17 @@ lemma john_nirenberg_aux1 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n)) exact fun h ↦ ⟨Or.inr h.2, not_disjoint_iff.mpr ⟨x, mem_of_mem_of_subset mxβ‚‚ h.1, mxβ‚‚βŸ©βŸ© rw [req] at mx -- The new second sum of RHS is at most `l * 2 ^ (n + 1)` - set Q₁ := Finset.univ.filter (fun q ↦ q ∈ 𝔐 (X := X) k n ∧ π“˜ q ≀ L) - set Qβ‚‚ := Finset.univ.filter (fun q ↦ q ∈ 𝔐 (X := X) k n ∧ L < π“˜ q) - have Ql : βˆ‘ q ∈ Qβ‚‚, (π“˜ q : Set X).indicator 1 x ≀ l * 2 ^ (n + 1) := by + set Q₁ := { q ∈ 𝔐 (X := X) k n | π“˜ q ≀ L } + set Qβ‚‚ := { q ∈ 𝔐 (X := X) k n | L < π“˜ q } + have Ql : stackSize Qβ‚‚ x ≀ l * 2 ^ (n + 1) := by by_cases h : IsMax L Β· rw [Grid.isMax_iff] at h have : Qβ‚‚ = βˆ… := by - ext y; simp_rw [Qβ‚‚, Finset.mem_filter, Finset.mem_univ, true_and, Finset.not_mem_empty, - iff_false, not_and, h, Grid.lt_def, not_and_or, not_lt] + ext y; simp_rw [Qβ‚‚, mem_setOf_eq, Set.not_mem_empty, iff_false, not_and, h, Grid.lt_def, + not_and_or, not_lt] exact fun _ ↦ Or.inr (Grid.le_topCube).2 - simp [this] - have Lslq : βˆ€ q ∈ Qβ‚‚, L.succ ≀ π“˜ q := fun q mq ↦ by - simp_rw [Qβ‚‚, Finset.mem_filter, Finset.mem_univ, true_and] at mq - exact Grid.succ_le_of_lt mq.2 + simp [stackSize, this] + have Lslq : βˆ€ q ∈ Qβ‚‚, L.succ ≀ π“˜ q := fun q mq ↦ Grid.succ_le_of_lt mq.2 have Lout : Β¬(L.succ : Set X) βŠ† setA (X := X) l k n := by by_contra! hs rw [Grid.maxCubes, Finset.mem_filter] at mL @@ -300,16 +290,12 @@ lemma john_nirenberg_aux1 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n)) rw [not_subset_iff_exists_mem_not_mem] at Lout obtain ⟨x', mx', nx'⟩ := Lout calc - _ = βˆ‘ q ∈ Qβ‚‚, (π“˜ q : Set X).indicator 1 x' := by - refine Finset.sum_congr rfl fun q mq ↦ ?_ - simp only [indicator, Pi.one_apply, - mem_of_mem_of_subset mxβ‚‚ (Grid.le_succ.trans (Lslq q mq)).1, + _ = stackSize Qβ‚‚ x' := by + refine stackSize_congr rfl fun q mq ↦ ?_ + simp_rw [mem_of_mem_of_subset mxβ‚‚ (Grid.le_succ.trans (Lslq q mq)).1, mem_of_mem_of_subset mx' (Lslq q mq).1] - _ ≀ βˆ‘ q ∈ Finset.univ.filter (fun q ↦ q ∈ 𝔐 (X := X) k n), - (π“˜ q : Set X).indicator 1 x' := by - refine Finset.sum_le_sum_of_subset ?_ - simp_rw [Qβ‚‚, ← Finset.filter_filter] - apply Finset.filter_subset + _ ≀ stackSize (𝔐 (X := X) k n) x' := by + refine stackSize_mono <| sep_subset .. _ ≀ l * 2 ^ (n + 1) := by rwa [setA, mem_setOf_eq, not_lt] at nx' -- so the (unchanged) first sum of RHS is at least `2 ^ (n + 1)` rw [add_one_mul] at mx; omega @@ -348,7 +334,10 @@ lemma john_nirenberg_aux2 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n)) _ = ∫⁻ x in setA (X := X) (l + 1) k n ∩ L, 2 ^ (n + 1) := (setLIntegral_const _ _).symm _ ≀ ∫⁻ x in setA (X := X) (l + 1) k n ∩ L, βˆ‘ q ∈ Q₁, (π“˜ q : Set X).indicator 1 x := by refine setLIntegral_mono (by simp) (Finset.measurable_sum Q₁ Q₁m) fun x ⟨mx, mxβ‚‚βŸ© ↦ ?_ - have : 2 ^ (n + 1) ≀ βˆ‘ q ∈ Q₁, (π“˜ q : Set X).indicator 1 x := john_nirenberg_aux1 mL mx mxβ‚‚ + have : 2 ^ (n + 1) ≀ βˆ‘ q ∈ Q₁, (π“˜ q : Set X).indicator 1 x := by + convert john_nirenberg_aux1 mL mx mxβ‚‚ + simp_rw [stackSize, Q₁, mem_setOf_eq] + congr have lcast : (2 : ℝβ‰₯0∞) ^ (n + 1) = ((2 ^ (n + 1) : β„•) : ℝ).toNNReal := by rw [toNNReal_coe_nat, ENNReal.coe_natCast]; norm_cast have rcast : βˆ‘ q ∈ Q₁, (π“˜ q : Set X).indicator (1 : X β†’ ℝβ‰₯0∞) x = @@ -469,9 +458,8 @@ lemma top_tiles : βˆ‘ m ∈ Finset.univ.filter (Β· ∈ 𝔐 (X := X) k n), volum sorry /-- Lemma 5.2.8 -/ -lemma tree_count : βˆ‘ u ∈ Finset.univ.filter (Β· ∈ π”˜β‚ (X := X) k n j), (π“˜ u : Set X).indicator 1 x ≀ - 2 ^ (9 * a - j) * βˆ‘ m ∈ Finset.univ.filter (Β· ∈ 𝔐 (X := X) k n), (π“˜ m : Set X).indicator 1 x - := by +lemma tree_count : + stackSize (π”˜β‚ (X := X) k n j) x ≀ 2 ^ (9 * a - j) * stackSize (𝔐 (X := X) k n) x := by sorry variable (X) in @@ -573,11 +561,11 @@ lemma ordConnected_C4 : OrdConnected (β„­β‚„ k n j : Set (𝔓 X)) := by (ordConnected_C3.out (mem_of_mem_of_subset mp β„­β‚„_subset_ℭ₃) mp''₁) by_cases e : p' = p''; Β· rwa [← e] at mp'' simp_rw [β„­β‚„, mem_diff, mp'₁, true_and] - by_contra h; rw [mem_iUnion] at h; obtain ⟨l', p'm⟩ := h + by_contra h; simp_rw [mem_iUnion] at h; obtain ⟨l', hl', p'm⟩ := h rw [𝔏₃, mem_maximals_iff] at p'm; simp_rw [mem_diff] at p'm have p''nm : p'' βˆ‰ ⋃ l'', ⋃ (_ : l'' < l'), 𝔏₃ k n j l'' := by replace mp'' := mp''.2; contrapose! mp'' - exact mem_of_mem_of_subset mp'' (iUnionβ‚‚_subset_iUnion ..) + refine mem_of_mem_of_subset mp'' <| iUnionβ‚‚_mono' fun i hi ↦ ⟨i, hi.le.trans hl', subset_rfl⟩ exact absurd (p'm.2 ⟨mp''₁, p''nm⟩ mp'.2) e /-- Lemma 5.3.10 -/ @@ -618,7 +606,127 @@ lemma dens1_le {A : Set (𝔓 X)} (hA : A βŠ† β„­ k n) : dens₁ A ≀ 2 ^ (4 * /-! ## Section 5.4 and Lemma 5.1.2 -/ +/-- The subset `ℭ₆(k, n, j)` of `β„­β‚…(k, n, j)`, given above (5.4.1). -/ +def ℭ₆ (k n j : β„•) : Set (𝔓 X) := + { p ∈ β„­β‚… k n j | Β¬ (π“˜ p : Set X) βŠ† G' } + +lemma ℭ₆_subset_β„­β‚… : ℭ₆ (X := X) k n j βŠ† β„­β‚… k n j := sep_subset .. +lemma ℭ₆_subset_β„­ : ℭ₆ (X := X) k n j βŠ† β„­ k n := + ℭ₆_subset_β„­β‚… |>.trans β„­β‚…_subset_β„­β‚„ |>.trans β„­β‚„_subset_ℭ₃ |>.trans ℭ₃_subset_β„­β‚‚ |>.trans + β„­β‚‚_subset_ℭ₁ |>.trans ℭ₁_subset_β„­ + +/-- The subset `𝔗₁(u)` of `ℭ₁(k, n, j)`, given in (5.4.1). +In lemmas, we will assume `u ∈ π”˜β‚ k n l` -/ +def 𝔗₁ (k n j : β„•) (u : 𝔓 X) : Set (𝔓 X) := + { p ∈ ℭ₁ k n j | π“˜ p β‰  π“˜ u ∧ smul 2 p ≀ smul 1 u } + +/-- The subset `π”˜β‚‚(k, n, j)` of `π”˜β‚(k, n, j)`, given in (5.4.2). -/ +def π”˜β‚‚ (k n j : β„•) : Set (𝔓 X) := + { u ∈ π”˜β‚ k n j | Β¬ Disjoint (𝔗₁ k n j u) (ℭ₆ k n j) } + +/-- The relation `∼` defined below (5.4.2). It is an equivalence relation on `π”˜β‚‚ k n j`. -/ +def URel (k n j : β„•) (u u' : 𝔓 X) : Prop := + u = u' ∨ βˆƒ p ∈ 𝔗₁ k n j u, smul 10 p ≀ smul 1 u' + +nonrec lemma URel.rfl : URel k n j u u := Or.inl rfl + +/-- Lemma 5.4.1, part 1. -/ +lemma URel.eq (hu : u ∈ π”˜β‚‚ k n j) (hu' : u' ∈ π”˜β‚‚ k n j) (huu' : URel k n j u u') : + π“˜ u = π“˜ u' := sorry + +/-- Lemma 5.4.1, part 2. -/ +lemma URel.not_disjoint (hu : u ∈ π”˜β‚‚ k n j) (hu' : u' ∈ π”˜β‚‚ k n j) (huu' : URel k n j u u') : + Β¬ Disjoint (ball_(u) (𝒬 u) 100) (ball_(u') (𝒬 u') 100) := sorry + +/-- Lemma 5.4.2. -/ +lemma equivalenceOn_urel : EquivalenceOn (URel (X := X) k n j) (π”˜β‚‚ k n j) where + refl := fun x _ ↦ .rfl + symm := sorry + trans := sorry + +/-- `π”˜β‚ƒ(k, n, j) βŠ† π”˜β‚‚ k n j` is an arbitary set of representatives of `URel` on `π”˜β‚‚ k n j`, +given above (5.4.5). -/ +def π”˜β‚ƒ (k n j : β„•) : Set (𝔓 X) := + (equivalenceOn_urel (k := k) (n := n) (j := j)).reprs + +/-- The subset `𝔗₂(u)` of `ℭ₆(k, n, j)`, given in (5.4.5). +In lemmas, we will assume `u ∈ π”˜β‚ƒ k n l` -/ +def 𝔗₂ (k n j : β„•) (u : 𝔓 X) : Set (𝔓 X) := + ℭ₆ k n j ∩ ⋃ (u' ∈ π”˜β‚‚ k n j) (_ : URel k n j u u'), 𝔗₁ k n j u' + +lemma 𝔗₂_subset_ℭ₆ : 𝔗₂ k n j u βŠ† ℭ₆ k n j := inter_subset_left .. + +/-- Lemma 5.4.3 -/ +lemma C6_forest : ℭ₆ (X := X) k n j = ⋃ u ∈ π”˜β‚ƒ k n j, 𝔗₂ k n j u := by + sorry + +/- Lemma 5.4.4 seems to be a duplicate of Lemma 5.4.6. +The numberings below might change once we remove Lemma 5.4.4 -/ + +/-- Lemma 5.4.5, verifying (2.0.32) -/ +lemma forest_geometry (hu : u ∈ π”˜β‚ƒ k n j) (hp : p ∈ 𝔗₂ k n j u) : smul 4 p ≀ smul 1 u := by + sorry + +/-- Lemma 5.4.6, verifying (2.0.33) -/ +lemma forest_convex (hu : u ∈ π”˜β‚ƒ k n j) : OrdConnected (𝔗₂ k n j u) := by + sorry + +/-- Lemma 5.4.7, verifying (2.0.36) +Note: swapped `u` and `u'` to match (2.0.36) -/ +lemma forest_separation (hu : u ∈ π”˜β‚ƒ k n j) (hu' : u' ∈ π”˜β‚ƒ k n j) (huu' : u β‰  u') + (hp : p ∈ 𝔗₂ k n j u') (h : π“˜ p ≀ π“˜ u) : 2 ^ (Z * (n + 1)) < dist_(p) (𝒬 p) (𝒬 u) := by + sorry + +/-- Lemma 5.4.8, verifying (2.0.37) -/ +lemma forest_inner (hu : u ∈ π”˜β‚ƒ k n j) (hp : p ∈ 𝔗₂ k n j u') : + ball (𝔠 p) (8 * D ^ 𝔰 p) βŠ† π“˜ u := by + sorry + +def C5_4_8 (n : β„•) : β„• := 1 + (4 * n + 12) * 2 ^ n + +/-- Lemma 5.4.8, used to verify that π”˜β‚„ satisfies 2.0.34. -/ +lemma forest_stacking (x : X) : stackSize (π”˜β‚ƒ (X := X) k n j) x ≀ C5_4_8 n := by + sorry + +/-- Pick a maximal subset of `s` satisfying `βˆ€ x, stackSize s x ≀ 2 ^ n` -/ +def auxπ”˜β‚„ (s : Set (𝔓 X)) : Set (𝔓 X) := by + revert s; sorry + +/-- The sets `(π”˜β‚„(k, n, j, l))_l` form a partition of `π”˜β‚ƒ k n j`. -/ +def π”˜β‚„ (k n j l : β„•) : Set (𝔓 X) := + auxπ”˜β‚„ <| π”˜β‚ƒ k n j \ ⋃ (l' < l), π”˜β‚„ k n j l' + +lemma iUnion_π”˜β‚„ : ⋃ l, π”˜β‚„ (X := X) k n j l = π”˜β‚ƒ k n j := by + sorry + +lemma π”˜β‚„_subset_π”˜β‚ƒ : π”˜β‚„ (X := X) k n j l βŠ† π”˜β‚ƒ k n j := by + sorry + +lemma le_of_nonempty_π”˜β‚„ (h : (π”˜β‚„ (X := X) k n j l).Nonempty) : l < 4 * n + 13 := by + sorry + +lemma pairwiseDisjoint_π”˜β‚„ : univ.PairwiseDisjoint (π”˜β‚„ (X := X) k n j) := by + sorry + +lemma stackSize_π”˜β‚„_le (x : X) : stackSize (π”˜β‚„ (X := X) k n j l) x ≀ 2 ^ n := by + sorry + +open TileStructure +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 <| π”˜β‚„_subset_π”˜β‚ƒ hu + π“˜_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 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 @@ -628,8 +736,8 @@ lemma forest_union {f : X β†’ β„‚} (hf : βˆ€ x, β€–f xβ€– ≀ F.indicator 1 x) : C5_1_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ := by sorry - /-- The constant used in Lemma 5.1.3, with value `2 ^ (210 * a ^ 3) / (q - 1) ^ 5` -/ +-- todo: redefine in terms of other constants 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 @@ -639,19 +747,31 @@ lemma forest_complement {f : X β†’ β„‚} (hf : βˆ€ x, β€–f xβ€– ≀ F.indicator 1 C5_1_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ := by sorry +/-! ## Section 5.5 and Lemma 5.1.3 -/ -/-! 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`. -/ +/-- The set 𝔓_{G\G'} in the blueprint -/ +def 𝔓pos : Set (𝔓 X) := { p : 𝔓 X | 0 < volume (π“˜ p ∩ G ∩ G'ᢜ) } --- /-- `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 +/-- The union occurring in the statement of Lemma 5.5.1 containing 𝔏₀ -/ +def β„œβ‚€ : Set (𝔓 X) := 𝔓pos ∩ ⋃ (n : β„•) (k ≀ n), 𝔏₀ k n + +/-- The union occurring in the statement of Lemma 5.5.1 containing 𝔏₁ -/ +def β„œβ‚ : Set (𝔓 X) := 𝔓pos ∩ ⋃ (n : β„•) (k ≀ n) (j ≀ 2 * n + 3) (l ≀ Z * (n + 1)), 𝔏₁ k n j l + +/-- The union occurring in the statement of Lemma 5.5.1 containing 𝔏₂ -/ +def β„œβ‚‚ : Set (𝔓 X) := 𝔓pos ∩ ⋃ (n : β„•) (k ≀ n) (j ≀ 2 * n + 3), 𝔏₂ k n j + +/-- The union occurring in the statement of Lemma 5.5.1 containing 𝔏₃ -/ +def β„œβ‚ƒ : Set (𝔓 X) := 𝔓pos ∩ ⋃ (n : β„•) (k ≀ n) (j ≀ 2 * n + 3) (l ≀ Z * (n + 1)), 𝔏₃ k n j l + +/-- Lemma 5.5.1 -/ +lemma antichain_decomposition : 𝔓pos (X := X) ∩ π”“β‚αΆœ = β„œβ‚€ βˆͺ β„œβ‚ βˆͺ β„œβ‚‚ βˆͺ β„œβ‚ƒ := by + sorry /-- The constant used in Proposition 2.0.2, which has value `2 ^ (440 * a ^ 3) / (q - 1) ^ 5` in the blueprint. -/ +-- todo: redefine in terms of other constants def C2_0_2 (a : ℝ) (q : ℝβ‰₯0) : ℝβ‰₯0 := C5_1_2 a q + C5_1_3 a q lemma C2_0_2_pos : C2_0_2 a nnq > 0 := sorry diff --git a/Carleson/Forest.lean b/Carleson/Forest.lean index 2da0e7f9..8f5f9ddc 100644 --- a/Carleson/Forest.lean +++ b/Carleson/Forest.lean @@ -1,6 +1,6 @@ import Carleson.TileStructure -open Set MeasureTheory Metric Function Complex Bornology +open Set MeasureTheory Metric Function Complex Bornology Classical open scoped NNReal ENNReal ComplexConjugate noncomputable section @@ -8,32 +8,69 @@ 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} + {C C' : Set (𝔓 X)} {x x' : X} -namespace TileStructure -variable (X) in -structure Tree where - carrier : Finset (𝔓 X) - nonempty : Nonempty (𝔓 X) - ordConnected : OrdConnected (carrier : Set (𝔓 X)) +/-- The number of tiles `p` in `s` whose underlying cube `π“˜ p` contains `x`. -/ +def stackSize (C : Set (𝔓 X)) (x : X) : β„• := + βˆ‘ p ∈ Finset.univ.filter (Β· ∈ 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 : C = C') (h2 : βˆ€ p ∈ C, x ∈ (π“˜ p : Set X) ↔ x' ∈ (π“˜ p : Set X)) : + stackSize C x = stackSize C' x' := by + subst h + refine Finset.sum_congr rfl fun p hp ↦ ?_ + simp_rw [Finset.mem_filter, Finset.mem_univ, true_and] at hp + simp_rw [indicator, h2 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)] -attribute [coe] Tree.carrier -instance : CoeTC (Tree X) (Finset (𝔓 X)) where coe := Tree.carrier -instance : CoeTC (Tree X) (Set (𝔓 X)) where coe p := ((p : Finset (𝔓 X)) : Set (𝔓 X)) -instance : Membership (𝔓 X) (Tree X) := ⟨fun x p => x ∈ (p : Set _)⟩ -instance : Preorder (Tree X) := Preorder.lift Tree.carrier +/-! 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 +-- carrier : Set (𝔓 X) +-- nonempty : Nonempty carrier +-- ordConnected : OrdConnected carrier -- (2.0.33) + +-- attribute [coe] Tree.carrier +-- instance : CoeTC (Tree X) (Set (𝔓 X)) where coe := Tree.carrier +-- -- instance : CoeTC (Tree X) (Finset (𝔓 X)) where coe := Tree.carrier +-- -- instance : CoeTC (Tree X) (Set (𝔓 X)) where coe p := ((p : Finset (𝔓 X)) : Set (𝔓 X)) +-- instance : Membership (𝔓 X) (Tree X) := ⟨fun x p => x ∈ (p : Set _)⟩ +-- instance : Preorder (Tree X) := Preorder.lift Tree.carrier variable (X) in /-- An `n`-forest -/ structure Forest (n : β„•) where - π”˜ : Finset (𝔓 X) - 𝔗 : 𝔓 X β†’ Tree X -- Is it a problem that we totalized this function? + π”˜ : 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 - essSup_tsum_le : snorm (βˆ‘ u ∈ π”˜, (π“˜ u : Set X).indicator (1 : X β†’ ℝ)) ∞ volume ≀ 2 ^ n - dens₁_𝔗_le {u} (hu : u ∈ π”˜) : dens₁ (𝔗 u : Set (𝔓 X)) ≀ 2 ^ (4 * a + 1 - n) + 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') - (h : π“˜ p ≀ π“˜ u) : 2 ^ (Z * (n + 1)) < dist_(p) (𝒬 p) (𝒬 u) - ball_subset {u} (hu : u ∈ π”˜) {p} (hp : p ∈ 𝔗 u) : ball (𝔠 p) (8 * D ^ 𝔰 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 diff --git a/Carleson/ForestOperator.lean b/Carleson/ForestOperator.lean index 95aedd16..ad97ebba 100644 --- a/Carleson/ForestOperator.lean +++ b/Carleson/ForestOperator.lean @@ -6,7 +6,7 @@ variable {X : Type*} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X noncomputable section -open Set MeasureTheory Metric Function Complex Bornology TileStructure +open Set MeasureTheory Metric Function Complex Bornology TileStructure Classical open scoped NNReal ENNReal ComplexConjugate def C2_0_4 (a q : ℝ) (n : β„•) : ℝβ‰₯0 := 2 ^ (432 * a ^ 3 - (q - 1) / q * n) @@ -14,7 +14,8 @@ def C2_0_4 (a q : ℝ) (n : β„•) : ℝβ‰₯0 := 2 ^ (432 * a ^ 3 - (q - 1) / q * n theorem forest_operator {n : β„•} (𝔉 : Forest X n) {f g : X β†’ β„‚} (hf : Measurable f) (h2f : βˆ€ x, β€–f xβ€– ≀ F.indicator 1 x) (hg : Measurable g) (h2g : IsBounded (support g)) : - β€–βˆ« x, conj (g x) * βˆ‘ u ∈ 𝔉.π”˜, βˆ‘ p ∈ 𝔉.𝔗 u, T p f xβ€–β‚Š ≀ + β€–βˆ« x, conj (g x) * βˆ‘ u ∈ Finset.univ.filter (Β· ∈ 𝔉.π”˜), + βˆ‘ p ∈ Finset.univ.filter (Β· ∈ 𝔉.𝔗 u), T p f xβ€–β‚Š ≀ C2_0_4 a q n * (densβ‚‚ (X := X) (⋃ u ∈ 𝔉.π”˜, 𝔉.𝔗 u)) ^ (q⁻¹ - 2⁻¹) * snorm f 2 volume * snorm g 2 volume := by sorry diff --git a/Carleson/ToMathlib/Misc.lean b/Carleson/ToMathlib/Misc.lean index 2c26e16a..5e87592b 100644 --- a/Carleson/ToMathlib/Misc.lean +++ b/Carleson/ToMathlib/Misc.lean @@ -108,3 +108,82 @@ lemma ENNReal.sum_geometric_two_pow_neg_two : βˆ‘' (n : β„•), (2 : ℝβ‰₯0∞) ^ (-2 * n : β„€) = ((4 : ℝ) / 3).toNNReal := by conv_lhs => enter [1, n, 2]; rw [← Nat.cast_two] rw [ENNReal.sum_geometric_two_pow_toNNReal zero_lt_two]; norm_num + +/-! ## `EquivalenceOn` -/ + +/-- An equivalence relation on the set `s`. -/ +structure EquivalenceOn {Ξ± : Type*} (r : Ξ± β†’ Ξ± β†’ Prop) (s : Set Ξ±) : Prop where + /-- An equivalence relation is reflexive: `x ~ x` -/ + refl : βˆ€ x ∈ s, r x x + /-- An equivalence relation is symmetric: `x ~ y` implies `y ~ x` -/ + symm : βˆ€ {x y}, x ∈ s β†’ y ∈ s β†’ r x y β†’ r y x + /-- An equivalence relation is transitive: `x ~ y` and `y ~ z` implies `x ~ z` -/ + trans : βˆ€ {x y z}, x ∈ s β†’ y ∈ s β†’ z ∈ s β†’ r x y β†’ r y z β†’ r x z + + +namespace EquivalenceOn + +variable {Ξ± : Type*} {r : Ξ± β†’ Ξ± β†’ Prop} {s : Set Ξ±} {hr : EquivalenceOn r s} {x y : Ξ±} + +variable (hr) in +protected def setoid : Setoid s where + r x y := r x y + iseqv := { + refl := fun x ↦ hr.refl x x.2 + symm := fun {x y} ↦ hr.symm x.2 y.2 + trans := fun {x y z} ↦ hr.trans x.2 y.2 z.2 + } + +lemma exists_rep (x : Ξ±) : βˆƒ y, x ∈ s β†’ y ∈ s ∧ r x y := + ⟨x, fun hx ↦ ⟨hx, hr.refl x hx⟩⟩ + +open Classical in +variable (hr) in +/-- An arbitrary representative of `x` w.r.t. the equivalence relation `r`. -/ +protected noncomputable def out (x : Ξ±) : Ξ± := + if hx : x ∈ s then (Quotient.out (s := hr.setoid) ⟦⟨x, hx⟩⟧ : s) else x + +lemma out_mem (hx : x ∈ s) : hr.out x ∈ s := by + rw [EquivalenceOn.out, dif_pos hx] + apply Subtype.prop + +@[simp] +lemma out_mem_iff : hr.out x ∈ s ↔ x ∈ s := by + refine ⟨fun h ↦ ?_, out_mem⟩ + by_contra hx + rw [EquivalenceOn.out, dif_neg hx] at h + exact hx h + +lemma out_rel (hx : x ∈ s) : r (hr.out x) x := by + rw [EquivalenceOn.out, dif_pos hx] + exact @Quotient.mk_out _ (hr.setoid) ⟨x, hx⟩ + +lemma rel_out (hx : x ∈ s) : r x (hr.out x) := hr.symm (out_mem hx) hx (out_rel hx) + +lemma out_inj (hx : x ∈ s) (hy : y ∈ s) (h : r x y) : hr.out x = hr.out y := by + simp_rw [EquivalenceOn.out, dif_pos hx, dif_pos hy] + congr 1 + simp_rw [Quotient.out_inj, Quotient.eq] + exact h + +lemma out_inj' (hx : x ∈ s) (hy : y ∈ s) (h : r (hr.out x) (hr.out y)) : hr.out x = hr.out y := by + apply out_inj hx hy + refine' hr.trans hx _ hy (rel_out hx) <| hr.trans _ _ hy h <| out_rel hy + all_goals simpa + +variable (hr) in +/-- The set of representatives. -/ +def reprs : Set Ξ± := hr.out '' s + +lemma out_mem_reprs (hx : x ∈ s) : hr.out x ∈ hr.reprs := ⟨x, hx, rfl⟩ + +lemma reprs_subset : hr.reprs βŠ† s := by + rintro _ ⟨x, hx, rfl⟩ + exact out_mem hx + +lemma reprs_inj (hx : x ∈ hr.reprs) (hy : y ∈ hr.reprs) (h : r x y) : x = y := by + obtain ⟨x, hx, rfl⟩ := hx + obtain ⟨y, hy, rfl⟩ := hy + exact out_inj' hx hy h + +end EquivalenceOn diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index 1938086e..56afb1cd 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -2718,6 +2718,8 @@ \section{Proof of the Forest Union Lemma} \begin{lemma}[relation geometry] \label{relation-geometry} + \leanok + \lean{URel.eq, URel.not_disjoint} \uses{wiggle-order-3} If $\fu \sim \fu'$, then $\scI(u) = \scI(u')$ and \begin{equation*} @@ -2750,6 +2752,8 @@ \section{Proof of the Forest Union Lemma} \begin{lemma}[equivalence relation] \label{equivalence-relation} \uses{relation-geometry} +\leanok +\lean{equivalenceOn_urel} For each $k,n,j$, the relation $\sim$ on $\fU_2(k,n,j)$ is an equivalence relation. \end{lemma} @@ -2813,6 +2817,8 @@ \section{Proof of the Forest Union Lemma} \begin{lemma}[C6 forest] \label{C6-forest} +\leanok +\lean{C6_forest} \uses{equivalence-relation} We have \begin{equation} @@ -2824,7 +2830,7 @@ \section{Proof of the Forest Union Lemma} By \eqref{eq-C4-def} and \eqref{defc5}, we have $\fp \in \fC_3(k,n,j)$. By \eqref{eq-L2-def} and \eqref{eq-C3-def}, there exists $\fu \in \fU_1(k,n,j)$ with $2\fp \lesssim \fu$ and $\scI(\fp) \ne \scI(\fu)$, that is, with $\fp \in \mathfrak{T}_1(\fu)$. Then $\mathfrak{T}_1(\fu)$ is clearly nonempty, so $\fu \in \fU_2(k,n,j)$. By the definition of $\fU_3(k,n,j)$, there exists $\fu' \in \fU_3(k,n,j)$ with $\fu \sim \fu'$. By \eqref{definesv}, we have $\fp \in \mathfrak{T}_2(\fu')$. \end{proof} -\begin{lemma}[C6 convex] +\begin{lemma}[C6 convex] %% TODO: delete, duplicate of forest-convex \label{C6-convex} \uses{C5-convex} Let $\fu \in \fU_3(k,n,j)$. If $\fp \le \fp' \le \fp''$ and $\fp, \fp'' \in \mathfrak{T}_2(\fu)$, then $\fp' \in \mathfrak{T}_2(\fu)$. @@ -2839,6 +2845,8 @@ \section{Proof of the Forest Union Lemma} \begin{lemma}[forest geometry] \label{forest-geometry} \uses{relation-geometry} + \leanok + \lean{forest_geometry} For each $\fu\in \fU_3(k,n,j)$, the set $\mathfrak{T}_2(\fu)$ satisfies \eqref{forest1}. @@ -2863,6 +2871,8 @@ \section{Proof of the Forest Union Lemma} \begin{lemma}[forest convex] \label{forest-convex} \uses{C6-convex} + \leanok + \lean{forest_convex} For each $\fu\in \fU_3(k,n,j)$, the set $\mathfrak{T}_2(\fu)$ satisfies the convexity condition \eqref{forest2}. @@ -2879,6 +2889,8 @@ \section{Proof of the Forest Union Lemma} \begin{lemma}[forest separation] \label{forest-separation} \uses{monotone-cube-metrics} + \leanok + \lean{forest_separation} For each $\fu,\fu'\in \fU_3(k,n,j)$ with $\fu\neq \fu'$ and each $\fp \in \fT_2(\fu)$ with $\scI(\fp)\subset \scI(\fu')$ we have \begin{equation} @@ -2907,6 +2919,8 @@ \section{Proof of the Forest Union Lemma} \begin{lemma}[forest inner] \label{forest-inner} \uses{relation-geometry} + \leanok + \lean{forest_inner} For each $\fu\in \fU_3(k,n,j)$ and each $\fp \in \mathfrak{T}_2(\fu)$ we have @@ -2933,6 +2947,8 @@ \section{Proof of the Forest Union Lemma} \begin{lemma}[forest stacking] \label{forest-stacking} + \leanok + \lean{forest_stacking} It holds that \begin{equation} \sum_{\fu \in \fU_3(k,n,j)} \mathbf{1}_{\scI(\fu)} \le 1 + (4n+12)2^{n}\,. @@ -2992,7 +3008,9 @@ \section{Proof of the Forest Complement Lemma} Define $\fP_{G \setminus G'}$ to be the set of all $\fp \in \fP$ such that $\mu(\scI(\fp) \cap (G \setminus G')) > 0$. \begin{lemma}[antichain decomposition] -\label{antichain-decomposition} + \label{antichain-decomposition} + \leanok + \lean{antichain_decomposition} We have that \begin{align} \label{eq-fp'-decomposition}