English
If κ is IsSFiniteKernel, then for a fixed AEStronglyMeasurable f on a product space, the integrals with respect to κ along fibres are well-defined and measurable.
Русский
Если κ является IsSFiniteKernel, то для фиксированной AEStronglyMeasurable f интегралы по векторам вдоль фибр корректны и измеримы.
LaTeX
$$$\\text{Integrable}(f, \\kappa a) \n\\Rightarrow \\text{measurable}(x \\mapsto \\int f) $$$
Lean4
theorem integral_kernel ⦃f : β → E⦄ (hf : StronglyMeasurable f) : StronglyMeasurable fun x ↦ ∫ y, f y ∂κ x := by
classical
by_cases hE : CompleteSpace E; swap
· simp [integral, hE, stronglyMeasurable_const]
borelize E
have : TopologicalSpace.SeparableSpace (range f ∪ {0} : Set E) := hf.separableSpace_range_union_singleton
let s : ℕ → SimpleFunc β E := SimpleFunc.approxOn _ hf.measurable (range f ∪ {0}) 0 (by simp)
let f' n : α → E := {x | Integrable f (κ x)}.indicator fun x ↦ (s n).integral (κ x)
refine stronglyMeasurable_of_tendsto (f := f') atTop (fun n ↦ ?_) ?_
· refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
simp_rw [SimpleFunc.integral_eq]
refine Finset.stronglyMeasurable_fun_sum _ fun _ _ ↦ ?_
refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
exact κ.measurable_coe ((s n).measurableSet_fiber _)
· rw [tendsto_pi_nhds]; intro x
by_cases hfx : Integrable f (κ x)
· simp only [mem_setOf_eq, hfx, indicator_of_mem, f']
apply tendsto_integral_approxOn_of_measurable_of_range_subset _ hfx
exact subset_rfl
· simp [f', hfx, integral_undef]
