English
The map sending a γ →₁[(η ∘ₖ κ) a]-valued function f to the iterated integral ∫ x ∫ y f(y) dη x dκ a is continuous with respect to the L1 norm.
Русский
Отображение, отправляющее функцию f в L1-пространстве в элемент в E через двойной интеграл, непрерывно по норме L1.
LaTeX
$$$$ \\text{Continuous}\\big( f \\mapsto \\int x \\int y f(y) d\\eta_x(y) d\\kappa a \\big) $$$$
Lean4
theorem continuous_integral_integral_comp : Continuous fun f : γ →₁[(η ∘ₖ κ) a] E ↦ ∫ x, ∫ y, f y ∂η x ∂κ a :=
by
refine continuous_iff_continuousAt.2 fun g ↦ ?_
refine
tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_comp
(Eventually.of_forall fun h ↦ (L1.integrable_coeFn h).integral_comp) ?_
simp_rw [← lintegral_fn_integral_sub_comp (‖·‖ₑ) (L1.integrable_coeFn _) (L1.integrable_coeFn g)]
refine
tendsto_of_tendsto_of_tendsto_of_le_of_le (h := fun i ↦ ∫⁻ x, ∫⁻ y, ‖i y - g y‖ₑ ∂η x ∂κ a) tendsto_const_nhds ?_
(fun _ ↦ zero_le _) ?_
swap; · exact fun _ ↦ lintegral_mono fun _ ↦ enorm_integral_le_lintegral_enorm _
have (i : γ →₁[(η ∘ₖ κ) a] E) : Measurable fun z ↦ ‖i z - g z‖ₑ :=
((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm
simp_rw [← lintegral_comp _ _ _ (this _), ← L1.ofReal_norm_sub_eq_lintegral, ← ofReal_zero]
exact (continuous_ofReal.tendsto 0).comp (tendsto_iff_norm_sub_tendsto_zero.1 tendsto_id)
