OAI/Geometry/RCD/Sobolev/WeakLaplacianDomain.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The linear domain of the weak L² Laplacian

  1. lemma OAI.RegularPointCoordinates.IsWeakLaplacian.add line 16
  2. lemma OAI.RegularPointCoordinates.IsWeakLaplacian.smul line 23
  3. def OAI.RegularPointCoordinates.weakLaplacianDomain line 31

    Source documentation

    The existence domain, with no bound on the size of its Laplacian.

    def weakLaplacianDomain : Submodule ℝ (SobolevSpace μ hQ) where
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace