ScaledGaussianTail.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Off-diagonal decay at a fixed relative scale

theorem OAI.RegularPointCoordinates.inverse_power_sqrt line 14
theorem OAI.RegularPointCoordinates.gaussian_envelope_scale line 22

theorem OAI.RegularPointCoordinates.HasCoordinateHeatBounds.scaled_off_diagonal_small line 49

Source documentation

The small relative time is chosen before the physical radius.

theorem HasCoordinateHeatBounds.scaled_off_diagonal_small
    (hg : HasCoordinateHeatBounds μ ker)
    (hnonneg : ∀ t, 0 < t → ∀ x y, 0 ≤ ker t x y)
    (n : ℕ) {c V η : ℝ} (hc : 0 < c) (hV : 0 < V) (hη : 0 < η) :
    ∃ δ : ℝ, 0 < δ ∧ δ ≤ 1 ∧ ∀ R, 0 < R → R ≤ 1 →
      ∀ t, 0 < t → t < δ * R ^ 2 → ∀ x y,
      c * R ≤ dist x y →
      V * (Real.sqrt t) ^ n ≤ μ.real (ball y (Real.sqrt t)) →
      R ^ n * |ker t x y| ≤ η := by
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds