English
The map ε ↦ ∫ f(t) dμ over thickenings is continuous as ε ↓ 0 for a fixed bounded f and finite measure μ.
Русский
Пусть f ограничена и μ — конечная; функция ε ↦ ∫ f над размытиями множества по ε стягивается к пределу при ε → 0.
LaTeX
$$$\\operatorname{Tendsto}\\Big(ε \\mapsto \\int f(t)\\,d\\big(μ\\text{ real of thickening}(ε\\cdot)\\big)\\Big)_{𝓝[>0]0} = \\text{limit}$.$$
Lean4
/-- A monotone decreasing convergence lemma for integrals of measures of thickenings:
`∫ t in (0, ‖f‖], μ (thickening ε {x | f(x) ≥ t}) dt` tends to
`∫ t in (0, ‖f‖], μ {x | f(x) ≥ t} dt` as `ε → 0`. -/
theorem tendsto_integral_meas_thickening_le (f : Ω →ᵇ ℝ) {A : Set ℝ} (A_finmeas : volume A ≠ ∞)
(μ : ProbabilityMeasure Ω) :
Tendsto (fun ε ↦ ∫ t in A, (Measure.real μ (thickening ε {a | t ≤ f a}))) (𝓝[>] (0 : ℝ))
(𝓝 (∫ t in A, (Measure.real μ {a | t ≤ f a}))) :=
by
apply
tendsto_integral_filter_of_dominated_convergence (G := ℝ) (μ := volume.restrict A) (F := fun ε t ↦
(μ (thickening ε {a | t ≤ f a}))) (f := fun t ↦ (μ {a | t ≤ f a})) 1
· apply Eventually.of_forall fun n ↦ Measurable.aestronglyMeasurable ?_
simp only [measurable_coe_nnreal_real_iff]
apply measurable_toNNReal.comp <| Antitone.measurable (fun s t hst ↦ ?_)
exact measure_mono <| thickening_subset_of_subset _ <| fun ω h ↦ hst.trans h
· apply Eventually.of_forall (fun i ↦ ?_)
apply Eventually.of_forall (fun t ↦ ?_)
simp only [Real.norm_eq_abs, NNReal.abs_eq, Pi.one_apply]
exact ENNReal.toReal_mono one_ne_top prob_le_one
· have aux : IsFiniteMeasure (volume.restrict A) := ⟨by simp [lt_top_iff_ne_top, A_finmeas]⟩
apply integrable_const
· apply Eventually.of_forall (fun t ↦ ?_)
simp only [NNReal.tendsto_coe]
apply (ENNReal.tendsto_toNNReal _).comp
· apply tendsto_measure_thickening_of_isClosed ?_ ?_
· exact ⟨1, ⟨Real.zero_lt_one, measure_ne_top _ _⟩⟩
· exact isClosed_le continuous_const f.continuous
· finiteness
