GaussianBounds.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Gaussian bounds and fixed-parameter theta convergence

def OAI.Nagata.W02.gaussianConstant line 19
theorem OAI.Nagata.W02.gaussian_exponent_le line 22
Source documentation
Completed square with a spare linear decay of slope one.
```
theorem gaussian_exponent_le (c C t : ℝ) (hc : 0 < c) :
    -c * t ^ 2 + C * t ≤ gaussianConstant c C - t := by
…
```
Mentions: OAI.Nagata.W02.gaussianConstant
theorem OAI.Nagata.W02.gaussian_exp_le line 31
Source documentation
Global explicit exponential majorant, independent of the index.
```
theorem gaussian_exp_le (c C t : ℝ) (hc : 0 < c) :
    Real.exp (-c * t ^ 2 + C * t) ≤
      Real.exp (gaussianConstant c C) * Real.exp (-t) := by
…
```
Mentions: OAI.Nagata.W02.gaussianConstant
theorem OAI.Nagata.W02.summable_pow_mul_gaussian line 39
Source documentation
Any polynomially weighted Gaussian with arbitrary linear perturbation is summable on natural numbers; the index zero is included.
```
theorem summable_pow_mul_gaussian (c C : ℝ) (N : ℕ) (hc : 0 < c) :
    Summable (fun t : ℕ => (t : ℝ) ^ N * Real.exp (-c * (t : ℝ) ^ 2 + C * t)) := by
…
```
def OAI.Nagata.W02.thetaGaussianDecay line 64
def OAI.Nagata.W02.thetaGaussianLinear line 66
def OAI.Nagata.W02.thetaGaussianMajorant line 69
theorem OAI.Nagata.W02.thetaGaussianDecay_pos line 74

theorem OAI.Nagata.W02.norm_zpow_le_exp_natAbs line 80

Source documentation

General nonzero multipliers cost only a linear exponential in |p|.

theorem norm_zpow_le_exp_natAbs (ε : ℂ) (hε : ε ≠ 0) (p : ℤ) :
    ‖ε ^ (-p)‖ ≤ Real.exp (|Real.log ‖ε‖| * (p.natAbs : ℝ)) := by
…

theorem OAI.Nagata.W02.affine_frequency_pow_le line 90

Source documentation

Affine frequency weights are absorbed into a linear exponential.

theorem affine_frequency_pow_le (A n t : ℝ) (N : ℕ)
    (hA : 0 ≤ A) (hn : 0 ≤ n) (ht : 0 ≤ t) :
    (A + n * t) ^ N ≤ (A + n) ^ N * Real.exp ((N : ℝ) * t) := by
…

theorem OAI.Nagata.W02.norm_normalizedThetaDerivativeTerm_le_gaussian line 102

Source documentation

The exact derivative summands have a disk-uniform Gaussian majorant.

theorem norm_normalizedThetaDerivativeTerm_le_gaussian
    {n a K τ R : ℝ} {ε x : ℂ} (hn : 0 < n) (hτ : 0 < τ) (hτ1 : τ < 1)
    (hε : ε ≠ 0) (hR : 0 ≤ R) (hx : ‖x‖ ≤ R) (N : ℕ) (p : ℤ) :
    ‖normalizedThetaDerivativeTerm n a K ε τ N p x‖ ≤
      thetaGaussianMajorant n a K τ R ε N p := by
…

Mentions: OAI.Nagata.W02.thetaGaussianMajorant

theorem OAI.Nagata.W02.summable_natAbs line 167
Source documentation
Transfer an absolutely summable natural sequence to symmetric integer indices.
```
theorem summable_natAbs {f : ℕ → ℝ} (hf : Summable f) :
    Summable (fun p : ℤ => f p.natAbs) := by
…
```

theorem OAI.Nagata.W02.summable_thetaGaussianMajorant line 177

Source documentation

The same explicit majorant is summable on the entire integer lattice.

theorem summable_thetaGaussianMajorant {n τ : ℝ} (hn : 0 < n)
    (hτ : 0 < τ) (hτ1 : τ < 1) (a K R : ℝ) (ε : ℂ) (N : ℕ) :
    Summable (thetaGaussianMajorant n a K τ R ε N) := by
…

Mentions: OAI.Nagata.W02.thetaGaussianMajorant

theorem OAI.Nagata.W02.summable_normalizedThetaDerivativeTerm_allTau line 188

Source documentation

Absolute summability at every point, for every fixed 0<τ<1 and ε≠0.

theorem summable_normalizedThetaDerivativeTerm_allTau
    {n a K τ : ℝ} {ε : ℂ} (hn : 0 < n) (hτ : 0 < τ) (hτ1 : τ < 1)
    (hε : ε ≠ 0) (N : ℕ) (x : ℂ) :
    Summable (fun p : ℤ => ‖normalizedThetaDerivativeTerm n a K ε τ N p x‖) := by
…

theorem OAI.Nagata.W02.tendstoUniformlyOn_normalizedThetaDerivativeSeries_allTau line 197

Source documentation

Normal convergence of actual derivative-series finite sums on every closed disk.

theorem tendstoUniformlyOn_normalizedThetaDerivativeSeries_allTau
    {n a K τ R : ℝ} {ε : ℂ} (hn : 0 < n) (hτ : 0 < τ) (hτ1 : τ < 1)
    (hε : ε ≠ 0) (hR : 0 ≤ R) (N : ℕ) :
    TendstoUniformlyOn
      (fun S : Finset ℤ => fun x => ∑ p ∈ S, normalizedThetaDerivativeTerm n a K ε τ N p x)
      (normalizedThetaDerivativeSeries n a K ε τ N) atTop {x : ℂ | ‖x‖ ≤ R} := by
…

theorem OAI.Nagata.W02.differentiable_normalizedThetaDerivativeSeries_allTau line 209

Source documentation

Every formal derivative series is entire, obtained from its actual finite sums on a disk around each point.

theorem differentiable_normalizedThetaDerivativeSeries_allTau
    {n a K τ : ℝ} {ε : ℂ} (hn : 0 < n) (hτ : 0 < τ) (hτ1 : τ < 1)
    (hε : ε ≠ 0) (N : ℕ) :
    Differentiable ℂ (normalizedThetaDerivativeSeries n a K ε τ N) := by
…

theorem OAI.Nagata.W02.differentiable_normalizedThetaSeries_allTau line 237
Source documentation
The literal source theta series is entire for every fixed allowed parameter and arbitrary nonzero multiplier, without invoking Jacobi theta.
```
theorem differentiable_normalizedThetaSeries_allTau
    {n a K τ : ℝ} {ε : ℂ} (hn : 0 < n) (hτ : 0 < τ) (hτ1 : τ < 1)
    (hε : ε ≠ 0) : Differentiable ℂ (normalizedThetaSeries n a K ε τ) := by
…
```