English
The map sending an L1-function f: α×β → E to its double integral ∫∫ f is continuous on the L1-space.
Русский
Отображение, отправляющее функцию L¹ f: α×β → E в её двойной интеграл ∫∫ f, непрерывно на пространстве L¹.
LaTeX
$$$$\\text{The map } f \\mapsto \\int_α \\int_β f(x,y)\\, dν(y)\\, dμ(x) \\text{ is continuous on } L^1(μ×ν; E).$$$$
Lean4
/-- The map that sends an L¹-function `f : α × β → E` to `∫∫f` is continuous. -/
theorem continuous_integral_integral : Continuous fun f : α × β →₁[μ.prod ν] E => ∫ x, ∫ y, f (x, y) ∂ν ∂μ :=
by
rw [continuous_iff_continuousAt]; intro g
refine
tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_prod_left
(Eventually.of_forall fun h => (L1.integrable_coeFn h).integral_prod_left) ?_
simp_rw [← lintegral_fn_integral_sub _ (L1.integrable_coeFn _) (L1.integrable_coeFn g)]
apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le _) _
· exact fun i => ∫⁻ x, ∫⁻ y, ‖i (x, y) - g (x, y)‖ₑ ∂ν ∂μ
swap; · exact fun i => lintegral_mono fun x => enorm_integral_le_lintegral_enorm _
change Tendsto (fun i : α × β →₁[μ.prod ν] E => ∫⁻ x, ∫⁻ y : β, ‖i (x, y) - g (x, y)‖ₑ ∂ν ∂μ) (𝓝 g) (𝓝 0)
have this (i : α × β →₁[μ.prod ν] E) : Measurable fun z => ‖i z - g z‖ₑ :=
((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm
simp_rw [← lintegral_prod _ (this _).aemeasurable, ← L1.ofReal_norm_sub_eq_lintegral, ← ofReal_zero]
refine (continuous_ofReal.tendsto 0).comp ?_
rw [← tendsto_iff_norm_sub_tendsto_zero]; exact tendsto_id
