GaussianLinearGrowth.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RegularPointCoordinates.linear_sub_quadratic_le line 15
Source documentation
Completing the square leaves half of the Gaussian exponent available.
```
theorem linear_sub_quadratic_le (A s : ℝ) {c : ℝ} (hc : 0 < c) :
    A * s - c * s ^ 2 ≤ A ^ 2 / (2 * c) - (c / 2) * s ^ 2 := by
…
```
theorem OAI.RegularPointCoordinates.summable_gaussian_with_linear_growth line 25
Source documentation
A fixed exponential volume factor in the shell radius does not spoil summability of any geometric normalization loss.
```
theorem summable_gaussian_with_linear_growth {b c : ℝ} (hb : 0 ≤ b) (hc : 0 < c) (A : ℝ) :
    Summable (fun j : ℕ => b ^ j * Real.exp (A * 2 ^ j - c * 4 ^ j)) := by
…
```
theorem OAI.RegularPointCoordinates.summable_shell_with_linear_growth line 45
Source documentation
The first shell includes the pole; all later shells still allow a global hyperbolic exponential factor in their radius.
```
theorem summable_shell_with_linear_growth {b c : ℝ} (hb : 0 ≤ b) (hc : 0 < c) (A : ℝ) :
    Summable (fun j : ℕ => b ^ j * Real.exp (A * 2 ^ j) * gaussianShellFactor c j) := by
…
```
Mentions: OAI.RegularPointCoordinates.gaussianShellFactor