Phase functions

This module formalizes the phase function definitions from the blueprint's Exponential sum growth exponents chapter (beta-chapter). 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.modelPhase (σ : ℝ) : ℝ → ℝ

The reference phase u ↦ u ^ (-σ) whose derivatives a model phase follows.

Equations

• Expdb.modelPhase σ u = u ^ (-σ)

noncomputable def Expdb.modelPhaseErrorAt (F : ℝ → ℝ) (σ : ℝ) (p : ℕ) (u : ℝ) : ℝ

The fixed-data model-phase error at derivative order p.

Equations

• Expdb.modelPhaseErrorAt F σ p u = iteratedDerivWithin (p + 1) F Expdb.phaseInterval u - iteratedDerivWithin p (Expdb.modelPhase σ) Expdb.phaseInterval u

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 = Expdb.modelPhaseErrorAt (F i) σ p ↑u

@[simp]

theorem Expdb.modelPhaseError_apply (F : VariableFunction (VariableObject.fixed ℝ) ℝ) (σ : ℝ) (p i : ℕ) (u : ↑phaseInterval) : modelPhaseError F σ p i u = modelPhaseErrorAt (F i) σ p ↑u

theorem Expdb.uniqueDiffOn_phaseInterval : UniqueDiffOn ℝ phaseInterval

The phase interval has unique derivatives.

theorem Expdb.contDiffOn_modelPhase (σ : ℝ) : ContDiffOn ℝ (↑⊤) (modelPhase σ) phaseInterval

Every reference model phase is smooth on the phase interval.

theorem Expdb.iteratedDerivWithin_modelPhase (σ : ℝ) (p : ℕ) {u : ℝ} (hu : u ∈ phaseInterval) : iteratedDerivWithin p (modelPhase σ) phaseInterval u = Polynomial.eval (-σ) (descPochhammer ℝ p) * u ^ (-σ - ↑p)

The derivatives of the reference model phase have the expected falling-factorial formula on the phase interval.

theorem Expdb.norm_iteratedDerivWithin_modelPhase_le {σ : ℝ} (hσ : 0 ≤ σ) (p : ℕ) {u : ℝ} (hu : u ∈ phaseInterval) : ‖iteratedDerivWithin p (modelPhase σ) phaseInterval u‖ ≤ ‖Polynomial.eval (-σ) (descPochhammer ℝ p)‖

On [1, 2], the falling-factorial coefficient bounds the corresponding derivative of a model phase with nonnegative exponent.

theorem Expdb.continuousOn_iteratedDerivWithin_modelPhase (σ : ℝ) (p : ℕ) : ContinuousOn (iteratedDerivWithin p (modelPhase σ) phaseInterval) phaseInterval

The iterated derivatives of a reference model phase vary continuously on the phase interval.

def Expdb.IsApproximateModelPhaseFunction (F : ℝ → ℝ) (σ : ℝ) (P : ℕ) (δ : ℝ) : Prop

A fixed phase function whose model-phase errors through order P are at most δ.

Equations

• Expdb.IsApproximateModelPhaseFunction F σ P δ = (ContDiffOn ℝ (↑⊤) F Expdb.phaseInterval ∧ ∀ p ≤ P, ∀ (u : ↑Expdb.phaseInterval), ‖Expdb.modelPhaseErrorAt F σ p ↑u‖ ≤ δ)

def Expdb.HasPhaseDerivBound (F : ℝ → ℝ) (n : ℕ) (K : ℝ) : Prop

The derivatives of orders 1, …, n of F are bounded by K on the phase interval.

Equations

• Expdb.HasPhaseDerivBound F n K = ∀ (k : ℕ), 1 ≤ k → k ≤ n → ∀ u ∈ Expdb.phaseInterval, ‖iteratedDerivWithin k F Expdb.phaseInterval u‖ ≤ K

def Expdb.HasPhaseFirstDerivLowerBound (F : ℝ → ℝ) (c : ℝ) : Prop

The first derivative of F is at least c on the phase interval.

Equations

• Expdb.HasPhaseFirstDerivLowerBound F c = ∀ u ∈ Expdb.phaseInterval, c ≤ iteratedDerivWithin 1 F Expdb.phaseInterval u

theorem Expdb.HasPhaseDerivBound.of_le {F : ℝ → ℝ} {m n : ℕ} {K : ℝ} (hF : HasPhaseDerivBound F n K) (hmn : m ≤ n) : HasPhaseDerivBound F m K

A derivative bound may be restricted to a smaller order.

structure Expdb.IsModelPhaseFunctionWith (F : VariableFunction (VariableObject.fixed ℝ) ℝ) (σ : ℝ) : Prop

The data defining a model phase when its reference exponent σ has already been fixed.

• isPhaseFunction : IsPhaseFunction F

  Every member of the family is smooth on the phase interval.

• error_isChoicewiseInfinitesimal (p : ℕ) : (modelPhaseError F σ p).IsChoicewiseInfinitesimal

  Every fixed-order model-phase error is choicewise infinitesimal.

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 choicewise infinitesimal for every fixed derivative order p.

Equations

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

theorem Expdb.IsModelPhaseFunctionWith.isModelPhaseFunction {F : VariableFunction (VariableObject.fixed ℝ) ℝ} {σ : ℝ} (hF : IsModelPhaseFunctionWith F σ) (hσ : 0 < σ) : IsModelPhaseFunction F

Fixed model-phase data with a positive reference exponent gives a model phase function.

theorem Expdb.IsModelPhaseFunction.exists_with {F : VariableFunction (VariableObject.fixed ℝ) ℝ} (hF : IsModelPhaseFunction F) : ∃ (σ : ℝ), 0 < σ ∧ IsModelPhaseFunctionWith F σ

A model phase function admits fixed-exponent model-phase data.

theorem Expdb.modelPhaseErrorAt_add_linear {F : ℝ → ℝ} {σ c u : ℝ} {p : ℕ} (hF : ContDiffOn ℝ (↑⊤) F phaseInterval) (hu : u ∈ phaseInterval) : modelPhaseErrorAt (fun (x : ℝ) => F x + c * x) σ p u = modelPhaseErrorAt F σ p u + if p = 0 then c else 0

Adding a linear function changes only the zeroth model-phase error.

theorem Expdb.IsApproximateModelPhaseFunction.add_linear {F : ℝ → ℝ} {σ δ η c : ℝ} {P : ℕ} (hF : IsApproximateModelPhaseFunction F σ P δ) (hc : ‖c‖ ≤ η) : IsApproximateModelPhaseFunction (fun (u : ℝ) => F u + c * u) σ P (δ + η)

Adding a controlled linear term increases the model-phase error by at most the norm of its coefficient.

theorem Expdb.IsModelPhaseFunctionWith.add_infinitesimal_linear {F : VariableFunction (VariableObject.fixed ℝ) ℝ} {σ : ℝ} (hF : IsModelPhaseFunctionWith F σ) {c : VariableObject ℝ} (hc : c.IsInfinitesimal) : IsModelPhaseFunctionWith (fun (i : ℕ) (u : VariableObject.fixed ℝ i) => F i u + c i * u) σ

Model-phase data is stable under addition of an infinitesimal linear term.

theorem Expdb.IsModelPhaseFunctionWith.comp_affine_tendsto_id {F : VariableFunction (VariableObject.fixed ℝ) ℝ} {σ : ℝ} (hF : IsModelPhaseFunctionWith F σ) {c d : VariableObject ℝ} (hc : Filter.Tendsto c Filter.atTop (nhds 1)) (hd : Filter.Tendsto d Filter.atTop (nhds 0)) (hmap : ∀ (i : ℕ), Set.MapsTo (fun (u : ℝ) => c i * u + d i) phaseInterval phaseInterval) : IsModelPhaseFunctionWith (fun (i : ℕ) (u : VariableObject.fixed ℝ i) => F i (c i * u + d i)) σ

Model-phase data is stable under affine reparametrizations that tend to the identity and map the phase interval to itself.

theorem Expdb.IsModelPhaseFunctionWith.eventually_isApproximate {F : VariableFunction (VariableObject.fixed ℝ) ℝ} {σ : ℝ} (hF : IsModelPhaseFunctionWith F σ) (P : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (i : ℕ) in Filter.atTop, IsApproximateModelPhaseFunction (F i) σ P δ

At every fixed finite order, fixed-exponent model-phase data is eventually a uniformly approximate model phase.

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.