Source indexedlemma · leanprover/lean4:v4.32.0

cover_by_cubes

Carleson.TileExistence · Carleson/TileExistence.lean:653 to 668

Mathematical statement

Exact Lean statement

lemma cover_by_cubes {l : ℤ} (hl : -S ≤ l) :
    ∀ {k : ℤ}, l ≤ k → (hk : -S ≤ k) → ∀ y, I3 hk y ⊆ ⋃ (yl : Yk X l), I3 hl yl

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cover_by_cubes {l : ℤ} (hl : -S ≤ l) :    ∀ {k : ℤ}, l ≤ k → (hk : -S ≤ k) → ∀ y, I3 hk y ⊆ ⋃ (yl : Yk X l), I3 hl yl := by  apply Int.leInduction  · intro _ y x hx    rw [mem_iUnion]    use y  intro k hlk hind  rw [← add_sub_cancel_right k 1] at hind  intro hk1 y x hx  have h : -S < k + 1 := by linarith  have : x ∈ I2 hk1 y := I3_subset_I2 hk1 y hx  rw [I2, dif_neg h.ne'] at this  push _ ∈ _ at this  obtain ⟨z, _, hz'⟩ := this  specialize hind (I_induction_proof hk1 h.ne') z hz'  exact hind