isFiniteMeasure_withDensity_ofReal

English

If f: α → ℝ has finite integral, then the density μ.withDensity (f) is finite: IsFiniteMeasure (μ.withDensity (fun x => ENNReal.ofReal (f(x))))

Русский

Если f: α → ℝ имеет конечный интеграл, то плотность μ.withDensity(ENNReal.ofReal f) задаёт конечную меру.

LaTeX

$$$HasFiniteIntegral f μ \Rightarrow IsFiniteMeasure (μ.withDensity (fun x => ENNReal.ofReal (f x)))$$$

Lean4

theorem isFiniteMeasure_withDensity_ofReal {f : α → ℝ} (hfi : HasFiniteIntegral f μ) :
    IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal <| f x) :=
  by
  refine isFiniteMeasure_withDensity ((lintegral_mono fun x => ?_).trans_lt hfi).ne
  exact Real.ofReal_le_enorm (f x)

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