diff --git a/Carleson/Discrete/Defs.lean b/Carleson/Discrete/Defs.lean index a898c489..34218830 100644 --- a/Carleson/Discrete/Defs.lean +++ b/Carleson/Discrete/Defs.lean @@ -21,6 +21,16 @@ def 𝓒 (k : β„•) : Set (Grid X) := /-- The definition `𝔓(k)` given in (5.1.3). -/ def TilesAt (k : β„•) : Set (𝔓 X) := π“˜ ⁻¹' 𝓒 k +lemma disjoint_TilesAt_of_ne {m n : β„•} (h : m β‰  n) : Disjoint (TilesAt (X := X) m) (TilesAt n) := by + wlog hl : m < n generalizing m n; Β· exact (this h.symm (by omega)).symm + by_contra! h; rw [not_disjoint_iff] at h; obtain ⟨p, mp₁, mpβ‚‚βŸ© := h + simp_rw [TilesAt, mem_preimage, 𝓒, mem_diff, aux𝓒, mem_setOf] at mp₁ mpβ‚‚ + apply absurd _ mpβ‚‚.2; obtain ⟨j, lj, vj⟩ := mp₁.1; use j, lj; apply lt_of_le_of_lt _ vj + exact mul_le_mul_right' (ENNReal.zpow_le_of_le one_le_two (by omega)) _ + +lemma pairwiseDisjoint_TilesAt : univ.PairwiseDisjoint (TilesAt (X := X)) := fun _ _ _ _ ↦ + disjoint_TilesAt_of_ne + def aux𝔐 (k n : β„•) : Set (𝔓 X) := {p ∈ TilesAt k | 2 ^ (-n : β„€) * volume (π“˜ p : Set X) < volume (E₁ p) } @@ -46,6 +56,21 @@ def β„­ (k n : β„•) : Set (𝔓 X) := lemma β„­_subset_TilesAt {k n : β„•} : β„­ k n βŠ† TilesAt (X := X) k := fun t mt ↦ by rw [β„­, mem_setOf] at mt; exact mt.1 +lemma disjoint_β„­_of_ne {k m n : β„•} (h : m β‰  n) : Disjoint (β„­ (X := X) k m) (β„­ k n) := by + wlog hl : m < n generalizing m n; Β· exact (this h.symm (by omega)).symm + by_contra! h; rw [not_disjoint_iff] at h; obtain ⟨p, mp₁, mpβ‚‚βŸ© := h + apply absurd _ (not_disjoint_iff.mpr ⟨_, mp₁.2, mpβ‚‚.2⟩) + rw [Ioc_disjoint_Ioc, le_max_iff]; left; rw [min_le_iff]; right + exact ENNReal.zpow_le_of_le one_le_two (by omega) + +lemma pairwiseDisjoint_β„­ : + (univ : Set (β„• Γ— β„•)).PairwiseDisjoint (fun kn ↦ β„­ (X := X) kn.1 kn.2) := + fun ⟨k₁, nβ‚βŸ© _ ⟨kβ‚‚, nβ‚‚βŸ© _ hn ↦ by + change Disjoint (β„­ k₁ n₁) (β„­ kβ‚‚ nβ‚‚) + by_cases hk : k₁ = kβ‚‚ + Β· rw [ne_eq, Prod.mk.injEq, not_and] at hn; exact hk β–Έ disjoint_β„­_of_ne (hn hk) + Β· exact disjoint_of_subset β„­_subset_TilesAt β„­_subset_TilesAt (disjoint_TilesAt_of_ne hk) + /-- The subset `𝔅(p)` of `𝔐(k, n)`, given in (5.1.8). -/ def 𝔅 (k n : β„•) (p : 𝔓 X) : Set (𝔓 X) := { m ∈ 𝔐 k n | smul 100 p ≀ smul 1 m } @@ -61,6 +86,16 @@ def ℭ₁ (k n j : β„•) : Set (𝔓 X) := lemma ℭ₁_subset_β„­ {k n j : β„•} : ℭ₁ k n j βŠ† β„­ (X := X) k n := fun t mt ↦ by rw [ℭ₁, preℭ₁, mem_diff, mem_setOf] at mt; exact mt.1.1 +lemma disjoint_ℭ₁_of_ne {k n j l : β„•} (h : j β‰  l) : Disjoint (ℭ₁ (X := X) k n j) (ℭ₁ k n l) := by + wlog hl : j < l generalizing j l; Β· exact (this h.symm (by omega)).symm + by_contra! h; rw [not_disjoint_iff] at h; obtain ⟨p, mp₁, mpβ‚‚βŸ© := h + simp_rw [ℭ₁, mem_diff, preℭ₁, mem_setOf, mp₁.1.1, true_and, not_le] at mp₁ mpβ‚‚ + have := mpβ‚‚.1.trans_lt mp₁.2 + rw [pow_lt_pow_iff_right one_lt_two] at this; omega + +lemma pairwiseDisjoint_ℭ₁ {k n : β„•} : univ.PairwiseDisjoint (ℭ₁ (X := X) k n) := fun _ _ _ _ ↦ + disjoint_ℭ₁_of_ne + lemma card_𝔅_of_mem_ℭ₁ {k n j : β„•} {p : 𝔓 X} (hp : p ∈ ℭ₁ k n j) : (𝔅 k n p).toFinset.card ∈ Ico (2 ^ j) (2 ^ (j + 1)) := by simp_rw [ℭ₁, mem_diff, preℭ₁, mem_setOf, hp.1.1, true_and, not_le] at hp @@ -130,6 +165,8 @@ is at most the least upper bound of `𝓛 n u` in `Grid X`. -/ def 𝔏₄ (k n j : β„•) : Set (𝔓 X) := { p ∈ β„­β‚„ k n j | βˆƒ u ∈ π”˜β‚ k n j, (π“˜ p : Set X) βŠ† ⋃ (i ∈ 𝓛 (X := X) n u), i } +lemma 𝔏₄_subset_β„­β‚„ {k n j : β„•} : 𝔏₄ k n j βŠ† β„­β‚„ (X := X) k n j := fun _ mu ↦ mu.1 + /-- The subset `β„­β‚…(k, n, j)` of `β„­β‚„(k, n, j)`, given in (5.1.23). -/ def β„­β‚… (k n j : β„•) : Set (𝔓 X) := β„­β‚„ k n j \ 𝔏₄ k n j @@ -142,6 +179,37 @@ lemma β„­β‚…_def {k n j : β„•} {p : 𝔓 X} : 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 +-- These inclusion and disjointness lemmas are only used in `antichain_decomposition` +section AntichainDecomp + +variable {k n j l : β„•} + +lemma 𝔏₀_subset_β„­ : 𝔏₀ (X := X) k n βŠ† β„­ k n := fun _ mu ↦ mu.1 +lemma 𝔏₀_disjoint_ℭ₁ : Disjoint (𝔏₀ (X := X) k n) (ℭ₁ k n j) := by + by_contra h; rw [not_disjoint_iff] at h; obtain ⟨p, ⟨_, b0⟩, ⟨⟨_, bp⟩ , _⟩⟩ := h + simp [filter_mem_univ_eq_toFinset, b0] at bp + +lemma 𝔏₁_subset_ℭ₁ : 𝔏₁ (X := X) k n j l βŠ† ℭ₁ k n j := minLayer_subset +lemma 𝔏₁_subset_β„­ : 𝔏₁ (X := X) k n j l βŠ† β„­ k n := minLayer_subset.trans ℭ₁_subset_β„­ + +lemma 𝔏₂_subset_ℭ₁ : 𝔏₂ k n j βŠ† ℭ₁ (X := X) k n j := 𝔏₂_subset_β„­β‚‚.trans β„­β‚‚_subset_ℭ₁ +lemma 𝔏₂_subset_β„­ : 𝔏₂ k n j βŠ† β„­ (X := X) k n := 𝔏₂_subset_ℭ₁.trans ℭ₁_subset_β„­ +lemma 𝔏₂_disjoint_ℭ₃ : Disjoint (𝔏₂ (X := X) k n j) (ℭ₃ k n j) := disjoint_sdiff_right + +lemma 𝔏₃_subset_ℭ₁ : 𝔏₃ k n j l βŠ† ℭ₁ (X := X) k n j := + maxLayer_subset.trans ℭ₃_subset_β„­β‚‚ |>.trans β„­β‚‚_subset_ℭ₁ +lemma 𝔏₃_subset_β„­ : 𝔏₃ k n j l βŠ† β„­ (X := X) k n := 𝔏₃_subset_ℭ₁.trans ℭ₁_subset_β„­ + +lemma 𝔏₄_subset_ℭ₁ : 𝔏₄ k n j βŠ† ℭ₁ (X := X) k n j := + 𝔏₄_subset_β„­β‚„.trans β„­β‚„_subset_ℭ₃ |>.trans ℭ₃_subset_β„­β‚‚ |>.trans β„­β‚‚_subset_ℭ₁ +lemma 𝔏₄_subset_β„­ : 𝔏₄ k n j βŠ† β„­ (X := X) k n := 𝔏₄_subset_ℭ₁.trans ℭ₁_subset_β„­ + +lemma β„­β‚…_subset_ℭ₁ : β„­β‚… k n j βŠ† ℭ₁ (X := X) k n j := + β„­β‚…_subset_β„­β‚„.trans β„­β‚„_subset_ℭ₃ |>.trans ℭ₃_subset_β„­β‚‚ |>.trans β„­β‚‚_subset_ℭ₁ +lemma β„­β‚…_subset_β„­ : β„­β‚… k n j βŠ† β„­ (X := X) k n := β„­β‚…_subset_ℭ₁.trans ℭ₁_subset_β„­ + +end AntichainDecomp + /-- The set $\mathcal{P}_{F,G}$, defined in (5.1.24). -/ def highDensityTiles : Set (𝔓 X) := { p : 𝔓 X | 2 ^ (2 * a + 5) * volume F / volume G < densβ‚‚ {p} } diff --git a/Carleson/Discrete/Forests.lean b/Carleson/Discrete/Forests.lean index 80f89116..a12dc8eb 100644 --- a/Carleson/Discrete/Forests.lean +++ b/Carleson/Discrete/Forests.lean @@ -143,9 +143,7 @@ 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_β„­ +lemma ℭ₆_subset_β„­ : ℭ₆ (X := X) k n j βŠ† β„­ k n := ℭ₆_subset_β„­β‚….trans β„­β‚…_subset_β„­ /-- The subset `𝔗₁(u)` of `ℭ₁(k, n, j)`, given in (5.4.1). In lemmas, we will assume `u ∈ π”˜β‚ k n l` -/ @@ -775,35 +773,81 @@ def β„œβ‚‚ : Set (𝔓 X) := 𝔓pos ∩ ⋃ (n : β„•) (k ≀ n) (j ≀ 2 * 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 +lemma mem_iUnion_iff_mem_of_mem_β„­ {f : β„• β†’ β„• β†’ Set (𝔓 X)} (hp : p ∈ β„­ k n ∧ k ≀ n) + (hf : βˆ€ k n, f k n βŠ† β„­ k n) : p ∈ ⋃ (n : β„•) (k ≀ n), f k n ↔ p ∈ f k n := by + simp_rw [mem_iUnion]; constructor <;> intro h + Β· obtain ⟨n', k', _, mp⟩ := h + have e := pairwiseDisjoint_β„­ (X := X).elim (mem_univ (k, n)) (mem_univ (k', n')) + (not_disjoint_iff.mpr ⟨p, hp.1, hf k' n' mp⟩) + rw [Prod.mk.inj_iff] at e + exact e.1 β–Έ e.2 β–Έ mp + Β· use n, k, hp.2 + +lemma mem_iUnion_iff_mem_of_mem_ℭ₁ {f : β„• β†’ Set (𝔓 X)} (hp : p ∈ ℭ₁ k n j ∧ j ≀ 2 * n + 3) + (hf : βˆ€ j, f j βŠ† ℭ₁ k n j) : p ∈ ⋃ (j ≀ 2 * n + 3), f j ↔ p ∈ f j := by + simp_rw [mem_iUnion]; constructor <;> intro h + Β· obtain ⟨j', _, mp⟩ := h + have e := pairwiseDisjoint_ℭ₁ (X := X).elim (mem_univ j) (mem_univ j') + (not_disjoint_iff.mpr ⟨p, hp.1, hf j' mp⟩) + exact e β–Έ mp + Β· use j, hp.2 + /-- Lemma 5.5.1 -/ -lemma antichain_decomposition : 𝔓pos (X := X) ∩ π”“β‚αΆœ βŠ† β„œβ‚€ βˆͺ β„œβ‚ βˆͺ β„œβ‚‚ βˆͺ β„œβ‚ƒ := by - unfold β„œβ‚€ β„œβ‚ β„œβ‚‚ β„œβ‚ƒ; simp_rw [← inter_union_distrib_left]; intro p ⟨h, mp'⟩ - refine ⟨h, ?_⟩; simp_rw [mem_union, mem_iUnion, or_assoc] +lemma antichain_decomposition : 𝔓pos (X := X) ∩ π”“β‚αΆœ = β„œβ‚€ βˆͺ β„œβ‚ βˆͺ β„œβ‚‚ βˆͺ β„œβ‚ƒ := by + unfold β„œβ‚€ β„œβ‚ β„œβ‚‚ β„œβ‚ƒ 𝔓₁; simp_rw [← inter_union_distrib_left]; ext p + simp_rw [mem_inter_iff, and_congr_right_iff, mem_compl_iff, mem_union]; intro h + obtain ⟨k, n, hkn, split⟩ := exists_k_n_j_of_mem_𝔓pos h + have pc : p ∈ β„­ k n := by + rcases split with ml0 | ⟨_, _, mc1⟩ + Β· exact 𝔏₀_subset_β„­ ml0 + Β· exact ℭ₁_subset_β„­ mc1 + iterate 5 rw [mem_iUnion_iff_mem_of_mem_β„­ ⟨pc, hkn⟩] + pick_goal 5; Β· exact fun _ _ ↦ 𝔏₀_subset_β„­ + pick_goal 4; Β· exact fun _ _ ↦ iUnionβ‚‚_subset fun _ _ ↦ iUnionβ‚‚_subset fun _ _ ↦ 𝔏₁_subset_β„­ + pick_goal 3; Β· exact fun _ _ ↦ iUnionβ‚‚_subset fun _ _ ↦ 𝔏₂_subset_β„­ + pick_goal 2; Β· exact fun _ _ ↦ iUnionβ‚‚_subset fun _ _ ↦ iUnionβ‚‚_subset fun _ _ ↦ 𝔏₃_subset_β„­ + pick_goal -1; Β· exact fun _ _ ↦ iUnionβ‚‚_subset fun _ _ ↦ β„­β‚…_subset_β„­ + by_cases ml0 : p ∈ 𝔏₀ k n + Β· simp_rw [ml0, true_or, iff_true, mem_iUnionβ‚‚]; push_neg; intro j hj + exact fun a ↦ disjoint_left.mp 𝔏₀_disjoint_ℭ₁ ml0 (β„­β‚…_subset_ℭ₁ a) + simp_rw [ml0, false_or] at split ⊒ + obtain ⟨j, hj, mc1⟩ := split + iterate 4 rw [mem_iUnion_iff_mem_of_mem_ℭ₁ ⟨mc1, hj⟩] + pick_goal 4; Β· exact fun _ ↦ iUnionβ‚‚_subset fun _ _ ↦ 𝔏₁_subset_ℭ₁ + pick_goal 3; Β· exact fun _ ↦ 𝔏₂_subset_ℭ₁ + pick_goal 2; Β· exact fun _ ↦ iUnionβ‚‚_subset fun _ _ ↦ 𝔏₃_subset_ℭ₁ + pick_goal -1; Β· exact fun _ ↦ β„­β‚…_subset_ℭ₁ + by_cases mc2 : p βˆ‰ β„­β‚‚ k n j + all_goals + have mc2' := mc2 + simp_rw [β„­β‚‚, layersAbove, mem_diff, not_and, mc1, true_implies, not_not_mem] at mc2' + Β· change p ∈ ⋃ (l ≀ Z * (n + 1)), 𝔏₁ k n j l at mc2' + simp_rw [mc2', true_or, iff_true]; contrapose! mc2 + exact β„­β‚…_subset_β„­β‚„.trans β„­β‚„_subset_ℭ₃ |>.trans ℭ₃_subset_β„­β‚‚ mc2 + change p βˆ‰ ⋃ (l ≀ Z * (n + 1)), 𝔏₁ k n j l at mc2'; simp_rw [mc2', false_or] + rw [not_not_mem] at mc2; by_cases ml2 : p ∈ 𝔏₂ k n j + Β· simp_rw [ml2, true_or, iff_true] + exact fun a ↦ disjoint_left.mp 𝔏₂_disjoint_ℭ₃ ml2 (β„­β‚…_subset_β„­β‚„.trans β„­β‚„_subset_ℭ₃ a) + simp_rw [ml2, false_or] + have mc3 : p ∈ ℭ₃ k n j := ⟨mc2, ml2⟩ + by_cases mc4 : p βˆ‰ β„­β‚„ k n j + all_goals + have mc4' := mc4 + simp_rw [β„­β‚„, layersBelow, mem_diff, not_and, mc3, true_implies, not_not_mem] at mc4' + Β· change p ∈ ⋃ (l ≀ Z * (n + 1)), 𝔏₃ k n j l at mc4' + simp_rw [mc4', iff_true]; contrapose! mc4 + exact β„­β‚…_subset_β„­β‚„ mc4 + change p βˆ‰ ⋃ (l ≀ Z * (n + 1)), 𝔏₃ k n j l at mc4' + simp_rw [mc4', iff_false, β„­β‚…]; rw [not_not_mem] at mc4 ⊒; simp_rw [mem_diff, mc4, true_and] have nG₃ : Β¬(π“˜ p : Set X) βŠ† G₃ := by suffices Β¬(π“˜ p : Set X) βŠ† G' by contrapose! this; exact subset_union_of_subset_right this _ by_contra hv rw [𝔓pos, mem_setOf, inter_comm _ G'ᢜ, ← inter_assoc, ← diff_eq_compl_inter, diff_eq_empty.mpr hv] at h simp at h - obtain ⟨k, n, hkn, mp⟩ := exists_k_n_j_of_mem_𝔓pos h - rcases mp with ml0 | ⟨j, hj, mc1⟩ - Β· exact Or.inl ⟨n, k, hkn, ml0⟩ - Β· right; by_cases mc2 : p βˆ‰ β„­β‚‚ k n j - Β· simp_rw [β„­β‚‚, layersAbove, mem_diff, not_and, mc1, true_implies, not_not_mem] at mc2 - simp_rw [mem_iUnion] at mc2; obtain ⟨l, hl, f⟩ := mc2 - exact Or.inl ⟨n, k, hkn, j, hj, l, hl, f⟩ - Β· right; rw [not_not_mem] at mc2; by_cases ml2 : p ∈ 𝔏₂ k n j - Β· exact Or.inl ⟨n, k, hkn, j, hj, ml2⟩ - Β· have mc3 : p ∈ ℭ₃ k n j := ⟨mc2, ml2⟩ - right; by_cases mc4 : p βˆ‰ β„­β‚„ k n j - Β· simp_rw [β„­β‚„, layersBelow, mem_diff, not_and, mc3, true_implies, not_not_mem] at mc4 - simp_rw [mem_iUnion] at mc4; obtain ⟨l, hl, f⟩ := mc4 - exact ⟨n, k, hkn, j, hj, l, hl, f⟩ - Β· apply absurd mp'; simp_rw [mem_compl_iff, not_not_mem, 𝔓₁, mem_iUnion] - refine ⟨n, k, hkn, j, hj, not_not_mem.mp mc4, ?_⟩ - contrapose! nG₃ - exact le_iSupβ‚‚_of_le n k <| le_iSupβ‚‚_of_le hkn j <| le_iSupβ‚‚_of_le hj p <| - le_iSup_of_le nG₃ subset_rfl + contrapose! nG₃ + exact le_iSupβ‚‚_of_le n k <| le_iSupβ‚‚_of_le hkn j <| + le_iSupβ‚‚_of_le hj p <| le_iSup_of_le nG₃ subset_rfl /-- The subset `𝔏₀(k, n, l)` of `𝔏₀(k, n)`, given in Lemma 5.5.3. We use the name `𝔏₀'` in Lean. The indexing is off-by-one w.r.t. the blueprint -/ diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index 341393ca..222f707b 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -3073,7 +3073,7 @@ \section{Proof of the Forest Complement Lemma} \begin{align} \label{eq-fp'-decomposition} &\quad \fP_2 \cap \fP_{G \setminus G'}\\ - &\subset \bigcup_{k \ge 0} \bigcup_{n \ge k} \fL_0(k,n) \cap \fP_{G \setminus G'} \\ + &= \bigcup_{k \ge 0} \bigcup_{n \ge k} \fL_0(k,n) \cap \fP_{G \setminus G'} \\ &\quad\cup \bigcup_{k \ge 0} \bigcup_{n \ge k}\bigcup_{0 \le j \le 2n+3} \fL_2(k,n,j) \cap \fP_{G \setminus G'}\\ &\quad\cup \bigcup_{k \ge 0} \bigcup_{n \ge k}\bigcup_{0 \le j \le 2n+3} \bigcup_{0 \le l \le Z(n+1)} \fL_1(k,n,j,l) \cap \fP_{G \setminus G'}\\ &\quad\cup \bigcup_{k \ge 0} \bigcup_{n \ge k}\bigcup_{0 \le j \le 2n+3} \bigcup_{0 \le l \le Z(n+1)} \fL_3(k,n,j,l)\cap \fP_{G \setminus G'}\,. @@ -3086,7 +3086,7 @@ \section{Proof of the Forest Complement Lemma} Next, since $E_2(\lambda, \fp') \subset \scI(\fp')\cap G$ for every $\lambda \ge 2$ and every tile $\fp' \in \fP(k)$ with $\lambda\fp \lesssim \lambda \fp'$, it follows from \eqref{muhj2} that $\mu(E_2(\lambda, \fp')) \le 2^{-k} \mu(\scI(\fp'))$ for every such $\fp'$, so $\dens_k'(\{\fp\}) \le 2^{-k}$. Combining this with $a \ge 0$, it follows from \eqref{def-cnk} that there exists $n\ge k$ with $\fp \in \fC(k,n)$. - Since $\fp \in \fP_{G \setminus G'}$, we have in particular $\scI(\fp) \not \subset A(2n + 6, k, n)$, so there exist at most $1 + (4n + 12)2^n < 2^{2n+4}$ tiles $\mathfrak{m} \in \mathfrak{M}(k,n)$ with $\fp \le \mathfrak{m}$. It follows that $\fp \in \fL_0(k,n)$ or $\fp \in \fC_1(k,n,j)$ for some $1 \le j \le 2n + 3$. In the former case we are done, in the latter case the inclusion to be shown follows immediately from the definitions of the collections $\fC_i$ and $\fL_i$. + Since $\fp \in \fP_{G \setminus G'}$, we have in particular $\scI(\fp) \not \subset A(2n + 6, k, n)$, so there exist at most $1 + (4n + 12)2^n < 2^{2n+4}$ tiles $\mathfrak{m} \in \mathfrak{M}(k,n)$ with $\fp \le \mathfrak{m}$. It follows that $\fp \in \fL_0(k,n)$ or $\fp \in \fC_1(k,n,j)$ for some $1 \le j \le 2n + 3$. In the former case we are done, in the latter case the equality to be shown follows from the definitions of the collections $\fC_i$ and $\fL_i$ and the pairwise disjointness of the $\fC_1$. \end{proof} \begin{lemma}[L0 antichain]