OAI/Geometry/RCD/Sobolev/WeakLaplacianOperator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual L² Laplacian as a linear operator on its domain

  1. def OAI.RegularPointCoordinates.weakLaplacianOperator line 17

    Source documentation

    Uniqueness in L² makes the weak Laplacian a linear operator. No continuity on the whole Sobolev domain is claimed.

    def weakLaplacianOperator : weakLaplacianDomain μ hQ →ₗ[ℝ] Lp ℝ 2 μ where
…

    Mentions: OAI.RegularPointCoordinates.weakLaplacianDomain

  2. theorem OAI.RegularPointCoordinates.weakLaplacianOperator_spec line 26