UniformHeatBase.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite starting bounds for actual regularized heat metrics

theorem OAI.RegularPointCoordinates.positive_equiv_norm_bounds line 18

Source documentation

Scalar lower and upper bounds control a positive metric and its inverse.

theorem positive_equiv_norm_bounds (Q : E ≃L[ℝ] E)
    (hQ : (Q : E →L[ℝ] E).IsPositive) {a L : ℝ} (ha : 0 < a) (hL : 0 ≤ L)
    (hlow : ∀ v, a * ‖v‖ ^ 2 ≤ ⟪v, Q v⟫_ℝ)
    (hupp : ∀ v, ⟪v, Q v⟫_ℝ ≤ L * ‖v‖ ^ 2) :
    ‖(Q : E →L[ℝ] E)‖ ≤ L ∧ ‖(Q.symm : E →L[ℝ] E)‖ ≤ a⁻¹ := by
…

theorem OAI.RegularPointCoordinates.exists_uniform_dyadic_heat_base line 45
Source documentation
One root-time constant bounds every pole, because the cutoff energy has unit heat mass and the same strictly positive scalar regularizer.
```
theorem exists_uniform_dyadic_heat_base {n : ℕ}
    {U : Euclidean n →L[ℝ] SobolevSpace μ hQ}
    {M : PositiveBilinearMeasure X (Euclidean n)} {κ r R lambda ρ C : ℝ}
    {p : X} {L : ℝ≥0}
    (G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : GoodLaplacianCutoff μ hQ p ρ C) (hρr : ρ < r)
    (hR : 0 < R) (hlambda : 0 < lambda) (J : ℕ) :
    ∃ T : ℝ, 0 < T ∧ ∀ x v,
      let Q := dyadicHeatGramAt μ hQ hk U χ x hR hlambda J
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.dyadicHeatGramAt