continuous_setToFun_of_dominated — Mathlib

English

Under dominated convergence assumptions, the function x ↦ setToFun μ T hT (fs x) is continuous on s.

Русский

При условиях доминированной сходимости функция x ↦ setToFun μ T hT (fs x) непрерывна на s.

LaTeX

$$$\\mathrm{ContinuousOn}(\\lambda x. \\mathrm{setToFun}\\;\\mu\\; T\\; hT\\; (fs x))\\ s$$$

Lean4

theorem continuous_setToFun_of_dominated (hT : DominatedFinMeasAdditive μ T C) {fs : X → α → E} {bound : α → ℝ}
    (hfs_meas : ∀ x, AEStronglyMeasurable (fs x) μ) (h_bound : ∀ x, ∀ᵐ a ∂μ, ‖fs x a‖ ≤ bound a)
    (bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ a ∂μ, Continuous fun x => fs x a) :
    Continuous fun x => setToFun μ T hT (fs x) :=
  continuous_iff_continuousAt.mpr fun _ =>
    continuousAt_setToFun_of_dominated hT (Eventually.of_forall hfs_meas) (Eventually.of_forall h_bound) ‹_› <|
      h_cont.mono fun _ => Continuous.continuousAt

Похожие утверждения