HeatVarianceForms.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Continuity of the forms in the reverse Poincaré inequality

theorem OAI.RegularPointCoordinates.heat_weighted_energy_continuous line 18
Source documentation
Weighted energy of a positive-time heat flow is continuous in its initial L² data.
```
theorem heat_weighted_energy_continuous (w : Lp ℝ 2 μ) (B : ℝ≥0)
    (hw : ∀ᵐ x ∂μ, |w x| ≤ B) (T : ℝ) (hT : 0 < T) :
    Continuous (fun f : Lp ℝ 2 μ => ∫ x, w x*(SobolevSpace.minimalSlope μ hQ
      (heatSobolev μ hQ T hT f) x)^2 ∂μ) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.heatSobolev

theorem OAI.RegularPointCoordinates.heat_variance_continuous line 28

Source documentation

Both terms of the heat variance are continuous in L².

theorem heat_variance_continuous (w : Lp ℝ 2 μ) (B : ℝ≥0)
    (hw : ∀ᵐ x ∂μ, |w x| ≤ B) (T : ℝ) :
    Continuous (fun f : Lp ℝ 2 μ =>
      (∫ x, heatAt μ hQ T w x*(f x)^2 ∂μ)-
        (∫ x, w x*(heatAt μ hQ T f x)^2 ∂μ)) := by
…

Mentions: OAI.RegularPointCoordinates.heatAt