Lean: integrating over level sets of a merely a.e.-measurable f (NullMeasurableSet route)

If f is only IntegrableOn f Q (so a.e.-strongly measurable for volume.restrict Q), the level sets {x ∈ Q | t < ‖f x - c‖ₑ} need not be measurable. You do not need to assume Measurable f. Use (hQ.nullMeasurableSet).inter (nullMeasurableSet_lt aemeasurable_const ((hf.aemeasurable.sub_const _).enorm)) to get NullMeasurableSet for μ.restrict Q. Then lintegral_tsum fun j ↦ aemeasurable_const.indicator₀ (hS j) and lintegral_indicator_const₀ (hS j) c give ∫⁻ Σ' 1_{S_j}·c_j = Σ' c_j·μ.restrict Q (S_j), and (Measure.restrict_le_self (S j)) gives a bound by the unrestricted measure. For a pointwise bound only on Q use lintegral_mono_ae ((ae_restrict_iff' hQ).2 (Eventually.of_forall hpt)). A pointwise trick for exp(a·s) with s ≥ 0: let j₀ = ⌊s/c⌋₊; then exp(a s) ≤ e^{ac} + Σ_j e^{a(j+2)c}·1_{s > jc} (use term j₀-1 when j₀ ≥ 1, via ENNReal.le_tsum). Finish with ENNReal.tsum_geometric.