OAI/Geometry/RCD/Heat/GaussianIntegralEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.scaled_integral_le_geometric_mass line 18

   Source documentation

   The geometric shell bound applies to every integrable source weight, including averaged kernels and differences of kernels.

   theorem scaled_integral_le_geometric_mass (ν : Measure X) [IsFiniteMeasure ν]
       (m : ℕ) (p : X) {r C c T : ℝ} {f : X → ℝ}
       (hr : 0 < r) (hf : Integrable f ν) (hC : 0 ≤ C) (hc : 0 < c)
       (hT : 0 ≤ T) (N : ℕ)
       (hlocal : ∀ j ≤ N, ∀ z ∈ dyadicShell p r j,
         f z ≤ (C / r ^ (m + 2)) * gaussianShellFactor c j)
       (htail : ∀ z ∉ ball p (2 ^ N * r), f z ≤ T) :
       r ^ 2 * (∫ z, f z ∂ν) ≤
         C * gaussianMassConvolutionConstant m c *
           (∑ j ∈ Finset.range (N + 1), (3 / 4 : ℝ) ^ j *
             (((2 ^ j * r) ^ 2 / (2 ^ j * r) ^ (m + 2)) *
               ν.real (ball p (2 ^ j * r)))) + r ^ 2 * T * ν.real univ := by
   …

   Mentions: OAI.RegularPointCoordinates.dyadicShell, OAI.RegularPointCoordinates.gaussianShellFactor, OAI.RegularPointCoordinates.gaussianMassConvolutionConstant