HeatMeasureEvolution.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The heat identity for a full compactly supported signed Laplacian

The distributional source is paired with continuous positive-time kernel rows. Locality supplies the compact test, and the actual L2 heat equation supplies the derivative. This proves the positive-endpoint measure-source identity without assuming absolute continuity of the source.

theorem OAI.RegularPointCoordinates.kernelHeat_hasDerivAt line 29
Source documentation
Pointwise time differentiation of the continuous representative of heat flow from actual Sobolev data.
```
theorem kernelHeat_hasDerivAt (u : SobolevSpace μ hQ) {t : ℝ}
    (ht : 0 < t) (x : X) :
    HasDerivAt (fun s => kernelHeat μ hQ hp s (SobolevSpace.toLp μ hQ u) x)
      (-energyForm μ hQ u (heatKernelSobolev μ hQ hp t ht x)) t := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.kernelHeat, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.heatKernelSobolev

theorem OAI.RegularPointCoordinates.IsMeasureLaplacian.kernelHeat_hasDerivAt line 54

Source documentation

The pointwise derivative against the full signed source.

theorem IsMeasureLaplacian.kernelHeat_hasDerivAt
    {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) :
    HasDerivAt (fun s => kernelHeat μ hQ hp s (SobolevSpace.toLp μ hQ u) x)
      (∫ᵛ z, p t x z ∂<•ν) t := by
…

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

theorem OAI.RegularPointCoordinates.IsMeasureLaplacian.kernelHeat_sub_eq_integral line 68

Source documentation

The manuscript's positive-endpoint semigroup identity for compact measure sources, using continuous representatives and the full measure.

theorem IsMeasureLaplacian.kernelHeat_sub_eq_integral
    {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)
    {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) (x : X) :
    kernelHeat μ hQ hp t (SobolevSpace.toLp μ hQ u) x -
      kernelHeat μ hQ hp s (SobolevSpace.toLp μ hQ u) x =
      ∫ r in s..t, (∫ᵛ z, p r x z ∂<•ν) := by
…

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