MeasureLaplacianUniqueness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of the full local measure Laplacian

theorem OAI.RegularPointCoordinates.IsMeasureLaplacianOn.unique_restrict line 22

Source documentation

Local representatives have the same full Laplacian measure on every interior set with a compact cutoff. This includes singular parts.

theorem IsMeasureLaplacianOn.unique_restrict {Ω S : Set X} (hΩ : MeasurableSet Ω)
    (hS : MeasurableSet S) {f g : SobolevSpace μ hQ} {ν τ : SignedMeasure X}
    (hf : IsMeasureLaplacianOn μ hQ Ω f ν) (hg : IsMeasureLaplacianOn μ hQ Ω g τ)
    (hfg : SobolevSpace.toLp μ hQ f =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ g)
    (χ : X →ᵇ ℝ) {L : ℝ≥0} (hχ : LipschitzWith L χ)
    (hχc : HasCompactSupport (χ : X → ℝ)) (hχΩ : tsupport χ ⊆ Ω)
    (hχ0 : ∀ x, 0≤χ x) (hχ1 : ∀ x ∈ S, χ x=1) :
    ν.restrict S=τ.restrict S := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsMeasureLaplacianOn, OAI.RegularPointCoordinates.SobolevSpace.toLp