mapCLM — Mathlib

English

The push-forward construction can be upgraded to a continuous linear map mapCLM when f is continuous between Borels Spaces.

Русский

Пересылка мер по непрерывной функции между борелевскими пространствами образует непрерывное линейное отображение.

LaTeX

$$mapCLM f_cont : FiniteMeasure Ω →L[ℝ≥0] FiniteMeasure Ω' is continuous with toFun ν ↦ ν.map f$$

Lean4

/-- The push-forward of a finite measure by a continuous function between Borel spaces as
a continuous linear map. -/
noncomputable def mapCLM {f : Ω → Ω'} (f_cont : Continuous f) : FiniteMeasure Ω →L[ℝ≥0] FiniteMeasure Ω'
    where
  toFun := fun ν ↦ ν.map f
  map_add' := map_add f_cont.measurable
  map_smul' := map_smul
  cont := continuous_map f_cont

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