English
If F_measurable, bound_hasFiniteIntegral and h_bound/h_lim hold, then a.e. Tendsto of ENNReal.ofReal‖F_n a‖ to ENNReal.ofReal‖f a‖.
Русский
Если F_measurable, bound_hasFiniteIntegral и условия h_bound/h_lim выполнены, то почти везде имеет место сходимость ENNReal.ofReal‖F_n a‖ → ENNReal.ofReal‖f a‖.
LaTeX
$$HasFiniteIntegral bound μ ∧ (∀ n, ∀ᵐ a, ‖F n a‖ ≤ bound a) ∧ (∀ᵐ a, Tendsto (fun n => F n a) atTop (nhds (f a))) ⇒ ∀ᵐ a, Tendsto (fun n => ENNReal.ofReal ‖F n a‖) atTop (nhds (ENNReal.ofReal ‖f a‖))$$
Lean4
theorem tendsto_lintegral_norm_of_dominated_convergence (F_measurable : ∀ n, AEStronglyMeasurable (F n) μ)
(bound_hasFiniteIntegral : HasFiniteIntegral bound μ) (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a)
(h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))) :
Tendsto (fun n => ∫⁻ a, ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0) :=
by
have f_measurable : AEStronglyMeasurable f μ := aestronglyMeasurable_of_tendsto_ae _ F_measurable h_lim
let b a :=
2 *
ENNReal.ofReal
(bound a)
/- `‖F n a‖ ≤ bound a` and `F n a --> f a` implies `‖f a‖ ≤ bound a`, and thus by the
triangle inequality, have `‖F n a - f a‖ ≤ 2 * (bound a)`. -/
have hb : ∀ n, ∀ᵐ a ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a :=
by
intro n
filter_upwards [all_ae_ofReal_F_le_bound h_bound n, all_ae_ofReal_f_le_bound h_bound h_lim] with a h₁ h₂
calc
ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖ :=
by
rw [← ENNReal.ofReal_add]
· apply ofReal_le_ofReal
apply norm_sub_le
· exact norm_nonneg _
· exact norm_nonneg _
_ ≤ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) := (add_le_add h₁ h₂)
_ = b a := by
rw [← two_mul]
-- On the other hand, `F n a --> f a` implies that `‖F n a - f a‖ --> 0`
have h : ∀ᵐ a ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0) :=
by
rw [← ENNReal.ofReal_zero]
refine h_lim.mono fun a h => (continuous_ofReal.tendsto _).comp ?_
rwa [← tendsto_iff_norm_sub_tendsto_zero]
/- Therefore, by the dominated convergence theorem for nonnegative integration, have
` ∫ ‖f a - F n a‖ --> 0 ` -/
suffices Tendsto (fun n => ∫⁻ a, ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ _ : α, 0 ∂μ)) by
rwa [lintegral_zero] at this
refine
tendsto_lintegral_of_dominated_convergence' _ ?_ hb ?_
?_
-- Show `fun a => ‖f a - F n a‖` is almost everywhere measurable for all `n`
· exact fun n => measurable_ofReal.comp_aemeasurable ((F_measurable n).sub f_measurable).norm.aemeasurable
· rw [hasFiniteIntegral_iff_ofReal] at bound_hasFiniteIntegral
·
calc
∫⁻ a, b a ∂μ = 2 * ∫⁻ a, ENNReal.ofReal (bound a) ∂μ :=
by
rw [lintegral_const_mul']
finiteness
_ ≠ ∞ := mul_ne_top coe_ne_top bound_hasFiniteIntegral.ne
filter_upwards [h_bound 0] with _ h using le_trans (norm_nonneg _) h
· exact h
