GaussianMassEnvelope.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Geometric envelopes for the finite Gaussian mass convolution

def OAI.RegularPointCoordinates.gaussianMassConvolutionConstant line 15
Source documentation
The fixed three-quarter decay is compatible with the proved slow inverse growth, and dominates every Gaussian shell coefficient.
```
def gaussianMassConvolutionConstant (m : ℕ) (c : ℝ) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.gaussianMassConvolutionConstant_nonneg line 18
theorem OAI.RegularPointCoordinates.gaussian_mass_coefficient_le line 26
Source documentation
The dimension is m+2, so the scaled mass costs 2^(m j) on the jth outward shell. The remaining Gaussian gives a uniform geometric kernel.
```
theorem gaussian_mass_coefficient_le (m : ℕ) {c : ℝ} (hc : 0 < c) (j : ℕ) :
    ((2 : ℝ) ^ m) ^ j * gaussianShellFactor c j ≤
      gaussianMassConvolutionConstant m c * (3 / 4 : ℝ) ^ j := by
…
```
Mentions: OAI.RegularPointCoordinates.gaussianShellFactor, OAI.RegularPointCoordinates.gaussianMassConvolutionConstant

theorem OAI.RegularPointCoordinates.scaled_mass_dyadic_identity line 42

Source documentation

Exact cancellation of the scale factors in a dimension m+2 mass.

theorem scaled_mass_dyadic_identity (m j : ℕ) {r : ℝ} (hr : 0 < r) (v : ℝ) :
    (r ^ 2 / r ^ (m + 2)) * v =
      ((2 : ℝ) ^ m) ^ j * (((2 ^ j * r) ^ 2 / (2 ^ j * r) ^ (m + 2)) * v) := by
…