measure_le_lintegral_thickenedIndicatorAux

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

Похожие утверждения