HeatExteriorDecay.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Geometric decay of the exterior term in the actual heat increment

theorem OAI.RegularPointCoordinates.gaussianShellFactor_succ_le line 12
Source documentation
The Gaussian shell factor decreases with the outward shell index.
```
theorem gaussianShellFactor_succ_le {c : ℝ} (hc : 0 ≤ c) (j : ℕ) :
    gaussianShellFactor c (j + 1) ≤ gaussianShellFactor c j := by
…
```
Mentions: OAI.RegularPointCoordinates.gaussianShellFactor
theorem OAI.RegularPointCoordinates.gaussian_exterior_coefficient_le line 27
Source documentation
The exterior Gaussian uses the next shell and thus satisfies the same fixed geometric coefficient bound.
```
theorem gaussian_exterior_coefficient_le (m : ℕ) {D : ℝ} (hD : 0 < D) (j : ℕ) :
    ((2 : ℝ) ^ m) ^ j * Real.exp (-(4 : ℝ) ^ j / D) ≤
      gaussianMassConvolutionConstant m D⁻¹ * (3 / 4 : ℝ) ^ j := by
…
```
Mentions: OAI.RegularPointCoordinates.gaussianMassConvolutionConstant

theorem OAI.RegularPointCoordinates.heat_exterior_term_le_geometric line 40

Source documentation

A fixed outer radius converts the exterior source term into a geometrically decaying background term, with no residual inverse fine scale.

theorem heat_exterior_term_le_geometric (m N : ℕ) {s R A D M : ℝ}
    (hs : 0 < s) (hA : 0 ≤ A) (hD : 0 < D) (hM : 0 ≤ M)
    (hR : (2 : ℝ) ^ N * s = R) :
    s ^ 2 * ((A / s ^ (m + 2)) * Real.exp (-(4 : ℝ) ^ N / D)) * M ≤
      (A * gaussianMassConvolutionConstant m D⁻¹ * (R ^ 2 / R ^ (m + 2)) * M) *
        (3 / 4 : ℝ) ^ N := by
…

Mentions: OAI.RegularPointCoordinates.gaussianMassConvolutionConstant