ActualGramEnvelope.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual mean/heat discrepancy is controlled by the full mass envelope

theorem OAI.RegularPointCoordinates.exists_actual_gram_envelope_bound line 30

Source documentation

All three source components and the terminal value are estimated here for the same genuine harmonic map, cutoff, kernel and full Bochner measure.

theorem exists_actual_gram_envelope_bound (hg : HasCoordinateHeatBounds μ ker)
    (hdiff : HasGaussianHeatDifferenceBounds μ ker) (hρ : 0 < ρ) (hρr : ρ < r₀)
    {A V W δ R : ℝ} (hA : 0 ≤ A) (hV : 0 < V) (hW : 0 ≤ W)
    (hδ : 0 < δ) (hR : 0 < R) (hR1 : R ≤ 1) (lambda : ℝ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (i : ℕ), 1 ≤ i → ∀ (x q : X),
      μ (ball q (R / 2 ^ i)) ≠ ∞ →
      V * (R / 2 ^ i) ^ (m + 2) ≤ μ.real (ball q (R / 2 ^ i)) →
      dist x q ≤ A * (R / 2 ^ i) →
      (∀ j, μ.real (ball x (R / 2 ^ j)) ≤ W * (R / 2 ^ j) ^ (m + 2)) →
      (∀ t, 0 < t → t ≤ R ^ 2 → ∀ z ∈ ball x R,
        V * (Real.sqrt t) ^ (m + 2) ≤ μ.real (ball z (Real.sqrt t))) →
      closedBall p (2 * ρ) ⊆ ball x R →
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.HasGaussianHeatDifferenceBounds