Exponential sum growth exponents

This module formalizes Definition 4.2 of the ANTEDB blueprint. It defines admissible model-phase bounds at a fixed scale and defines β(α) as the least such exponent.

Definition 4.2 at a glance

For α : ℝ≥0, an exponent β is admissible if every model-phase exponential sum at scale N = T ^ (α + o(1)) is bounded by T ^ (β + o(1)). We show that the admissible exponents form [β(α), ∞) and then specialize the bound to the logarithmic model phase.

Definition 4.2

def Expdb.IsPowerAsymptotic (N T : VariableObject ℝ) (α : ℝ) : Prop

N = T ^ (α + o(1)), expressed using a variable exponent that is equal to α up to an infinitesimal.

Equations

• One or more equations did not get rendered due to their size.

def Expdb.IsPowerBounded {E : Type u_1} [SeminormedAddCommGroup E] (X : VariableObject E) (T : VariableObject ℝ) (β : ℝ) : Prop

X ≪ T ^ (β + o(1)), expressed using a variable exponent that is equal to β up to an infinitesimal.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Expdb.exponentialSum (F : VariableFunction (VariableObject.fixed ℝ) ℝ) (T N : VariableObject ℝ) (a b : VariableObject ℕ) : VariableObject ℂ

The variable exponential sum ∑ n ∈ [a, b], e(T F(n / N)).

Equations

• Expdb.exponentialSum F T N a b i = ∑ n ∈ Finset.Icc (a i) (b i), ↑(Real.fourierChar (T i * F i (↑n / N i)))

def Expdb.IsExponentSumBound (α : NNReal) (β : ℝ) : Prop

The assertion that β is an admissible exponential-sum growth exponent at scale α.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Expdb.exponentSumGrowthExponent (α : NNReal) : ℝ

The exponential sum growth exponent β(α) from Definition 4.2 of the blueprint.

Equations

• Expdb.exponentSumGrowthExponent α = sInf {β : ℝ | Expdb.IsExponentSumBound α β}

Power asymptotics

theorem Expdb.IsPowerAsymptotic.eventually_between {N T : VariableObject ℝ} {α ε : ℝ} (hNT : IsPowerAsymptotic N T α) (hT : ∀ᶠ (i : ℕ) in Filter.atTop, 1 ≤ T i) (hε : 0 < ε) : ∀ᶠ (i : ℕ) in Filter.atTop, T i ^ (α - ε) ≤ N i ∧ N i ≤ T i ^ (α + ε)

If N = T ^ (α + o(1)), then N eventually lies between the powers with exponents α - ε and α + ε.

Power bounds

theorem Expdb.isPowerBounded_iff_forall_pos {E : Type u_1} [SeminormedAddCommGroup E] (X : VariableObject E) (T : VariableObject ℝ) (β : ℝ) (hT : ∀ (i : ℕ), 1 ≤ T i) (hTunbounded : T.IsUnbounded) : IsPowerBounded X T β ↔ ∀ (ε : ℝ), 0 < ε → X =O[Filter.atTop] fun (i : ℕ) => T i ^ (β + ε)

If T is at least one and unbounded, then X ≪ T ^ (β + o(1)) iff X = O(T ^ (β + ε)) for every fixed ε > 0.

Admissible exponents

The candidate set is upward closed, nonempty, and bounded below.

Monotonicity

theorem Expdb.IsExponentSumBound.mono {α : NNReal} {β γ : ℝ} (hβ : IsExponentSumBound α β) (hβγ : β ≤ γ) : IsExponentSumBound α γ

Admissible exponential-sum bounds are monotone in the exponent.

Nonemptiness and lower bound

theorem Expdb.isExponentSumBound_self (α : NNReal) : IsExponentSumBound α ↑α

The triangle inequality gives the admissible exponent α.

theorem Expdb.IsExponentSumBound.nonneg {α : NNReal} {β : ℝ} (hβ : IsExponentSumBound α β) : 0 ≤ β

Every admissible exponent at a nonnegative scale is nonnegative.

The least admissible exponent

theorem Expdb.isExponentSumBound_exponentSumGrowthExponent (α : NNReal) : IsExponentSumBound α (exponentSumGrowthExponent α)

By underspill, the infimum of the admissible exponents is itself admissible.

theorem Expdb.exponentSumGrowthExponent_le_iff {α : NNReal} {β : ℝ} : exponentSumGrowthExponent α ≤ β ↔ IsExponentSumBound α β

The defining universal property of the exponential sum growth exponent.

theorem Expdb.isLeast_exponentSumGrowthExponent (α : NNReal) : IsLeast {β : ℝ | IsExponentSumBound α β} (exponentSumGrowthExponent α)

The exponent sum growth exponent is the least admissible exponent.

theorem Expdb.exponentSumBounds_eq_Ici (α : NNReal) : {β : ℝ | IsExponentSumBound α β} = Set.Ici (exponentSumGrowthExponent α)

At scale α, the admissible exponents form the interval [β(α), ∞).

theorem Expdb.isClosed_exponentSumBounds (α : NNReal) : IsClosed {β : ℝ | IsExponentSumBound α β}

The set of admissible exponential-sum exponents at scale α is closed.

Logarithmic model phase

theorem Expdb.isPowerBounded_logPhase (α : NNReal) {N T : VariableObject ℝ} {a b : VariableObject ℕ} (hN : ∀ (i : ℕ), 1 ≤ N i) (hT : ∀ (i : ℕ), 1 ≤ T i) (hTunbounded : T.IsUnbounded) (hNT : IsPowerAsymptotic N T ↑α) (hab : ∀ (i : ℕ), N i ≤ ↑(a i) ∧ ↑(b i) ≤ 2 * N i) : IsPowerBounded (exponentialSum logPhase T N a b) T (exponentSumGrowthExponent α)

The least admissible exponent bounds the logarithmic model-phase sum.