Source indexedlemma · leanprover/lean4:v4.32.0

I2_measurableSet

Carleson.TileExistence · Carleson/TileExistence.lean:367 to 376

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma I2_measurableSet {k : ℤ} (hk : -S ≤ k) (y : Yk X k) : MeasurableSet (I2 hk y) := by    by_cases hk_s : k = -S    · rw [I2, 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)      rw [I2, dif_neg hk_s]      letI := (Yk_countable X (k - 1)).to_subtype      refine MeasurableSet.biUnion (to_countable (Yk X (k - 1) ↓∩ ball (↑y) (2 * D ^ k))) ?_      · simp only [mem_preimage]        exact fun b _ ↦ I3_measurableSet (I_induction_proof hk hk_s) b