Source indexedlemma · leanprover/lean4:v4.32.0

transitive_boundary

Carleson.TileExistence · Carleson/TileExistence.lean:885 to 903

Mathematical statement

Exact Lean statement

lemma transitive_boundary {k1 k2 k3 : ℤ} (hk1 : -S ≤ k1) (hk2 : -S ≤ k2) (hk3 : -S ≤ k3)
  (hk1_2 : k1 ≤ k2) (hk2_3 : k2 ≤ k3) (y1 : Yk X k1) (y2 : Yk X k2) (y3 : Yk X k3)
    (x : X) (hx : x ∈ I3 hk1 y1 ∩ I3 hk2 y2 ∩ I3 hk3 y3) :
    clProp(hk1,y1|hk3,y3) → (clProp(hk1,y1|hk2,y2) ∧ clProp(hk2,y2|hk3,y3))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma transitive_boundary {k1 k2 k3 : ℤ} (hk1 : -S ≤ k1) (hk2 : -S ≤ k2) (hk3 : -S ≤ k3)  (hk1_2 : k1 ≤ k2) (hk2_3 : k2 ≤ k3) (y1 : Yk X k1) (y2 : Yk X k2) (y3 : Yk X k3)    (x : X) (hx : x ∈ I3 hk1 y1 ∩ I3 hk2 y2 ∩ I3 hk3 y3) :    clProp(hk1,y1|hk3,y3) → (clProp(hk1,y1|hk2,y2) ∧ clProp(hk2,y2|hk3,y3)) := by  by_cases hk1_eq_2 : k1 = k2  · subst hk1_eq_2    intro hcl    have : y1 = y2 := by apply I3_prop_1; exact hx.left    subst this    constructor    · exact ⟨le_refl _,by        obtain hx := hcl.I3_infdist_lt        apply lt_of_le_of_lt _ hx        apply Metric.infEDist_anti        simp only [compl_subset_compl]        exact hcl.I3_subset⟩    exact hcl  · have : k1 < k2 := lt_of_le_of_ne hk1_2 hk1_eq_2    exact transitive_boundary' hk1 hk2 hk3 this hk2_3 y1 y2 y3 x hx