Source indexedlemma · leanprover/lean4:v4.32.0

I1_measurableSet

Carleson.TileExistence · Carleson/TileExistence.lean:354 to 364

Mathematical statement

Exact Lean statement

lemma I1_measurableSet {k : ℤ} (hk : -S ≤ k) (y : Yk X k) : MeasurableSet (I1 hk y)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma I1_measurableSet {k : ℤ} (hk : -S ≤ k) (y : Yk X k) : MeasurableSet (I1 hk y) := by    by_cases hk_s : k = -S    · rw [I1, dif_pos hk_s]      exact measurableSet_ball    · let hk'' : -S < k := lt_of_le_of_ne hk fun a_1 ↦ hk_s (id a_1.symm)      have h1: 0 ≤ S + (k - 1) := by linarith      rw [I1, dif_neg hk_s]      letI := (Yk_countable X (k - 1)).to_subtype      refine MeasurableSet.biUnion (to_countable (Yk X (k - 1) ↓∩ ball y (D ^ k))) ?_      simp only [mem_preimage]      exact fun b _ ↦ I3_measurableSet (I_induction_proof hk hk_s) b