OAI/Geometry/RCD/Coordinates/RegularDirichletCore.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A dense compact test core with actual L² Laplacians

  1. def OAI.RegularPointCoordinates.compactLaplacianCore line 16

    Source documentation

    Compact Lipschitz Sobolev functions whose weak Laplacian belongs to L².

    def compactLaplacianCore (μ : Measure X) (hQ : QuadraticCheegerEnergy μ) (Ω : Set X) :
    Submodule ℝ (SobolevSpace μ hQ) :=
…

    Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace

  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compactLaplacianCore_closure line 20
  3. def OAI.RegularPointCoordinates.regularDirichletCore line 87

    Source documentation

    The same core as a submodule of the actual zero-boundary space.

    def regularDirichletCore (μ : Measure X) (hQ : QuadraticCheegerEnergy μ) (Ω : Set X) :
    Submodule ℝ (SobolevSpace.dirichlet μ hQ Ω) :=
…

    Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace.dirichlet

  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regularDirichletCore_dense line 91