English
The a.e. equality of the restricting CLM coincides with the a.e. equality of the restricted function.
Русский
Слабая эквивалентность ограничивающего CLM совпадает с эквивалентностью ограниченной функции почти повсюду.
LaTeX
$$$$LpToLpRestrictCLM\\_coeFn: a.e_{μ.restrict s}(f) = f|_s$$$$
Lean4
/-- The parametric integral over a continuous function on a compact set is continuous,
under mild assumptions on the topologies involved. -/
theorem continuous_parametric_integral_of_continuous [FirstCountableTopology X] [LocallyCompactSpace X]
[SecondCountableTopologyEither Y E] [IsLocallyFiniteMeasure μ] {f : X → Y → E} (hf : Continuous f.uncurry)
{s : Set Y} (hs : IsCompact s) : Continuous (∫ y in s, f · y ∂μ) :=
by
rw [continuous_iff_continuousAt]
intro x₀
rcases exists_compact_mem_nhds x₀ with ⟨U, U_cpct, U_nhds⟩
rcases (U_cpct.prod hs).bddAbove_image hf.norm.continuousOn with ⟨M, hM⟩
apply continuousAt_of_dominated
· filter_upwards with x using Continuous.aestronglyMeasurable (by fun_prop)
· filter_upwards [U_nhds] with x x_in
rw [ae_restrict_iff]
· filter_upwards with t t_in using hM (mem_image_of_mem _ <| mk_mem_prod x_in t_in)
· exact (isClosed_le (by fun_prop) (by fun_prop)).measurableSet
· exact integrableOn_const hs.measure_ne_top
· filter_upwards using (by fun_prop)
