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

Antichain.Ep_inter_G_inter_Ip'_subset_E2

Carleson.Antichain.AntichainTileCount Β· Carleson/Antichain/AntichainTileCount.lean:296 to 319

Source documentation

We prove inclusion 6.3.24 for every p ∈ (𝔄_aux 𝔄 Ο‘ N) with 𝔰 p' < 𝔰 p such that (π“˜ p : Set X) ∩ (π“˜ p') β‰  βˆ…. The variable p' corresponds to 𝔭_Ο‘ in the blueprint.

Exact Lean statement

lemma Ep_inter_G_inter_Ip'_subset_E2 {𝔄 : Set (𝔓 X)} (Ο‘ : Θ X) (N : β„•) {p p' : 𝔓 X}
    (hpin : p ∈ (𝔄_aux 𝔄 Ο‘ N).toFinset) (hp' : Ο‘ ∈ ball_(p') (𝒬 p') (2 ^ (N + 1)))
    (hs : 𝔰 p' < 𝔰 p) (hπ“˜ : ((π“˜ p' : Set X) ∩ (π“˜ p)).Nonempty) :
    E p ∩ G ∩ ↑(π“˜ p') βŠ† Eβ‚‚ (2^(N + 3)) p'

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
lemma Ep_inter_G_inter_Ip'_subset_E2 {𝔄 : Set (𝔓 X)} (Ο‘ : Θ X) (N : β„•) {p p' : 𝔓 X}    (hpin : p ∈ (𝔄_aux 𝔄 Ο‘ N).toFinset) (hp' : Ο‘ ∈ ball_(p') (𝒬 p') (2 ^ (N + 1)))    (hs : 𝔰 p' < 𝔰 p) (hπ“˜ : ((π“˜ p' : Set X) ∩ (π“˜ p)).Nonempty) :    E p ∩ G ∩ ↑(π“˜ p') βŠ† Eβ‚‚ (2^(N + 3)) p' := by  have hle : π“˜ p' ≀ π“˜ p := ⟨Or.resolve_right (fundamental_dyadic (le_of_lt hs))    (not_disjoint_iff_nonempty_inter.mpr hπ“˜), le_of_lt hs⟩  -- Ineq. 6.3.22  have hΟ‘in : dist_(p) (𝒬 p) Ο‘ < ((2 : ℝ)^(N + 1)) := by    simp only [𝔄_aux, mem_Ico, sep_and, toFinset_inter, toFinset_setOf, Finset.mem_inter,      Finset.mem_filter_univ] at hpin    exact (lt_one_add (dist_(p) (𝒬 p) Ο‘)).trans hpin.2.2  -- Ineq. 6.3.23  have hsmul_le : smul (2 ^ (N + 3)) p' ≀ smul (2 ^ (N + 3)) p :=    tile_reach (le_of_lt (mem_ball'.mpr hp')) (le_of_lt hΟ‘in) hle hs  -- Ineq. 6.3.24  simp only [TileLike.le_def, smul_snd] at hsmul_le  simp only [E, Eβ‚‚, TileLike.toSet, smul_fst, smul_snd, subset_inter_iff, inter_subset_right,    true_and]  refine ⟨?_, fun _ hx ↦ ?_⟩  Β· rw [inter_assoc, inter_comm, inter_assoc]    exact inter_subset_left  Β· apply mem_of_subset_of_mem (le_trans      (le_trans subset_cball (ball_subset_ball (mod_cast Nat.one_le_two_pow)))      hsmul_le.2) hx.1.1.2.1