English
Let F be a closed subset of a topological space X and μ a measure. There exists a decreasing sequence of functions approximating the indicator of F from above, such that for every n the measure of F is bounded above by the integral of the nth approximant: μ(F) ≤ ∫ (hF.apprSeq n) dμ.
Русский
Пусть F является замкнутым подмножеством пространства X и μ — мера. Существует убывающая последовательность функций, аппроксимирующих индикатор F сверху, такая что для каждого n выполнено: μ(F) ≤ ∫ (hF.apprSeq n) dμ.
LaTeX
$$$\\mu(F) \\le \\int_X \\bigl(h_F.apprSeq(n)(x)\\bigr) \\, d\\mu(x)$$$
Lean4
/-- The measure of a closed set is at most the integral of any function in a decreasing
approximating sequence to the indicator of the set. -/
theorem measure_le_lintegral [MeasurableSpace X] [OpensMeasurableSpace X] (μ : Measure X) (n : ℕ) :
μ F ≤ ∫⁻ x, (hF.apprSeq n x : ℝ≥0∞) ∂μ :=
by
convert_to ∫⁻ x, (F.indicator (fun _ ↦ (1 : ℝ≥0∞))) x ∂μ ≤ ∫⁻ x, hF.apprSeq n x ∂μ
· rw [lintegral_indicator hF.measurableSet]
simp only [lintegral_one, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
· apply lintegral_mono
intro x
by_cases hxF : x ∈ F
· simp only [hxF, indicator_of_mem, apprSeq_apply_eq_one hF n hxF, ENNReal.coe_one, le_refl]
· simp only [hxF, not_false_eq_true, indicator_of_notMem, zero_le]
