GaussianGradientAlgebra.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Scalar constants in the Gaussian gradient estimate

theorem OAI.RegularPointCoordinates.gaussian_gradient_algebra line 11

Source documentation

The local square estimate from reverse Poincaré gives a Gaussian bound for the gradient, with one uniform enlarged coefficient.

theorem gaussian_gradient_algebra {C D V t r k B d g : ℝ}
    (hC : 0 < C) (hD : 1 ≤ D) (hV : 0 < V) (ht : 0 < t) (hr : 0 < r)
    (hr2 : r^2 = t) (hk : 0 ≤ k)
    (hg : (t*Real.exp (-k*t))*g^2 ≤
      (C*D/V*Real.exp (B*t))*(C*Real.exp 1/V*Real.exp (-d^2/(10*t)+B*t))) :
    g ≤ (C*D*Real.exp 1/(r*V))*Real.exp (-d^2/(20*t)+(B+k)*t) := by
…

theorem OAI.RegularPointCoordinates.gaussian_amplitude_algebra line 54

Source documentation

The same envelope dominates the local amplitude.

theorem gaussian_amplitude_algebra {C D V t k B d : ℝ}
    (hC : 0 < C) (hD : 1 ≤ D) (hV : 0 < V) (ht : 0 < t) (hk : 0 ≤ k) :
    C*Real.exp 1/V*Real.exp (-d^2/(10*t)+B*t) ≤
      C*D*Real.exp 1/V*Real.exp (-d^2/(20*t)+(B+k)*t) := by
…

theorem OAI.RegularPointCoordinates.gaussian_cutoff_factor line 70

Source documentation

The cutoff coefficient has exactly the required heat-length scaling.

theorem gaussian_cutoff_factor {A E r V : ℝ} (hA : 0 ≤ A) (hE : 0 ≤ E)
    (hr : 0 < r) (hV : 0 < V) :
    Real.sqrt (2*(A/(r*V)*E)^2+2*(A/V*E)^2*(r⁻¹)^2) =
      2*A/(r*V)*E := by
…