Skip to main content
therefore
Sign inSign up
Open navigation
fpvandoorn/carleson
Source indexedlemma Β· leanprover/lean4:v4.32.0

antichain_decomposition

Carleson.Discrete.ForestComplement Β· Carleson/Discrete/ForestComplement.lean:250 to 286

Source documentation

Lemma 5.5.1.

We will not use the lemma in this form, as to decompose the Carleson sum it is also crucial that the union is disjoint. This is easier to formalize by decomposing into successive terms, taking advantage of disjointess at each step, instead of doing everything in one go. Still, we keep this lemma as it corresponds to the blueprint, and the key steps of its proof will also be the key steps when doing the successive decompositions.

Exact Lean statement

lemma antichain_decomposition : 𝔓pos (X := X) ∩ π”“β‚αΆœ = β„œβ‚€ βˆͺ β„œβ‚ βˆͺ β„œβ‚‚ βˆͺ β„œβ‚ƒ

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
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 Not; intros    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_sdiff, not_and, mc1, true_implies, not_notMem] 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_notMem] 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]  exact notMem_β„­β‚…_iff_mem_𝔏₃ hkn hj h mc2 ml2