OAI/Geometry/RCD/Sobolev/HessianLocality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.localGamma_eq_of_dirichlet_right line 18

   Source documentation

   A zero-boundary test sees only the potential inside its domain.

   theorem localGamma_eq_of_dirichlet_right {Ω : Set X} (hΩ : MeasurableSet Ω)
       {f g : SobolevSpace μ hQ}
       (hfg : SobolevSpace.toLp μ hQ f =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ g)
       (φ : SobolevSpace.dirichlet μ hQ Ω) :
       localGamma μ hQ f φ.val =ᵐ[μ] localGamma μ hQ g φ.val := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.localGamma

2. theorem OAI.RegularPointCoordinates.energyForm_eq_of_dirichlet line 32
3. def OAI.RegularPointCoordinates.LocalHessianPairing.congr line 42

   Source documentation

   Replacing either potential outside the domain preserves the complete integrated Hessian data, including its dense core.

   def LocalHessianPairing.congr {Ω : Set X} (hΩ : MeasurableSet Ω)
       {f a F A : SobolevSpace μ hQ}
       (G : LocalHessianPairing μ hQ Ω F A)
       (hf : SobolevSpace.toLp μ hQ F =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ f)
       (ha : SobolevSpace.toLp μ hQ A =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ a) :
       LocalHessianPairing μ hQ Ω f a where
   …

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