BoundedHeatSemigroup.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Pointwise semigroup law for the constructed heat measures

theorem OAI.RegularPointCoordinates.HasBoundedAmplitude.heatAt line 19
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.boundedHeat_semigroup line 29
Source documentation
Uniqueness of continuous representatives upgrades the L² semigroup identity to equality at every point.
```
theorem boundedHeat_semigroup (f : Lp ℝ 2 (hausdorff n X))
    (hf : HasBoundedAmplitude f) (s t : ℝ) (hs : 0 < s) (ht : 0 < t) :
    hX.boundedHeat hn p (heatAt (hausdorff n X) hX.quadratic t f)
      (hf.heatAt hX t) s hs =
      hX.boundedHeat hn p f hf (s + t) (add_pos hs ht) := by
…
```
Mentions: OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.HasBoundedAmplitude, OAI.RegularPointCoordinates.heatAt

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_integral_semigroup line 41

Source documentation

Iterated integration of bounded L² data agrees with time addition, for every starting point of the constructed probability family.

theorem heatRadonMeasure_integral_semigroup (f : Lp ℝ 2 (hausdorff n X))
    (C : ℝ≥0) (hf : ∀ᵐ y ∂hausdorff n X, |f y| ≤ C)
    (s t : ℝ) (hs : 0 < s) (ht : 0 < t) (x : X) :
    (∫ y, (∫ z, f z ∂hX.heatRadonMeasure hn p t ht y)
      ∂hX.heatRadonMeasure hn p s hs x) =
      ∫ z, f z ∂hX.heatRadonMeasure hn p (s + t) (add_pos hs ht) x := by
…

Mentions: OAI.RegularPointCoordinates.hausdorff