HarmonicEndpointBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The terminal heat value in the actual Gram comparison

theorem OAI.RegularPointCoordinates.exists_harmonic_endpoint_bound line 24

Source documentation

At the fixed terminal time R², the genuine bounded cutoff energy acquires the averaging displacement ratio r/R.

theorem exists_harmonic_endpoint_bound (hg : HasCoordinateHeatBounds μ ker)
    (hdiff : HasGaussianHeatDifferenceBounds μ ker)
    (n : ℕ) {A V W : ℝ} (hA : 0 ≤ A) (hV : 0 < V) (hW : 0 ≤ W) :
    ∃ C : ℝ, 0 < C ∧ ∀ (R r : ℝ) (x q : X),
      0 < R → R ≤ 1 → 0 < r → r ≤ R / 2 →
      μ (ball q r) ≠ ∞ → 0 < μ.real (ball q r) → dist x q ≤ A * r →
      μ.real (ball x R) ≤ W * R ^ n →
      (∀ z ∈ ball x R, V * R ^ n ≤ μ.real (ball z R)) →
      ∀ (U : E →L[ℝ] SobolevSpace μ hQ) (M : PositiveBilinearMeasure X E)
        (κ : ℝ) (p : X) (s : ℝ) (L : ℝ≥0) (v : E)
        (G : LocalHarmonicEnergy μ hQ U M κ p s L v) (χ : X →ᵇ ℝ),
      (∀ z, 0 ≤ χ z ∧ χ z ≤ 1) → tsupport (χ : X → ℝ) ⊆ ball p (2 * s) →
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.HasGaussianHeatDifferenceBounds, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy