Project-specific asymptotic notation

This module formalizes the infinitesimal equality and comparison relations and the underspill principle from Chapter 2 of the ANTEDB blueprint. The notations X =o Y and X ≤o Y are available after open scoped Expdb.

The blueprint also uses non-standard objects indexed by an ambient natural-number parameter. These are represented by VariableObject. Their asymptotic properties are encoded in the VariableObject namespace.

Variable functions whose domain type may depend on the ambient parameter are represented by VariableFunction. Their pointwise asymptotic properties are encoded in the VariableFunction namespace.

@[reducible, inline]

abbrev Expdb.VariableObject (α : Type u) : Type u

A family indexed by the ambient natural-number parameter.

Equations

• Expdb.VariableObject α = (ℕ → α)

@[reducible, inline]

abbrev Expdb.VariableFunction (domain : VariableObject (Type u)) (codomain : Type v) : Type (max u v)

A family of functions whose domain may depend on the ambient natural-number parameter.

Equations

• Expdb.VariableFunction domain codomain = ((i : ℕ) → domain i → codomain)

@[reducible, inline]

abbrev Expdb.VariableObject.fixed {α : Type u} (x : α) : VariableObject α

The constant variable object with value x.

Equations

• Expdb.VariableObject.fixed x x✝ = x

def Expdb.VariableObject.IsBounded {α : Type u} [SeminormedAddCommGroup α] (X : VariableObject α) : Prop

A variable object whose norm is eventually bounded by a fixed constant.

Equations

• X.IsBounded = ∃ (C : ℝ), ∀ᶠ (i : ℕ) in Filter.atTop, ‖X i‖ ≤ C

def Expdb.VariableObject.IsUnbounded {α : Type u} [SeminormedAddCommGroup α] (X : VariableObject α) : Prop

A variable object whose norm tends to infinity.

Equations

• X.IsUnbounded = Filter.Tendsto (fun (i : ℕ) => ‖X i‖) Filter.atTop Filter.atTop

theorem Expdb.VariableObject.isUnbounded_iff_forall_eventually_norm_ge {α : Type u} [SeminormedAddCommGroup α] (X : VariableObject α) : X.IsUnbounded ↔ ∀ (C : ℝ), ∀ᶠ (i : ℕ) in Filter.atTop, C ≤ ‖X i‖

A variable object is unbounded iff its norm eventually exceeds every fixed threshold.

def Expdb.VariableObject.IsInfinitesimal {α : Type u} [SeminormedAddCommGroup α] (X : VariableObject α) : Prop

A variable object whose norm tends to zero.

Equations

• X.IsInfinitesimal = Filter.Tendsto (fun (i : ℕ) => ‖X i‖) Filter.atTop (nhds 0)

theorem Expdb.VariableObject.isInfinitesimal_iff_forall_pos {α : Type u} [SeminormedAddCommGroup α] (X : VariableObject α) : X.IsInfinitesimal ↔ ∀ (δ : ℝ), 0 < δ → ∀ᶠ (i : ℕ) in Filter.atTop, ‖X i‖ < δ

A variable object is infinitesimal iff its norm is eventually below every positive tolerance.

def Expdb.VariableFunction.IsPointwiseBounded {domain : VariableObject (Type u)} {α : Type v} [SeminormedAddCommGroup α] (f : VariableFunction domain α) : Prop

A variable function that is bounded along every variable choice. The choice may vary with the ambient index; it is not a fixed point of the domain.

Equations

• f.IsPointwiseBounded = ∀ (x : (i : ℕ) → domain i), Expdb.VariableObject.IsBounded fun (i : ℕ) => f i (x i)

def Expdb.VariableFunction.IsPointwiseInfinitesimal {domain : VariableObject (Type u)} {α : Type v} [SeminormedAddCommGroup α] (f : VariableFunction domain α) : Prop

A variable function that is infinitesimal along every variable choice. The choice may vary with the ambient index; it is not a fixed point of the domain.

Equations

• f.IsPointwiseInfinitesimal = ∀ (x : (i : ℕ) → domain i), Expdb.VariableObject.IsInfinitesimal fun (i : ℕ) => f i (x i)

def Expdb.IsEqUpToInfinitesimal {E : Type u} [SeminormedAddCommGroup E] (X Y : VariableObject E) : Prop

The relation X = Y + o(1), meaning that X - Y is infinitesimal.

Equations

• Expdb.IsEqUpToInfinitesimal X Y = (X - Y).IsInfinitesimal

def Expdb.IsLEUpToInfinitesimal (X Y : VariableObject ℝ) : Prop

The relation X ≤ Y + o(1), meaning that the positive part of X - Y is infinitesimal.

Equations

• Expdb.IsLEUpToInfinitesimal X Y = Expdb.VariableObject.IsInfinitesimal fun (i : ℕ) => max (X i - Y i) 0

def Expdb.«term_=o_» : Lean.TrailingParserDescr

X =o Y denotes X = Y + o(1), not the little-o relation X = o(Y).

Equations

• Expdb.«term_=o_» = Lean.ParserDescr.trailingNode `Expdb.«term_=o_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =o ") (Lean.ParserDescr.cat `term 51))

def Expdb.«term_≤o_» : Lean.TrailingParserDescr

X ≤o Y denotes X ≤ Y + o(1).

Equations

• Expdb.«term_≤o_» = Lean.ParserDescr.trailingNode `Expdb.«term_≤o_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤o ") (Lean.ParserDescr.cat `term 51))

theorem Expdb.IsEqUpToInfinitesimal.refl {E : Type u} [SeminormedAddCommGroup E] (X : VariableObject E) : IsEqUpToInfinitesimal X X

The relation =o is reflexive.

theorem Expdb.IsEqUpToInfinitesimal.symm {E : Type u} [SeminormedAddCommGroup E] {X Y : VariableObject E} (h : IsEqUpToInfinitesimal X Y) : IsEqUpToInfinitesimal Y X

The relation =o is symmetric.

theorem Expdb.IsEqUpToInfinitesimal.trans {E : Type u} [SeminormedAddCommGroup E] {X Y Z : VariableObject E} (hXY : IsEqUpToInfinitesimal X Y) (hYZ : IsEqUpToInfinitesimal Y Z) : IsEqUpToInfinitesimal X Z

The relation =o is transitive.

theorem Expdb.IsEqUpToInfinitesimal.neg {E : Type u} [SeminormedAddCommGroup E] {X Y : VariableObject E} (h : IsEqUpToInfinitesimal X Y) : IsEqUpToInfinitesimal (-X) (-Y)

The relation =o is preserved by negation.

theorem Expdb.IsEqUpToInfinitesimal.add {E : Type u} [SeminormedAddCommGroup E] {X₁ X₂ Y₁ Y₂ : VariableObject E} (h₁ : IsEqUpToInfinitesimal X₁ Y₁) (h₂ : IsEqUpToInfinitesimal X₂ Y₂) : IsEqUpToInfinitesimal (X₁ + X₂) (Y₁ + Y₂)

The relation =o is preserved by addition.

theorem Expdb.IsEqUpToInfinitesimal.sub {E : Type u} [SeminormedAddCommGroup E] {X₁ X₂ Y₁ Y₂ : VariableObject E} (h₁ : IsEqUpToInfinitesimal X₁ Y₁) (h₂ : IsEqUpToInfinitesimal X₂ Y₂) : IsEqUpToInfinitesimal (X₁ - X₂) (Y₁ - Y₂)

The relation =o is preserved by subtraction.

theorem Expdb.IsEqUpToInfinitesimal.const_smul {𝕜 : Type u} {F : Type v} [NormedField 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {X Y : VariableObject F} (h : IsEqUpToInfinitesimal X Y) (c : 𝕜) : IsEqUpToInfinitesimal (c • X) (c • Y)

The relation =o is preserved by multiplication by a fixed scalar.

theorem Expdb.isEqUpToInfinitesimal_iff_forall_pos {E : Type u} [SeminormedAddCommGroup E] (X Y : VariableObject E) : IsEqUpToInfinitesimal X Y ↔ ∀ (δ : ℝ), 0 < δ → ∀ᶠ (i : ℕ) in Filter.atTop, ‖X i - Y i‖ < δ

X =o Y iff X and Y are eventually within every positive tolerance.

theorem Expdb.isLEUpToInfinitesimal_iff_forall_pos (X Y : VariableObject ℝ) : IsLEUpToInfinitesimal X Y ↔ ∀ (δ : ℝ), 0 < δ → ∀ᶠ (i : ℕ) in Filter.atTop, X i ≤ Y i + δ

X ≤o Y iff X i ≤ Y i + δ eventually for every δ > 0.

theorem Expdb.isEqUpToInfinitesimal_iff_leUpToInfinitesimal (X Y : VariableObject ℝ) : IsEqUpToInfinitesimal X Y ↔ IsLEUpToInfinitesimal X Y ∧ IsLEUpToInfinitesimal Y X

For real variable objects, X =o Y iff X ≤o Y and Y ≤o X.

theorem Expdb.underspill (X Y : VariableObject ℝ) : IsLEUpToInfinitesimal X Y ↔ ∀ ε > 0, IsLEUpToInfinitesimal X fun (i : ℕ) => Y i + ε

Underspill principle. The relation X ≤ Y + o(1) holds if and only if X ≤ Y + ε + o(1) for every fixed ε > 0.