NeighborhoodGramEnvelope.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/ScaledNeighborhoodGram.lean:14 (same declaration text).
theorem OAI.RegularPointCoordinates.volume_half_upper line 23
Distinct definitions of this name: OAI/Geometry/RCD/Harmonic/ScaledNeighborhoodGram.lean:23 (same statement text; different proof or body). Qualify references as OAI.RegularPointCoordinates.volume_half_upper@path.

theorem OAI.RegularPointCoordinates.exists_neighborhood_gram_envelope_bound line 44

Source documentation

A single finite comparison constant works at all nearby heat poles and all sufficiently small testing balls, using the same harmonic data.

theorem exists_neighborhood_gram_envelope_bound (hg : HasCoordinateHeatBounds μ ker)
    (hdiff : HasGaussianHeatDifferenceBounds μ ker) (hR : 0 < R) (hR1 : R ≤ 1)
    (homega : 0 < omega)
    (hvolume : ∀ y, dist p y ≤ 16 * R → ∀ s, 0 < s → s ≤ 32 * R →
      |μ.real (ball y s) / (omega * s ^ (m + 2)) - 1| ≤ 1 / 2)
    {A : ℝ} (hA : 0 ≤ A) (lambda : ℝ) :
    ∃ C : ℝ, 0 < C ∧ ∃ J : ℕ, ∀ i, J ≤ i → ∀ x ∈ ball p (R / 32),
      ∀ q, dist x q ≤ A * (R / 2 ^ i) → ∀ v : Euclidean (m + 2),
      |⟪v, (sobolevMeanGram μ hQ U (ball q (R / 2 ^ i)) measurableSet_ball -
        cutoffHeatGram μ hQ hk χ.weight.continuous (χ.hasCompactSupport μ hQ)
          U (sq_pos_of_pos (div_pos hR (pow_pos (by norm_num : (0 : ℝ) < 2) i))) x lambda) v⟫_ℝ| ≤
        C * ⟪v, dyadicBochnerEnvelope M (m + 2) x R i v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.HasGaussianHeatDifferenceBounds, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.cutoffHeatGram, OAI.RegularPointCoordinates.dyadicBochnerEnvelope