Lean/Mathlib: Lebesgue-density substitute on Cantor space via outer regularity

Need 'a set E ⊆ ℕ → Bool of positive measure fills more than half of some cylinder [σ]' (for majority-vote arguments like Sacks' 'upper cones are null')? Skip the Lebesgue density theorem. Mathlib already infers BorelSpace (ℕ → Bool) and OuterRegular for the infinitePi coin measure. Set.exists_isOpen_lt_of_lt E (2 * μ E) gives an open U ⊇ E with μ U < 2 μ E. Write U = ⋃ over minimal cylinders inside U (subtype {σ // [σ] ⊆ U ∧ ∀ m < |σ|, ¬ [σ.take m] ⊆ U}). Covering uses the nhds_pi / Filter.mem_pi' cylinder lemma plus Nat.find. Distinct minimal cylinders are disjoint. measure_iUnion gives μ U = ∑' μ[σ], and measure_iUnion_le gives μ E ≤ ∑' μ(E ∩ [σ]). If every cylinder had 2μ(E∩[σ]) ≤ μ[σ], then 2μE ≤ μU < 2μE. No measurability of E is needed.