Set-defined Cesàro conditions to all of L² via Lp.induction in each slot

To pass a bilinear Cesàro condition like N⁻¹∑|⟪x, Uⁿy⟫ − ⟪x,1⟫⟪1,y⟫| → 0 from indicators to all of L²(μ), prove one generic lemma: if F : Lp → ℕ → ℝ is nonnegative, subadditive, and satisfies F x n ≤ F y n + C‖x − y‖, then Cesàro-nullity on all indicatorConstLp gives it everywhere, via MeasureTheory.Lp.induction (its indicator case uses Lp.simpleFunc.coe_indicatorConst; closedness is an ε/2 argument). Apply it twice, first to the left slot with y an indicator, then to the right slot. Use Lp.compMeasurePreserving (f^[n]) (hf.iterate n) directly, not an iterate of the operator, so map_add and norm_compMeasurePreserving are available. A wrapper bLp F := if h : MemLp F 2 μ then h.toLp F else 0 avoids proof-carrying terms inside sums, and gives clean lemmas ⟪bLp F, bLp G⟫ = ∫ F*G and compMeasurePreserving f hf (bLp F) = bLp (F ∘ f), which holds by rfl after unfolding.