HeatDensityConvolution.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Density-level Chapman--Kolmogorov without a pre-existing kernel

def OAI.RegularPointCoordinates.NoncollapsedRCD.heatDensityConvolution line 18
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatDensityConvolution_measurable line 22
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatDensityConvolution_withDensity line 35
Source documentation
Tonelli and the already proved measure semigroup law identify the convolution as the Radon--Nikodym density at the sum of the two times.
```
theorem heatDensityConvolution_withDensity (s t : ℝ) (hs : 0 < s) (ht : 0 < t) (x : X) :
    (hausdorff n X).withDensity (hX.heatDensityConvolution hn p s t hs ht x) =
      hX.heatRadonMeasure hn p (s + t) (add_pos hs ht) x := by
…
```
Mentions: OAI.RegularPointCoordinates.hausdorff
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatDensityConvolution_ae line 73

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatJointDensity_convolution_ae line 88

Source documentation

The density convolution is a finite real integral for almost every endpoint, for each fixed starting point.

theorem heatJointDensity_convolution_ae (s t : ℝ) (hs : 0 < s) (ht : 0 < t) (x : X) :
    ∀ᵐ y ∂hausdorff n X,
      Integrable (fun z => hX.heatJointDensity hn p s hs x z *
        hX.heatJointDensity hn p t ht z y) (hausdorff n X) ∧
      (∫ z, hX.heatJointDensity hn p s hs x z * hX.heatJointDensity hn p t ht z y
        ∂hausdorff n X) = hX.heatJointDensity hn p (s + t) (add_pos hs ht) x y := by
…

Mentions: OAI.RegularPointCoordinates.hausdorff