HarmonicOperatorEvolution.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The full operator-valued harmonic heat equation

theorem OAI.RegularPointCoordinates.harmonicHeatGram_hasDerivAt line 25

Source documentation

Polarizing the actual scalar Bochner identities yields the full operator derivative, with the singular mass measure retained.

theorem harmonicHeatGram_hasDerivAt (hρ : 0 < ρ) (hρr : ρ < r)
    {t : ℝ} (ht : 0 < t) (x : X) {lambda : ℝ} (hlambda : 0 ≤ lambda) :
    HasDerivAt
      (fun s => cutoffHeatGramAt μ hQ hk χ.weight.continuous
        (χ.hasCompactSupport μ hQ) U s x lambda)
      ((2 : ℝ) • cutoffHeatMass μ hQ hk χ.weight.continuous
          (χ.hasCompactSupport μ hQ) M ht x -
        (2 * κ) • cutoffHeatGram μ hQ hk χ.weight.continuous
          (χ.hasCompactSupport μ hQ) U ht x 0 +
        harmonicHeatError μ hQ (k := k) G χ t x +
…

Mentions: OAI.RegularPointCoordinates.cutoffHeatGramAt, OAI.RegularPointCoordinates.cutoffHeatMass, OAI.RegularPointCoordinates.cutoffHeatGram, OAI.RegularPointCoordinates.harmonicHeatError

theorem OAI.RegularPointCoordinates.harmonicHeatError_energy line 84
Source documentation
The quadratic value of the operator error equals the scalar error in every direction, not just those used in polarization.
```
theorem harmonicHeatError_energy (hρ : 0 < ρ) (hρr : ρ < r)
    {t : ℝ} (ht : 0 < t) (x : X) (v : Euclidean n) :
    ⟪v, harmonicHeatError μ hQ (k := k) G χ t x v⟫_ℝ =
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.harmonicHeatError