OAI/Geometry/RCD/Heat/SupportedGaussianVolume.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.supported_gaussian_integral_le line 19

   Source documentation

   A compactly supported Gaussian source is controlled by upper volume bounds in the original metric, with no global volume hypothesis.

   theorem supported_gaussian_integral_le (n : ℕ) (x : X)
       {s R C D V : ℝ} (hs : 0 < s) (hC : 0 ≤ C) (hD : 0 < D) (hV : 0 ≤ V)
       (N : ℕ) (hroot : (2 : ℝ) ^ N * s = R) {f : X → ℝ} (hf : Integrable f μ)
       (hpoint : ∀ z, f z ≤ C / s ^ n * Real.exp (-(dist x z) ^ 2 / (D * s ^ 2)))
       (hzero : ∀ z ∉ ball x R, f z = 0)
       (hvolume : ∀ j ≤ N, μ.real (ball x (2 ^ j * s)) ≤ V * (2 ^ j * s) ^ n) :
       (∫ z, f z ∂μ) ≤ C * V * gaussianVolumeMomentConstant n D⁻¹ := by
   …

   Mentions: OAI.RegularPointCoordinates.gaussianVolumeMomentConstant