Phase functions

This module formalizes the definitions from Section 4.1 of the ANTEDB blueprint. A phase function is smooth on [1, 2]. A model phase function is a variable family of phase functions whose successive derivatives asymptotically agree with those of u ↦ u ^ (-σ) for some fixed positive exponent σ.

def Expdb.phaseInterval : Set ℝ

The interval on which phase functions are considered.

Equations

• Expdb.phaseInterval = Set.Icc 1 2

def Expdb.IsPhaseFunction (F : VariableFunction (VariableObject.fixed ℝ) ℝ) : Prop

A phase function is a variable real-valued function that is smooth on [1, 2] at every ambient index.

Equations

• Expdb.IsPhaseFunction F = ∀ (i : ℕ), ContDiffOn ℝ (↑⊤) (F i) Expdb.phaseInterval

noncomputable def Expdb.modelPhaseError (F : VariableFunction (VariableObject.fixed ℝ) ℝ) (σ : ℝ) (p : ℕ) : VariableFunction (VariableObject.fixed ↑phaseInterval) ℝ

The variable error function in the model phase condition at derivative order p.

Equations

• Expdb.modelPhaseError F σ p i u = iteratedDerivWithin (p + 1) (F i) Expdb.phaseInterval ↑u - iteratedDerivWithin p (fun (v : ℝ) => v ^ (-σ)) Expdb.phaseInterval ↑u

def Expdb.IsModelPhaseFunction (F : VariableFunction (VariableObject.fixed ℝ) ℝ) : Prop

A variable phase function is a model phase function when, for some fixed σ > 0, the error between its (p + 1)st derivative and the pth derivative of u ↦ u ^ (-σ) is pointwise infinitesimal for every fixed derivative order p.

Equations

• Expdb.IsModelPhaseFunction F = (Expdb.IsPhaseFunction F ∧ ∃ (σ : ℝ), 0 < σ ∧ ∀ (p : ℕ), (Expdb.modelPhaseError F σ p).IsPointwiseInfinitesimal)

noncomputable def Expdb.logPhase : VariableFunction (VariableObject.fixed ℝ) ℝ

The fixed logarithmic phase u ↦ log u, regarded as a variable family.

Equations

• Expdb.logPhase x✝ = Real.log

theorem Expdb.isModelPhaseFunction_log : IsModelPhaseFunction logPhase

The fixed logarithmic phase u ↦ log u is a model phase function, with model exponent σ = 1.

theorem Expdb.IsModelPhaseFunction.exists_subsequence_uniform_error {F : VariableFunction (VariableObject.fixed ℝ) ℝ} (hF : IsModelPhaseFunction F) (P : ℕ) : ∃ (σ : ℝ), 0 < σ ∧ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (c : VariableObject ℝ), c.IsInfinitesimal ∧ ∀ (i p : ℕ), p ≤ P → ∀ (u : ↑phaseInterval), ‖modelPhaseError F σ p (φ i) u‖ ≤ c i

For any fixed derivative cutoff, the errors of a model phase function have a common infinitesimal bound, uniform over the phase interval and all derivative orders up to the cutoff, after passing to a subsequence.