Exponential Decay Lemmas

This file contains lemmas about exponential decay that are used in the RH criterion proof. These are standard results from real analysis about the behavior of exp(-x²) as x → ∞.

theorem Frourio.exp_neg_sq_tendsto_zero (c : ℝ) (hc : 0 < c) : Filter.Tendsto (fun (n : ℕ) => Real.exp (-c * ↑n ^ 2)) Filter.atTop (nhds 0)

The key property: exp(-cx²) → 0 faster than any polynomial as x → ∞

theorem Frourio.tendsto_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {x : Filter α} {y : Filter β} {z : Filter γ} (hg : Filter.Tendsto g y z) (hf : Filter.Tendsto f x y) : Filter.Tendsto (g ∘ f) x z

theorem Frourio.exponential_decay_bound (ε : ℝ) (hε : 0 < ε) : ∃ (N : ℕ), ∀ n ≥ N, 4 * Real.exp (-Real.pi * ε ^ 2 * (↑n + 1) ^ 2) < ε

For any ε > 0, there exists N such that for all n ≥ N, 4 * exp(-π ε² (n+1)²) < ε. This captures the super-exponential decay of the Gaussian function.

theorem Frourio.exponential_decay_bound_reciprocal (ε : ℝ) (hε : 0 < ε) : ∃ (δ₀ : ℝ), 0 < δ₀ ∧ ∀ (δ : ℝ), 0 < δ → δ ≤ δ₀ → 4 * Real.exp (-Real.pi * ε ^ 2 / δ ^ 2) < ε

Alternative formulation controlling the reciprocal width parameter δ. For sufficiently small positive δ, the Gaussian tail becomes smaller than ε.

theorem Frourio.gaussian_tail_bound (ε : ℝ) (hε : 0 < ε) : ∃ (N : ℕ), ∀ n ≥ N, let δ := 1 / (↑n + 1); 4 * Real.exp (-Real.pi * ε ^ 2 / δ ^ 2) < ε

For Gaussian decay with parameter depending on 1/(n+1)

theorem Frourio.general_exponential_bound (A B ε : ℝ) (hB : 0 < B) (hε : 0 < ε) : ∃ (N : ℕ), ∀ n ≥ N, A * Real.exp (-B * ↑n ^ 2) < ε

General exponential bound: for any A > 0 and B > 0, A * exp(-B * n²) eventually becomes smaller than any ε > 0