testAgainstNN_coe_eq — Mathlib

English

The ENNReal value of μ.testAgainstNN f equals the integral of f against μ, written via ENNReal coercions.

Русский

Значение ENNReal от μ.testAgainstNN f равно интегралу по μ от f, выраженному через приведения ENNReal.

LaTeX

$$$(\mu.testAgainstNN f) : \mathbb{R}_{≥0}^{∞} = \int f \, d\mu$$$

Lean4

@[simp]
theorem testAgainstNN_coe_eq {μ : FiniteMeasure Ω} {f : Ω →ᵇ ℝ≥0} :
    (μ.testAgainstNN f : ℝ≥0∞) = ∫⁻ ω, f ω ∂(μ : Measure Ω) :=
  ENNReal.coe_toNNReal (f.lintegral_lt_top_of_nnreal _).ne

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