HeatRegimeBridges.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Passing a common geometric regime to the cumulative heat estimates

theorem OAI.RegularPointCoordinates.eventual_dyadic_time_blocks line 17
Source documentation
A small-time estimate suffices for all sufficiently fine dyadic blocks. No control at times comparable to the cutoff radius is requested.
```
theorem eventual_dyadic_time_blocks {R δ : ℝ} (hR : 0 < R) (hδ : 0 < δ) :
    ∃ J : ℕ, ∀ i, J ≤ i → ∀ t ∈ Icc ((R / 2 ^ i) ^ 2 / 4) ((R / 2 ^ i) ^ 2),
      0 < t ∧ t < δ := by
…
```

theorem OAI.RegularPointCoordinates.dyadic_heat_volumes_of_common_regime line 36

Source documentation

One half-error volume neighborhood supplies the fixed denominators used in all dyadic heat blocks.

theorem dyadic_heat_volumes_of_common_regime (μ : Measure X) (n : ℕ)
    (p : X) {R omega : ℝ} (hR : 0 < R) (homega : 0 < omega)
    (hvolume : ∀ y, dist p y ≤ 2 * R → ∀ r, 0 < r → r ≤ R →
      |μ.real (ball y r) / (omega * r ^ n) - 1| ≤ 1 / 2) :
    ∀ i y, dist p y ≤ 2 * R →
      ∀ t ∈ Icc ((R / 2 ^ i) ^ 2 / 4) ((R / 2 ^ i) ^ 2),
        (omega / (2 * (2 : ℝ) ^ n)) * (R / 2 ^ i) ^ n ≤ μ.real (ball y (Real.sqrt t)) ∧
        μ.real (ball y (Real.sqrt t)) ≤ ((3 / 2 : ℝ) * omega) * (R / 2 ^ i) ^ n := by
…

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.gamma_bound_on_smaller_ball line 57
Source documentation
The bounded representative in the local Bochner construction supplies the original-frame Gamma bound on every smaller working ball.
```
theorem LocalHarmonicEnergy.gamma_bound_on_smaller_ball {n : ℕ}
    {U : Euclidean n →L[ℝ] SobolevSpace μ hQ}
    {M : PositiveBilinearMeasure X (Euclidean n)} {κ r R : ℝ} {L : ℝ≥0} {p : X}
    (G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p r L v) (hR : R ≤ 2 * r)
    (v : Euclidean n) :
    ∀ᵐ x ∂μ.restrict (ball p R), localGamma μ hQ (U v) (U v) x ≤ (L : ℝ) ^ 2 * ‖v‖ ^ 2 := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.localGamma