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

notMem_β„­β‚…_iff_mem_𝔏₃

Carleson.Discrete.ForestComplement Β· Carleson/Discrete/ForestComplement.lean:218 to 239

Mathematical statement

Exact Lean statement

lemma notMem_β„­β‚…_iff_mem_𝔏₃ (hkn : k ≀ n) (hj : j ≀ 2 * n + 3)
    (h : p ∈ 𝔓pos) (mc2 : p ∈ β„­β‚‚ k n j) (ml2 : p βˆ‰ 𝔏₂ k n j) :
    p βˆ‰ β„­β‚… k n j ↔ p ∈ ⋃ l, ⋃ (_ : l ≀ Z * (n + 1)), 𝔏₃ k n j l

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
lemma notMem_β„­β‚…_iff_mem_𝔏₃ (hkn : k ≀ n) (hj : j ≀ 2 * n + 3)    (h : p ∈ 𝔓pos) (mc2 : p ∈ β„­β‚‚ k n j) (ml2 : p βˆ‰ 𝔏₂ k n j) :    p βˆ‰ β„­β‚… k n j ↔ p ∈ ⋃ l, ⋃ (_ : l ≀ Z * (n + 1)), 𝔏₃ k n j l := by  have mc3 : p ∈ ℭ₃ k n j := ⟨mc2, ml2⟩  by_cases mc4 : p βˆ‰ β„­β‚„ k n j  all_goals    have mc4' := mc4    simp_rw [β„­β‚„, layersBelow, mem_sdiff, not_and, mc3, true_implies, not_notMem] 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_notMem] at mc4 ⊒; simp_rw [mem_sdiff, 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, ← sdiff_eq_compl_inter,      sdiff_eq_empty.mpr hv] at h    simp at h  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