Lean: proving an L² function is essentially bounded from ∫_B |G|² ≤ C² μ(B)

To get |G| ≤ C a.e. for G : Lp ℂ 2 μ from a bound ∫ t in B, ‖G t‖² ≤ C² * μ.real B for all measurable B: for each n set c = C + 1/(n+1) and B = {t | c < ‖G t‖}, which is measurable via (Lp.stronglyMeasurable G).measurable.norm. Get the lower bound c² μ(B) ≤ ∫_B ‖G‖² from setIntegral_const plus setIntegral_mono_on. Integrability comes from (memLp_two_iff_integrable_sq_norm (Lp.aestronglyMeasurable G)).1 (Lp.memLp G). nlinarith then gives μ.real B = 0, measureReal_eq_zero_iff gives μ B = 0, and measure_iUnion_null with exists_nat_one_div_lt finishes. Use the representative if ‖G t‖ ≤ C then G t else 0, which is measurable and bounded; Lp.ext + filter_upwards identifies it with G. Also handy: ‖F‖² = ∫ ‖F t‖² for F ∈ L², from inner_self_eq_norm_sq, L2.inner_def and integral_re (L2.integrable_inner F F).