OAI/Geometry/RCD/Sobolev/BochnerSourceUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.bochnerGramSource_unique_restrict line 20
2. theorem OAI.RegularPointCoordinates.bochnerDensity_unique line 40

   Source documentation

   Local uniqueness of the full source also identifies the density used in a pointwise Hessian estimate, independently of the auxiliary family.

   theorem bochnerDensity_unique [SigmaFinite μ] {Ω S : Set X} (hΩ : MeasurableSet Ω)
       (hS : MeasurableSet S) (K : ℝ) (f g df dg F G : SobolevSpace μ hQ)
       (ν τ : Measure X) [IsFiniteMeasure ν] [IsFiniteMeasure τ]
       (hF : IsMeasureLaplacianOn μ hQ Ω F (bochnerGramSource μ hQ K f g df dg ν.toSignedMeasure))
       (hG : IsMeasureLaplacianOn μ hQ Ω G (bochnerGramSource μ hQ K f g df dg τ.toSignedMeasure))
       (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) :
       (fun x => (ν.rnDeriv μ x).toReal) =ᵐ[μ.restrict S] fun x => (τ.rnDeriv μ x).toReal := by
   …

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