English
Continuity of the map sending a function to its iterated integral with respect to kernels κ and η.
Русский
Непрерывность отображения, отправляющего функцию в её повторный интеграл по ядрам κ и η.
LaTeX
$$Continuous fun f => ∫ x ∫ y f(x,y) dy dη(a,x) with κ.$$
Lean4
theorem continuous_integral_integral : Continuous fun f : β × γ →₁[(κ ⊗ₖ η) a] E => ∫ x, ∫ y, f (x, y) ∂η (a, x) ∂κ a :=
by
rw [continuous_iff_continuousAt]; intro g
refine
tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_compProd
(Eventually.of_forall fun h => (L1.integrable_coeFn h).integral_compProd) ?_
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)‖ₑ ∂η (a, x) ∂κ a
swap; · exact fun i => lintegral_mono fun x => enorm_integral_le_lintegral_enorm _
change Tendsto (fun i : β × γ →₁[(κ ⊗ₖ η) a] E => ∫⁻ x, ∫⁻ y : γ, ‖i (x, y) - g (x, y)‖ₑ ∂η (a, x) ∂κ a) (𝓝 g) (𝓝 0)
have this (i : Lp (α := β × γ) E 1 (((κ ⊗ₖ η) a) : Measure (β × γ))) : Measurable fun z => ‖i z - g z‖ₑ :=
((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm
simp_rw [← lintegral_compProd _ _ _ (this _), ← L1.ofReal_norm_sub_eq_lintegral, ← ofReal_zero]
refine (continuous_ofReal.tendsto 0).comp ?_
rw [← tendsto_iff_norm_sub_tendsto_zero]
exact tendsto_id
