LocalSignedMeasureEquality.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Local test identities determine the full signed measure

theorem OAI.RegularPointCoordinates.signedMeasure_eq_restrict_of_tests line 19

Source documentation

Equality on the local compact Lipschitz test class includes singular parts of the measure on every interior set carrying such a cutoff.

theorem signedMeasure_eq_restrict_of_tests (ν τ : SignedMeasure X)
    {Ω S : Set X} (hS : MeasurableSet S)
    (χ : X →ᵇ ℝ) {L : ℝ≥0} (hχ : LipschitzWith L χ)
    (hχc : HasCompactSupport (χ : X → ℝ)) (hχΩ : tsupport χ ⊆ Ω)
    (hχ0 : ∀ x, 0≤χ x) (hχ1 : ∀ x ∈ S, χ x=1)
    (h : ∀ f : compactLipschitzTests Ω,
      signedTestIntegral (f : X →ᵇ ℝ) ν = signedTestIntegral (f : X →ᵇ ℝ) τ) :
    ν.restrict S=τ.restrict S := by
…

Mentions: OAI.RegularPointCoordinates.compactLipschitzTests, OAI.RegularPointCoordinates.signedTestIntegral