English
For any measurable set E and δ ∈ ℝ, the measure of E is bounded above by the lintegral of the thickened indicator function over μ.
Русский
Для измеримого множества E и произвольного δ в ℝ мера E ограничена линтагралом толще индикаторной функции по мере μ.
LaTeX
$$$$\\mu E \\le \\int^{\\! -}_{x} (thickenedIndicatorAux δ E x)\\,d\\mu.$$$$
Lean4
theorem measure_le_lintegral_thickenedIndicatorAux (μ : Measure X) {E : Set X} (E_mble : MeasurableSet E) (δ : ℝ) :
μ E ≤ ∫⁻ x, (thickenedIndicatorAux δ E x : ℝ≥0∞) ∂μ :=
by
convert_to lintegral μ (E.indicator fun _ => (1 : ℝ≥0∞)) ≤ lintegral μ (thickenedIndicatorAux δ E)
· rw [lintegral_indicator E_mble]
simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]
· apply lintegral_mono
apply indicator_le_thickenedIndicatorAux