continuous_integral_boundedContinuousFunction

English

For any fixed bounded continuous f, the map sending a finite measure μ to ∫ f dμ is a continuous functional on the space of finite measures.

Русский

Для фиксированной ограниченно непрерывной функции f отображение μ ↦ ∫ f dμ непрерывно на пространстве конечных мер.

LaTeX

$$$f ∈ C_b(α, \\mathbb{R})\\ \\Rightarrow\\ μ \\mapsto \\int f \\; dμ\\text{ is continuous on FiniteMeasure } α$$$

Lean4

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

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