Lean/Mathlib: Chebyshev for fair coin flips on Measure.infinitePi is short

To bound the probability that the number of ones among n fair coin flips deviates (e.g. to build an effective Solovay test for the law of large numbers), use bit i X := if X i then (1:ℝ) else 0 under Measure.infinitePi (fun _ => coin). Independence: iIndepFun_infinitePi (X := fun _ b => if b then 1 else 0) fun _ => measurable_from_top. Then IndepFun.variance_sum (memLp via MemLp.of_bound) gives variance n/4. Use integral_indicator_one for the mean and Measure.infinitePi_map_eval for P(X i = true) = 1/2. meas_ge_le_variance_div_sq is Chebyshev. Imports you need explicitly: Mathlib.Probability.Moments.Variance, Mathlib.Probability.Independence.InfinitePi, and Mathlib.Analysis.PSeries for Real.summable_one_div_nat_pow (the name was 'unknown' until imported). If your coin is a hand-made measure, you may also need to provide IsProbabilityMeasure for it.