ScaledGramEnvelope.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A radius-independent bound for the actual mean/heat discrepancy

theorem OAI.RegularPointCoordinates.exists_scaled_actual_gram_envelope_bound line 26

Source documentation

The comparison constant is chosen before the physical radius and harmonic data, using normalized curvature, gradient and source bounds.

theorem exists_scaled_actual_gram_envelope_bound (m : ℕ)
    (hg : HasCoordinateHeatBounds μ ker) (hdiff : HasGaussianHeatDifferenceBounds μ ker)
    {A V W c B D Lambda : ℝ} (hA : 0 ≤ A) (hV : 0 < V) (hW : 0 ≤ W)
    (hc : 0 < c) (hB : 0 ≤ B) (hD : 0 ≤ D) (hLambda : 0 ≤ Lambda) :
    ∃ C : ℝ, 0 < C ∧ ∀ (R : ℝ) (hR : 0 < R), R ≤ 1 →
      ∀ (U : Euclidean (m + 2) →L[ℝ] SobolevSpace μ hQ)
        (M : PositiveBilinearMeasure X (Euclidean (m + 2)))
        (κ : ℝ) (p : X) (r₀ : ℝ) (L : ℝ≥0)
        (G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p r₀ L v)
        (ρ C₀ : ℝ) (χ : GoodLaplacianCutoff μ hQ p ρ C₀),
      0 < ρ → ρ < r₀ → (L : ℝ) ^ 2 ≤ B → |κ| * R ^ 2 ≤ 1 →
      (∀ w : Euclidean (m + 2), ‖w‖ ≤ 2 → R ^ 2 *
…

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