HeatVarianceContinuity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Continuity and endpoint identities for the heat variance pairing

theorem OAI.RegularPointCoordinates.heatSquarePairing_continuous line 17
Source documentation
The variance pairing is continuous, including at both heat endpoints.
```
theorem heatSquarePairing_continuous (f w : Lp ℝ 2 μ) (C : ℝ≥0)
    (hf : ∀ᵐ x ∂μ, |f x| ≤ C) (T : ℝ) :
    Continuous (heatSquarePairing μ hQ f w C hf T) := by
…
```
Mentions: OAI.RegularPointCoordinates.heatSquarePairing

theorem OAI.RegularPointCoordinates.heatSquarePairing_eq_integral line 31

Source documentation

Integral representation with the actual heat functions.

theorem heatSquarePairing_eq_integral (f w : Lp ℝ 2 μ) (C : ℝ≥0)
    (hf : ∀ᵐ x ∂μ, |f x| ≤ C) (T s : ℝ) :
    heatSquarePairing μ hQ f w C hf T s =
      ∫ x, heatAt μ hQ s w x*(heatAt μ hQ (T-s) f x)^2 ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.heatSquarePairing, OAI.RegularPointCoordinates.heatAt

theorem OAI.RegularPointCoordinates.heatSobolev_iterate line 42
Source documentation
The heat semigroup identity holds in the actual Sobolev space.
```
theorem heatSobolev_iterate (f : Lp ℝ 2 μ) (s t : ℝ) (hs : 0 < s) (ht : 0 < t) :
    heatSobolev μ hQ s hs (SobolevSpace.toLp μ hQ (heatSobolev μ hQ t ht f)) =
      heatSobolev μ hQ (s+t) (add_pos hs ht) f := by
…
```
Mentions: OAI.RegularPointCoordinates.heatSobolev, OAI.RegularPointCoordinates.SobolevSpace.toLp