isFiniteMeasure_withDensity — Mathlib

English

If ∫ f dμ ≠ ∞, then μ.withDensity f is a finite measure.

Русский

Если интеграл f по μ не бесконечен, то μ.withDensity f является конечной мерой.

LaTeX

$$$\int f \, d\mu \neq \infty \Rightarrow \text{IsFiniteMeasure}(\mu.withDensity f)$$$

Lean4

theorem isFiniteMeasure_withDensity {f : α → ℝ≥0∞} (hf : ∫⁻ a, f a ∂μ ≠ ∞) : IsFiniteMeasure (μ.withDensity f) :=
  { measure_univ_lt_top := by rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ, lt_top_iff_ne_top] }

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