HeatVarianceDerivative.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Differentiating the forward/backward heat variance pairing

def OAI.RegularPointCoordinates.heatSquarePairing line 17
Source documentation
The pairing whose endpoints give the heat variance.
```
def heatSquarePairing (f w : Lp ℝ 2 μ) (C : ℝ≥0)
    (hf : ∀ᵐ x ∂μ, |f x| ≤ C) (T s : ℝ) : ℝ :=
…
```

theorem OAI.RegularPointCoordinates.heatSquarePairing_hasDerivAt line 24

Source documentation

In the interior of the time interval, the derivative is twice the weighted gradient energy of the backward heat flow.

theorem heatSquarePairing_hasDerivAt (f w : Lp ℝ 2 μ) (C B L : ℝ≥0)
    (hf : ∀ᵐ x ∂μ, |f x| ≤ C) (hw : ∀ᵐ x ∂μ, |w x| ≤ B)
    (T s : ℝ) (hs : 0 < s) (hTs : 0 < T-s)
    (hg : ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ
      (heatSobolev μ hQ (T-s) hTs f) x ≤ L) :
    HasDerivAt (heatSquarePairing μ hQ f w C hf T)
      (2*∫ x, heatAt μ hQ s w x*(SobolevSpace.minimalSlope μ hQ
        (heatSobolev μ hQ (T-s) hTs f) x)^2 ∂μ) s := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.heatSobolev, OAI.RegularPointCoordinates.heatSquarePairing, OAI.RegularPointCoordinates.heatAt