testAgainstNN_eq_mass_mul — Mathlib

English

For a finite measure μ and a bounded nonnegative function f, the testAgainstNN of μ equals the mass of μ times the testAgainstNN of the normalized finite measure.

Русский

Для конечной меры μ и ограниченной неотрицательной функции f выполнено: μ.testAgainstNN(f) = μ(Ω) · (μ.normalize.toFiniteMeasure).testAgainstNN(f).

LaTeX

$$$μ.testAgainstNN f = μ.mass \\cdot (μ.normalize.toFiniteMeasure).testAgainstNN f$$$

Lean4

theorem testAgainstNN_eq_mass_mul (f : Ω →ᵇ ℝ≥0) :
    μ.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f :=
  by
  nth_rw 1 [μ.self_eq_mass_smul_normalize]
  rw [μ.normalize.toFiniteMeasure.smul_testAgainstNN_apply μ.mass f, smul_eq_mul]

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