HeatGramEvolution.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Evolution of actual cutoff heat Grams

A weak measure Laplacian of the cutoff energy density gives its pointwise heat derivative and the integrated Gram increment. A nonnegative shifted source then implies monotonicity.

def OAI.RegularPointCoordinates.cutoffHeatGramAt line 29
Source documentation
An all-time extension used only to state ordinary derivatives at positive times; it agrees with the actual Gram wherever it is used.
```
def cutoffHeatGramAt (t : ℝ) (x : X) (lambda : ℝ) : E →L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.cutoffHeatGramAt_of_pos line 32
theorem OAI.RegularPointCoordinates.cutoffHeatGram_kernel_energy line 39
Source documentation
Identification with the continuous kernel representative, rather than an almost-everywhere choice of the heat flow.
```
theorem cutoffHeatGram_kernel_energy (v : E) (f : SobolevSpace μ hQ)
    (hf : SobolevSpace.toLp μ hQ f =ᵐ[μ]
      fun z => χ z * (SobolevSpace.minimalSlope μ hQ (U v) z) ^ 2)
    {t : ℝ} (ht : 0 < t) (x : X) (lambda : ℝ) :
    ⟪v, cutoffHeatGram μ hQ hp hχ hsχ U ht x lambda v⟫_ℝ =
      kernelHeat μ hQ hp t (SobolevSpace.toLp μ hQ f) x + lambda * t * ‖v‖ ^ 2 := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.cutoffHeatGram, OAI.RegularPointCoordinates.kernelHeat

theorem OAI.RegularPointCoordinates.cutoffHeatGram_hasDerivAt line 53

Source documentation

Full measure-source differentiation of the actual heat Gram.

theorem cutoffHeatGram_hasDerivAt (v : E) (f : SobolevSpace μ hQ)
    (hf : SobolevSpace.toLp μ hQ f =ᵐ[μ]
      fun z => χ z * (SobolevSpace.minimalSlope μ hQ (U v) z) ^ 2)
    (ν : SignedMeasure X) (hν : IsMeasureLaplacian μ hQ f ν)
    (c : X) {R : ℝ} (hR : 0 < R)
    (hfs : ∀ᵐ z ∂μ, R < dist c z → SobolevSpace.toLp μ hQ f z = 0)
    (hνs : ν.variation (Metric.closedBall c R)ᶜ = 0)
    {t : ℝ} (ht : 0 < t) (x : X) (lambda : ℝ) :
    HasDerivAt (fun s => ⟪v, cutoffHeatGramAt μ hQ hp hχ hsχ U s x lambda v⟫_ℝ)
      ((∫ᵛ z, p t x z ∂<•ν) + lambda * ‖v‖ ^ 2) t := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.IsMeasureLaplacian, OAI.RegularPointCoordinates.cutoffHeatGramAt

theorem OAI.RegularPointCoordinates.cutoffHeatGram_sub_eq_integral line 74

Source documentation

Integrating the source gives the actual Gram increment between any positive times. No density for the signed source is assumed.

theorem cutoffHeatGram_sub_eq_integral (v : E) (f : SobolevSpace μ hQ)
    (hf : SobolevSpace.toLp μ hQ f =ᵐ[μ]
      fun z => χ z * (SobolevSpace.minimalSlope μ hQ (U v) z) ^ 2)
    (ν : SignedMeasure X) (hν : IsMeasureLaplacian μ hQ f ν)
    (c : X) {R : ℝ} (hR : 0 < R)
    (hfs : ∀ᵐ z ∂μ, R < dist c z → SobolevSpace.toLp μ hQ f z = 0)
    (hνs : ν.variation (Metric.closedBall c R)ᶜ = 0)
    {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) (x : X) (lambda : ℝ) :
    ⟪v, cutoffHeatGram μ hQ hp hχ hsχ U (hs.trans_le hst) x lambda v⟫_ℝ -
      ⟪v, cutoffHeatGram μ hQ hp hχ hsχ U hs x lambda v⟫_ℝ =
      (∫ r in s..t, (∫ᵛ z, p r x z ∂<•ν)) + lambda * (t - s) * ‖v‖ ^ 2 := by
…

theorem OAI.RegularPointCoordinates.cutoffHeatGram_monotone line 92

Source documentation

Positivity of the shifted source gives monotonicity of the actual quadratic heat Gram on positive times.

theorem cutoffHeatGram_monotone (v : E) (f : SobolevSpace μ hQ)
    (hf : SobolevSpace.toLp μ hQ f =ᵐ[μ]
      fun z => χ z * (SobolevSpace.minimalSlope μ hQ (U v) z) ^ 2)
    (ν : SignedMeasure X) (hν : IsMeasureLaplacian μ hQ f ν)
    (c : X) {R : ℝ} (hR : 0 < R)
    (hfs : ∀ᵐ z ∂μ, R < dist c z → SobolevSpace.toLp μ hQ f z = 0)
    (hνs : ν.variation (Metric.closedBall c R)ᶜ = 0)
    (x : X) (lambda : ℝ)
    (hpos : ∀ t, 0 < t → 0 ≤ (∫ᵛ z, p t x z ∂<•ν) + lambda * ‖v‖ ^ 2)
    {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) :
    ⟪v, cutoffHeatGram μ hQ hp hχ hsχ U hs x lambda v⟫_ℝ ≤
      ⟪v, cutoffHeatGram μ hQ hp hχ hsχ U (hs.trans_le hst) x lambda v⟫_ℝ := by
…