HarmonicBochnerHeat.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual harmonic heat Gram and its canonical signed source

The local Bochner input, a cutoff with a weak Laplacian, and the published continuous heat kernel now give the heat Gram evolution. The source is constructed, with its full singular part and compact support retained.

def OAI.RegularPointCoordinates.LocalHarmonicEnergy.cutoffEnergy line 30
Source documentation
The actual bounded Sobolev product representing the cutoff energy.
```
def cutoffEnergy (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (c : SobolevSpace μ hQ) : SobolevSpace μ hQ :=
…
```
Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.SobolevSpace
def OAI.RegularPointCoordinates.LocalHarmonicEnergy.cutoffSource line 35
Source documentation
The canonical full signed source, not a density-only replacement.
```
def cutoffSource (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (c : SobolevSpace μ hQ) (q : Lp ℝ 2 μ) : SignedMeasure X :=
…
```
Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.SobolevSpace

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.cutoffEnergy_coe line 41

Source documentation

This product has exactly the required cutoff Gram representative.

theorem cutoffEnergy_coe (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (hχΩ : tsupport (χ : X → ℝ) ⊆ ball p (2 * r))
    (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ) :
    SobolevSpace.toLp μ hQ (G.cutoffEnergy μ hQ χ c) =ᵐ[μ]
      fun x => χ x * (SobolevSpace.minimalSlope μ hQ (U v) x) ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.cutoffEnergy_laplacian line 63

Source documentation

The global measure equation is derived from the local Bochner equation.

theorem cutoffEnergy_laplacian (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (hχs : HasCompactSupport (χ : X → ℝ))
    (hχΩ : tsupport (χ : X → ℝ) ⊆ ball p (2 * r))
    (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (q : Lp ℝ 2 μ) (hq : IsWeakLaplacian μ hQ c q) :
    IsMeasureLaplacian μ hQ (G.cutoffEnergy μ hQ χ c) (G.cutoffSource μ hQ χ c q) :=
…

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.heatGram_hasDerivAt line 75

Source documentation

Full-source evolution of the actual harmonic heat Gram. Compact support hypotheses concern only the cutoff and its weak Laplacian.

theorem heatGram_hasDerivAt (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (hχs : HasCompactSupport (χ : X → ℝ))
    (hχΩ : tsupport (χ : X → ℝ) ⊆ ball p (2 * r))
    (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (q : Lp ℝ 2 μ) (hq : IsWeakLaplacian μ hQ c q)
    (a : X) {R : ℝ} (hR : 0 < R)
    (hχR : ∀ x ∉ closedBall a R, χ x = 0)
    (hqR : ∀ᵐ x ∂μ, x ∉ closedBall a R → q x = 0)
    {t : ℝ} (ht : 0 < t) (x : X) (lambda : ℝ) :
    HasDerivAt (fun s => ⟪v, cutoffHeatGramAt μ hQ hk χ.continuous hχs U s x lambda v⟫_ℝ)
      ((∫ᵛ z, k t x z ∂<•(G.cutoffSource μ hQ χ c q)) + lambda * ‖v‖ ^ 2) t := by
…