continuous_integral_boundedContinuousFunction

English

For any f ∈ α →ᵇ ℝ, the map μ ↦ ∫ f dμ is continuous on ProbabilityMeasure α.

Русский

Для любого f ∈ α →ᵇ ℝ непрерывна функционал μ ↦ ∫ f dμ на ProbabilityMeasure α.

LaTeX

$$$\\text{continuous_integral_boundedContinuousFunction} \\; (f) : \\text{Continuous }(\\mu \\mapsto \\int x \\, f(x) \\, d\\mu)$$$

Lean4

theorem continuous_integral_boundedContinuousFunction {α : Type*} [TopologicalSpace α] [MeasurableSpace α]
    [OpensMeasurableSpace α] (f : α →ᵇ ℝ) : Continuous fun μ : ProbabilityMeasure α ↦ ∫ x, f x ∂μ :=
  by
  rw [continuous_iff_continuousAt]
  intro μ
  exact continuousAt_of_tendsto_nhds (ProbabilityMeasure.tendsto_iff_forall_integral_tendsto.mp tendsto_id f)

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