BoundedDensityGaussian.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Gaussian source bounds for the bounded curvature density

theorem OAI.RegularPointCoordinates.integral_bounded_density_gaussian_le line 17

Source documentation

Bounded densities supported on the working ball consume only its Gaussian volume moment. This will be applied to the curvature density.

theorem integral_bounded_density_gaussian_le (n : ℕ) (x : X)
    {s R α D V B : ℝ} (hs : 0 < s) (hα : 0 ≤ α) (hD : 0 < D)
    (hV : 0 ≤ V) (hB : 0 ≤ B) (N : ℕ) (hroot : (2 : ℝ) ^ N * s = R)
    {k g : X → ℝ} (hg : ∀ᵐ z ∂μ, |g z| ≤ B)
    (hzero : ∀ᵐ z ∂μ, z ∉ ball x R → g z = 0)
    (hkernel : ∀ z ∈ ball x R, |k z| ≤ α / s ^ n * Real.exp (-(dist x z) ^ 2 / (D * s ^ 2)))
    (hvolume : ∀ j ≤ N, μ.real (ball x (2 ^ j * s)) ≤ V * (2 ^ j * s) ^ n) :
    |∫ z, k z * g z ∂μ| ≤ α * B * V * gaussianVolumeMomentConstant n D⁻¹ := by
…

Mentions: OAI.RegularPointCoordinates.gaussianVolumeMomentConstant