CompactMeasureLaplacian.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported measure Laplacians and continuous Sobolev tests

IsMeasureLaplacian records the distributional integration-by-parts identity on continuous compactly supported Sobolev tests. It is a definition, not an existence assumption. The cutoff argument extends this identity to arbitrary continuous Sobolev representatives when the function and its full signed Laplacian have compact support. In particular it applies to positive-time kernel rows without removing singular mass.

def OAI.RegularPointCoordinates.IsMeasureLaplacian line 29
Source documentation
The weak measure-valued Laplacian, tested on continuous compactly supported Sobolev representatives.
```
def IsMeasureLaplacian (u : SobolevSpace μ hQ) (ν : SignedMeasure X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace

theorem OAI.RegularPointCoordinates.IsMeasureLaplacian.test_continuous line 36

Source documentation

Compact support of both the function and the full signed source allows all continuous Sobolev representatives as tests.

theorem IsMeasureLaplacian.test_continuous
    {u : SobolevSpace μ hQ} {ν : SignedMeasure X}
    (hν : IsMeasureLaplacian μ hQ u ν) (c : X) {R : ℝ} (hR : 0 < R)
    (hu : ∀ᵐ x ∂μ, R < dist c x → SobolevSpace.toLp μ hQ u x = 0)
    (hsν : ν.variation (Metric.closedBall c R)ᶜ = 0)
    (φ : SobolevSpace μ hQ) {v : X → ℝ} (hv : Continuous v)
    (hφ : SobolevSpace.toLp μ hQ φ =ᵐ[μ] v) :
    energyForm μ hQ u φ = -(∫ᵛ x, v x ∂<•ν) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsMeasureLaplacian, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm

theorem OAI.RegularPointCoordinates.IsMeasureLaplacian.test_heatKernel line 83

Source documentation

Integration by parts against the actual continuous heat-kernel row.

theorem IsMeasureLaplacian.test_heatKernel
    {u : SobolevSpace μ hQ} {ν : SignedMeasure X}
    (hν : IsMeasureLaplacian μ hQ u ν) (c : X) {R : ℝ} (hR : 0 < R)
    (hu : ∀ᵐ x ∂μ, R < dist c x → SobolevSpace.toLp μ hQ u x = 0)
    (hsν : ν.variation (Metric.closedBall c R)ᶜ = 0)
    {t : ℝ} (ht : 0 < t) (x : X) :
    energyForm μ hQ u (heatKernelSobolev μ hQ hp t ht x) =
      -(∫ᵛ z, p t x z ∂<•ν) :=
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsMeasureLaplacian, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.heatKernelSobolev