GaussianUpperEnvelope.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Coarse Gaussian envelopes needed for short heat differences

theorem OAI.RegularPointCoordinates.HasGaussianHeatBounds.upper_five line 16

Source documentation

Fix one sufficient Gaussian denominator for the application.

theorem HasGaussianHeatBounds.upper_five (hg : HasGaussianHeatBounds μ ker) :
    ∃ C B : ℝ, 0 < C ∧ 0 ≤ B ∧ ∀ t, 0 < t → ∀ x y,
      ker t x y ≤ C/μ.real (ball y (Real.sqrt t))*
        Real.exp (-dist x y^2/(5*t)+B*t) := by
…

Mentions: OAI.RegularPointCoordinates.HasGaussianHeatBounds

theorem OAI.RegularPointCoordinates.gaussian_upper_local line 37

Source documentation

On a ball of twice the heat length, a Gaussian is bounded by a Gaussian at its center with a coarser denominator.

theorem gaussian_upper_local {t C B V : ℝ} (ht : 0 < t) (hC : 0 ≤ C) (hV : 0 < V)
    (x z y : X) (hxy : dist x y ≤ 2*Real.sqrt t) :
    C/V*Real.exp (-dist y z^2/(5*t)+B*t) ≤
      C*Real.exp 1/V*Real.exp (-dist x z^2/(10*t)+B*t) := by
…