ScaledNeighborhoodGram.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

One source-comparison constant throughout the regular neighborhood

theorem OAI.RegularPointCoordinates.volume_half_lower line 14
Also declared: OAI/Geometry/RCD/Harmonic/NeighborhoodGramEnvelope.lean:14 (same declaration text).
theorem OAI.RegularPointCoordinates.volume_half_upper line 23
Distinct definitions of this name: OAI/Geometry/RCD/Harmonic/NeighborhoodGramEnvelope.lean:23 (same statement text; different proof or body). Qualify references as OAI.RegularPointCoordinates.volume_half_upper@path.

theorem OAI.RegularPointCoordinates.exists_scaled_neighborhood_gram_envelope_bound line 39

Source documentation

The comparison constant and first admissible index precede the choice of radius, harmonic map and its full Bochner measure.

theorem exists_scaled_neighborhood_gram_envelope_bound (m : ℕ)
    (hg : HasCoordinateHeatBounds μ ker) (hdiff : HasGaussianHeatDifferenceBounds μ ker)
    {omega A B D Lambda : ℝ} (homega : 0 < omega) (hA : 0 ≤ A)
    (hB : 0 ≤ B) (hD : 0 ≤ D) (hLambda : 0 ≤ Lambda) :
    ∃ C : ℝ, 0 < C ∧ ∃ J : ℕ, ∀ (R : ℝ) (hR : 0 < R), R ≤ 1 →
      ∀ (U : Euclidean (m + 2) →L[ℝ] SobolevSpace μ hQ)
        (M : PositiveBilinearMeasure X (Euclidean (m + 2)))
        (κ : ℝ) (p : X) (L : ℝ≥0)
        (G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p (4 * R) L v)
        (C₀ : ℝ) (χ : GoodLaplacianCutoff μ hQ p (3 * R / 8) C₀),
      (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