OAI/Geometry/RCD/Metric/SignedSourceDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating a full signed source and an integrable density

  1. theorem OAI.RegularPointCoordinates.integral_signedDensity line 19

    Source documentation

    A bounded continuous test integrates an integrable signed density by the expected product formula, without discarding either sign.

    theorem integral_signedDensity (μ : Measure X) {f : X → ℝ} (hf : Integrable f μ)
    (w : X →ᵇ ℝ) :
    (∫ᵛ x, w x ∂<•(μ.withDensityᵥ f)) = ∫ x, w x * f x ∂μ := by
…