HeatLogarithmData.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Constructed Sobolev logarithmic heat data

The regularized logarithm of the actual bounded RCD heat evolution has a Sobolev Laplacian and a Sobolev squared gradient. No bound on the original heat generator is assumed.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_logarithm_sobolev_data line 26
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_logarithm_bochner_data line 65
Source documentation
The actual logarithmic heat state satisfies Bochner for every bounded continuous nonnegative Sobolev test on the whole space.
```
theorem heat_logarithm_bochner_data (f : Lp ℝ 2 (hausdorff n X))
    (hf0 : 0≤f) (A : ℝ≥0) (hf : ∀ᵐ x ∂hausdorff n X, |f x|≤A)
    {t ε : ℝ} (ht : 0<t) (hε : 0<ε) :
    let v := hX.boundedHeat hn p f ⟨A,hf⟩ t ht
…
```
Mentions: OAI.RegularPointCoordinates.hausdorff