English
If f: X → Y → E is continuous in the uncurry sense, then the map x ↦ ∫_Y f(x,y) dμ(y) is continuous for suitable s, Y, μ, provided k is compact.
Русский
Если f: X → Y → E непрерывна по несущимся значениям, то x ↦ ∫_Y f(x,y) dμ(y) непрерывна при подходящих условиях на Y, μ, и компактности k.
LaTeX
$$$$ \\text{continuous_parametric_integral_of_continuous} $$$$
Lean4
/-- Given a measurable function `f` with values in `ℝ≥0`, there exists a lower semicontinuous
function `g ≥ f` with integral arbitrarily close to that of `f`. Formulation in terms of
`lintegral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`. -/
theorem exists_le_lowerSemicontinuous_lintegral_ge (f : α → ℝ≥0∞) (hf : Measurable f) {ε : ℝ≥0∞} (εpos : ε ≠ 0) :
∃ g : α → ℝ≥0∞, (∀ x, f x ≤ g x) ∧ LowerSemicontinuous g ∧ (∫⁻ x, g x ∂μ) ≤ (∫⁻ x, f x ∂μ) + ε :=
by
rcases ENNReal.exists_pos_sum_of_countable' εpos ℕ with ⟨δ, δpos, hδ⟩
have :
∀ n,
∃ g : α → ℝ≥0,
(∀ x, eapproxDiff f n x ≤ g x) ∧ LowerSemicontinuous g ∧ (∫⁻ x, g x ∂μ) ≤ (∫⁻ x, eapproxDiff f n x ∂μ) + δ n :=
fun n => SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge μ (eapproxDiff f n) (δpos n).ne'
choose g f_le_g gcont hg using this
refine ⟨fun x => ∑' n, g n x, fun x => ?_, ?_, ?_⟩
· rw [← tsum_eapproxDiff f hf]
exact ENNReal.tsum_le_tsum fun n => ENNReal.coe_le_coe.2 (f_le_g n x)
· refine lowerSemicontinuous_tsum fun n => ?_
exact ENNReal.continuous_coe.comp_lowerSemicontinuous (gcont n) fun x y hxy => ENNReal.coe_le_coe.2 hxy
·
calc
∫⁻ x, ∑' n : ℕ, g n x ∂μ = ∑' n, ∫⁻ x, g n x ∂μ := by
rw [lintegral_tsum fun n => (gcont n).measurable.coe_nnreal_ennreal.aemeasurable]
_ ≤ ∑' n, ((∫⁻ x, eapproxDiff f n x ∂μ) + δ n) := (ENNReal.tsum_le_tsum hg)
_ = ∑' n, ∫⁻ x, eapproxDiff f n x ∂μ + ∑' n, δ n := ENNReal.tsum_add
_ ≤ (∫⁻ x : α, f x ∂μ) + ε := by
refine add_le_add ?_ hδ.le
rw [← lintegral_tsum]
· simp_rw [tsum_eapproxDiff f hf, le_refl]
· intro n; exact (SimpleFunc.measurable _).coe_nnreal_ennreal.aemeasurable
