Finite-measure average estimates #
Shared analytic support for bounded measurable limits and local representatives. Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46.
theorem
Algsuperdiff.Probability.abs_average_sub_const_le_of_ae
{Omega : Type u_1}
[MeasurableSpace Omega]
{mu : MeasureTheory.Measure Omega}
[MeasureTheory.IsFiniteMeasure mu]
(hmu : mu ≠ 0)
{f : Omega → ℝ}
(hf : MeasureTheory.Integrable f mu)
{c C : ℝ}
(hC : ∀ᵐ (y : Omega) ∂mu, |f y - c| ≤ C)
:
An almost-everywhere bound about a constant also bounds the finite-measure average.