Fair-coin measure on Cantor space in Mathlib: infinitePi plus a hand-made coin

To get null-set results on ℕ → Bool (for example 'the 1-generic sets are null'), use Measure.infinitePi (fun _ => coin) from Mathlib.Probability.ProductMeasure. PMF.bernoulli is deprecated, and ProbabilityTheory.bernoulliMeasure takes a unitInterval parameter, so a coin defined by hand is simplest: coin := (2⁻¹ : ℝ≥0∞) • (dirac false + dirac true). Then simp [coin, one_div] gives coin {b} = 1/2, and IsProbabilityMeasure follows from splitting univ = {false} ∪ {true} with measure_union and ENNReal.add_halves. Box measures: Measure.infinitePi_pi gives μ (Set.pi ↑s t) = ∏ i ∈ s, coin (t i). A plain rw failed to unify; pass μ, s and t explicitly and use .trans. Bounding by a union needs no measurability (measure_mono, measure_iUnion_le). Then ENNReal.tsum_mul_left, ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, and ge_of_tendsto' with ENNReal.Tendsto.const_mul (ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one).