English
If T ≤ T' pointwise (for all s, x), then setToFun μ T hT f ≤ setToFun μ T' hT' f for all f.
Русский
Если T ≤ T' покомпонентно по всем s, x, то setToFun μ T hT f ≤ setToFun μ T' hT' f для всех f.
LaTeX
$$$\\forall s,x,\\; T s x \\le T' s x \\Rightarrow \\forall f,\\; setToFun \\mu T hT f \\le setToFun \\mu T' hT' f.$$$
Lean4
/-- If `F i → f` in `L1`, then `setToFun μ T hT (F i) → setToFun μ T hT f`. -/
theorem tendsto_setToFun_of_L1 (hT : DominatedFinMeasAdditive μ T C) {ι} (f : α → E) (hfi : Integrable f μ)
{fs : ι → α → E} {l : Filter ι} (hfsi : ∀ᶠ i in l, Integrable (fs i) μ)
(hfs : Tendsto (fun i => ∫⁻ x, ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)) :
Tendsto (fun i => setToFun μ T hT (fs i)) l (𝓝 <| setToFun μ T hT f) := by
classical
let f_lp := hfi.toL1 f
let F_lp i := if hFi : Integrable (fs i) μ then hFi.toL1 (fs i) else 0
have tendsto_L1 : Tendsto F_lp l (𝓝 f_lp) :=
by
rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm']
simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply]
refine (tendsto_congr' ?_).mp hfs
filter_upwards [hfsi] with i hi
refine lintegral_congr_ae ?_
filter_upwards [hi.coeFn_toL1, hfi.coeFn_toL1] with x hxi hxf
simp_rw [F_lp, dif_pos hi, hxi, f_lp, hxf]
suffices Tendsto (fun i => setToFun μ T hT (F_lp i)) l (𝓝 (setToFun μ T hT f))
by
refine (tendsto_congr' ?_).mp this
filter_upwards [hfsi] with i hi
suffices h_ae_eq : F_lp i =ᵐ[μ] fs i from setToFun_congr_ae hT h_ae_eq
simp_rw [F_lp, dif_pos hi]
exact hi.coeFn_toL1
rw [setToFun_congr_ae hT hfi.coeFn_toL1.symm]
exact ((continuous_setToFun hT).tendsto f_lp).comp tendsto_L1
