Multiseries definitions

In this file, we define the multiseries and its main properties: sortedness and approximation. A multiseries in a basis [b₁, ..., bₙ] represents a multivariate series: it is a formal series made from monomials b₁ ^ e₁ * ... * bₙ ^ eₙ where e₁, ..., eₙ are real numbers. We treat multivariate series in a basis [b₁, ..., bₙ] as a univariate series in the variable b₁ (basis_hd) with coefficients being multiseries in the basis [b₂, ..., bₙ] (basis_tl).

Main definitions

• Basis is the list of functions used to construct monomials in multiseries.
• Multiseries basis_hd basis_tl is the type of multiseries in a basis basis_hd :: basis_tl.
• MultiseriesExpansion basis is a multiseries expansion of some function f : ℝ → ℝ. If basis = [], then the multiseries represents a constant function, otherwise it is a pair of a multiseries ms : Multiseries basis_hd basis_tl and a function f : ℝ → ℝ.
• Multiseries.Sorted ms means that at each level of ms as a nested tree all exponents are strictly decreasing.
• MultiseriesExpansion.Approximates ms means that the multiseries ms can be used to obtain an asymptotical approximation of its attached function.

Implementation details

• Multiseries basis_hd basis_tl is defined as a Seq (ℝ × MultiseriesExpansion basis_tl), so we need to port some Seq API to Multiseries.

@[reducible, inline]

abbrev ComputeAsymptotics.Basis : Type

List of functions used to construct monomials in multiseries.

def ComputeAsymptotics.MultiseriesExpansion (basis : Basis) : Type

Multiseries representing a given function f : ℝ → ℝ. MultiseriesExpansion [] is just ℝ: multiseries representing constant functions. Otherwise it is a pair of a Multiseries basis_hd basis_tl and a function ℝ → ℝ. We call the former an expansion of the latter.

Note: most of the theory can be formulated in terms of Multiseries, but we need to explicitly store the approximated function to be able to use the eventual zeroness oracle at the trimming step.

def ComputeAsymptotics.MultiseriesExpansion.Multiseries (basis_hd : ℝ → ℝ) (basis_tl : Basis) : Type

Multiseries in a basis basis_hd :: basis_tl. It is a generalisation of asymptotic expansions. A multiseries in a basis [b₁, ..., bₙ] is a formal series made from monomials b₁ ^ e₁ * ... * bₙ ^ eₙ where e₁, ..., eₙ are real numbers. We treat multivariate series in a basis [b₁, ..., bₙ] as a univariate series in the variable b₁ (basis_hd) with coefficients being multiseries in the basis [b₂, ..., bₙ] (basis_tl). We represent such a series as a lazy list (Seq) of pairs (exp, coef) where exp is the exponent of b₁ and coef is the coefficient (a multiseries in basis_tl).

MultiseriesExpansion is a Multiseries with an attached real function.

def ComputeAsymptotics.MultiseriesExpansion.Multiseries.toSeq {basis_hd : ℝ → ℝ} {basis_tl : Basis} (ms : Multiseries basis_hd basis_tl) : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)

Converts a Multiseries basis_hd basis_tl to a Seq (ℝ × MultiseriesExpansion basis_tl).

def ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} : Multiseries basis_hd basis_tl

The empty multiseries.

def ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl) : Multiseries basis_hd basis_tl

Prepend a monomial to a multiseries.

def ComputeAsymptotics.MultiseriesExpansion.Multiseries.recOn {basis_hd : ℝ → ℝ} {basis_tl : Basis} {motive : Multiseries basis_hd basis_tl → Sort u_1} (ms : Multiseries basis_hd basis_tl) (nil : motive nil) (cons : (exp : ℝ) → (coef : MultiseriesExpansion basis_tl) → (tl : Multiseries basis_hd basis_tl) → motive (cons exp coef tl)) : motive ms

Recursion principle for Multiseries basis_hd basis_tl. It is equivalent to Stream'.Seq.recOn but provides some convenience.

def ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct {basis_hd : ℝ → ℝ} {basis_tl : Basis} (ms : Multiseries basis_hd basis_tl) : Option (ℝ × MultiseriesExpansion basis_tl × Multiseries basis_hd basis_tl)

Destruct a multiseries into a triple (exp, coef, tl), where exp is the leading exponent, coef is the leading coefficient, and tl is the tail.

def ComputeAsymptotics.MultiseriesExpansion.Multiseries.head {basis_hd : ℝ → ℝ} {basis_tl : Basis} (ms : Multiseries basis_hd basis_tl) : Option (ℝ × MultiseriesExpansion basis_tl)

The head of a multiseries, i.e. the first two entries of the tuple returned by destruct.

def ComputeAsymptotics.MultiseriesExpansion.Multiseries.tail {basis_hd : ℝ → ℝ} {basis_tl : Basis} (ms : Multiseries basis_hd basis_tl) : Multiseries basis_hd basis_tl

The tail of a multiseries, i.e. the last entry of the tuple returned by destruct.

def ComputeAsymptotics.MultiseriesExpansion.Multiseries.map {basis_hd : ℝ → ℝ} {basis_tl : Basis} {basis_hd' : ℝ → ℝ} {basis_tl' : Basis} (f : ℝ → ℝ) (g : MultiseriesExpansion basis_tl → MultiseriesExpansion basis_tl') (ms : Multiseries basis_hd basis_tl) : Multiseries basis_hd' basis_tl'

Given two functions f : ℝ → ℝ and g : MultiseriesExpansion basis_tl → MultiseriesExpansion basis_tl', apply them to exponents and coefficients of a multiseries.

def ComputeAsymptotics.MultiseriesExpansion.Multiseries.corec {β : Type u_1} {basis_hd : ℝ → ℝ} {basis_tl : Basis} (f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)) (b : β) : Multiseries basis_hd basis_tl

Corecursor for Multiseries basis_hd basis_tl.

@[implicit_reducible]

instance ComputeAsymptotics.MultiseriesExpansion.Multiseries.instInhabited (basis_hd : ℝ → ℝ) (basis_tl : Basis) : Inhabited (Multiseries basis_hd basis_tl)

@[implicit_reducible]

instance ComputeAsymptotics.MultiseriesExpansion.Multiseries.instMembershipProdReal {basis_hd : ℝ → ℝ} {basis_tl : Basis} : Membership (ℝ × MultiseriesExpansion basis_tl) (Multiseries basis_hd basis_tl)

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.eq_of_bisim {basis_hd : ℝ → ℝ} {basis_tl : Basis} {x y : Multiseries basis_hd basis_tl} (motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop) (base : motive x y) (step : ∀ (x y : Multiseries basis_hd basis_tl), motive x y → x = nil ∧ y = nil ∨ ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (x' : Multiseries basis_hd basis_tl) (y' : Multiseries basis_hd basis_tl), x = cons exp coef x' ∧ y = cons exp coef y' ∧ motive x' y') : x = y

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.eq_of_bisim_strong {basis_hd : ℝ → ℝ} {basis_tl : Basis} {x y : Multiseries basis_hd basis_tl} (motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop) (base : motive x y) (step : ∀ (x y : Multiseries basis_hd basis_tl), motive x y → x = y ∨ ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (x' : Multiseries basis_hd basis_tl) (y' : Multiseries basis_hd basis_tl), x = cons exp coef x' ∧ y = cons exp coef y' ∧ motive x' y') : x = y

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons_ne_nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} : cons exp coef tl ≠ nil

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil_ne_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} : nil ≠ cons exp coef tl

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons_eq_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp1 exp2 : ℝ} {coef1 coef2 : MultiseriesExpansion basis_tl} {tl1 tl2 : Multiseries basis_hd basis_tl} : cons exp1 coef1 tl1 = cons exp2 coef2 tl2 ↔ exp1 = exp2 ∧ coef1 = coef2 ∧ tl1 = tl2

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.corec_nil {β : Type u_1} {basis_hd : ℝ → ℝ} {basis_tl : Basis} {f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)} {b : β} (h : f b = none) : corec f b = nil

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.corec_cons {β : Type u_1} {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {next : β} {f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)} {b : β} (h : f b = some (exp, coef, next)) : corec f b = cons exp coef (corec f next)

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct_nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} : nil.destruct = none

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} : (cons exp coef tl).destruct = some (exp, coef, tl)

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct_eq_none {basis_hd : ℝ → ℝ} {basis_tl : Basis} {ms : Multiseries basis_hd basis_tl} (h : ms.destruct = none) : ms = nil

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct_eq_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {ms : Multiseries basis_hd basis_tl} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} (h : ms.destruct = some (exp, coef, tl)) : ms = cons exp coef tl

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.head_nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} : nil.head = none

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.head_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} : (cons exp coef tl).head = some (exp, coef)

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.tail_nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} : nil.tail = nil

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.tail_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} : (cons exp coef tl).tail = tl

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.map_nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} {basis_hd' : ℝ → ℝ} {basis_tl' : Basis} (f : ℝ → ℝ) (g : MultiseriesExpansion basis_tl → MultiseriesExpansion basis_tl') : map f g nil = nil

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.map_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {basis_hd' : ℝ → ℝ} {basis_tl' : Basis} (f : ℝ → ℝ) (g : MultiseriesExpansion basis_tl → MultiseriesExpansion basis_tl') {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} : map f g (cons exp coef tl) = cons (f exp) (g coef) (map f g tl)

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.map_id {basis_hd : ℝ → ℝ} {basis_tl : Basis} (ms : Multiseries basis_hd basis_tl) : map (fun (exp : ℝ) => exp) (fun (coef : MultiseriesExpansion basis_tl) => coef) ms = ms

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.map_comp {b₁ b₂ b₃ : ℝ → ℝ} {bs₁ bs₂ bs₃ : Basis} (f₁ : ℝ → ℝ) (g₁ : MultiseriesExpansion bs₁ → MultiseriesExpansion bs₂) (f₂ : ℝ → ℝ) (g₂ : MultiseriesExpansion bs₂ → MultiseriesExpansion bs₃) (ms : Multiseries b₁ bs₁) : map (f₂ ∘ f₁) (g₂ ∘ g₁) ms = map f₂ g₂ (map f₁ g₁ ms)

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.notMem_nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} {x : ℝ × MultiseriesExpansion basis_tl} : x ∉ nil

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.mem_cons_iff {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} {x : ℝ × MultiseriesExpansion basis_tl} : x ∈ cons exp coef tl ↔ x = (exp, coef) ∨ x ∈ tl

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.Pairwise_nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} {R : ℝ × MultiseriesExpansion basis_tl → ℝ × MultiseriesExpansion basis_tl → Prop} : Stream'.Seq.Pairwise R nil

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.Pairwise_cons_nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} {R : ℝ × MultiseriesExpansion basis_tl → ℝ × MultiseriesExpansion basis_tl → Prop} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} : Stream'.Seq.Pairwise R (cons exp coef nil)

def ComputeAsymptotics.MultiseriesExpansion.ofReal (c : ℝ) : MultiseriesExpansion []

Convert a real number to a multiseries in an empty basis.

def ComputeAsymptotics.MultiseriesExpansion.toReal (ms : MultiseriesExpansion []) : ℝ

Convert a multiseries in an empty basis to a real number.

def ComputeAsymptotics.MultiseriesExpansion.seq {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} (ms : MultiseriesExpansion (basis_hd :: basis_tl)) : Multiseries basis_hd basis_tl

Convert a multiseries in a non-empty basis to a sequence of pairs (exp, coef).

def ComputeAsymptotics.MultiseriesExpansion.toFun {basis : Basis} (ms : MultiseriesExpansion basis) : ℝ → ℝ

Convert a multiseries to a function.

def ComputeAsymptotics.MultiseriesExpansion.mk {basis_hd : ℝ → ℝ} {basis_tl : Basis} (s : Multiseries basis_hd basis_tl) (f : ℝ → ℝ) : MultiseriesExpansion (basis_hd :: basis_tl)

Constructs a multiseries from a Multiseries basis_hd basis_tl and a function.

def ComputeAsymptotics.MultiseriesExpansion.recOn {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} {motive : MultiseriesExpansion (basis_hd :: basis_tl) → Sort u_1} (nil : (f : ℝ → ℝ) → motive (mk Multiseries.nil f)) (cons : (exp : ℝ) → (coef : MultiseriesExpansion basis_tl) → (tl : Multiseries basis_hd basis_tl) → (f : ℝ → ℝ) → motive (mk (Multiseries.cons exp coef tl) f)) (ms : MultiseriesExpansion (basis_hd :: basis_tl)) : motive ms

Recursion principle for MultiseriesExpansion (basis_hd :: basis_tl).

@[implicit_reducible]

instance ComputeAsymptotics.MultiseriesExpansion.instInhabited (basis : Basis) : Inhabited (MultiseriesExpansion basis)

theorem ComputeAsymptotics.MultiseriesExpansion.eq_mk {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} (ms : MultiseriesExpansion (basis_hd :: basis_tl)) : ms = mk ms.seq ms.toFun

theorem ComputeAsymptotics.MultiseriesExpansion.mk_eq_mk_iff {basis_hd : ℝ → ℝ} {basis_tl : Basis} (s t : Multiseries basis_hd basis_tl) (f g : ℝ → ℝ) : mk s f = mk t g ↔ s = t ∧ f = g

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.ms_eq_mk_iff {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} (ms : MultiseriesExpansion (basis_hd :: basis_tl)) (s : Multiseries basis_hd basis_tl) (f : ℝ → ℝ) : ms = mk s f ↔ ms.seq = s ∧ ms.toFun = f

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.mk_eq_mk_iff_iff {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} (ms : MultiseriesExpansion (basis_hd :: basis_tl)) (s : Multiseries basis_hd basis_tl) (f : ℝ → ℝ) : mk s f = ms ↔ ms.seq = s ∧ ms.toFun = f

theorem ComputeAsymptotics.MultiseriesExpansion.ext_iff {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} (ms₁ ms₂ : MultiseriesExpansion (basis_hd :: basis_tl)) : ms₁ = ms₂ ↔ ms₁.seq = ms₂.seq ∧ ms₁.toFun = ms₂.toFun

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.const_toFun (ms : MultiseriesExpansion []) : ms.toFun = fun (x : ℝ) => ms.toReal

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.mk_toFun {basis_hd : ℝ → ℝ} {basis_tl : Basis} {s : Multiseries basis_hd basis_tl} {f : ℝ → ℝ} : (mk s f).toFun = f

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.mk_seq {basis_hd : ℝ → ℝ} {basis_tl : Basis} (s : Multiseries basis_hd basis_tl) (f : ℝ → ℝ) : (mk s f).seq = s

def ComputeAsymptotics.MultiseriesExpansion.replaceFun {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} (ms : MultiseriesExpansion (basis_hd :: basis_tl)) (f : ℝ → ℝ) : MultiseriesExpansion (basis_hd :: basis_tl)

Replace the function attached to a multiseries.

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.mk_replaceFun {basis_hd : ℝ → ℝ} {basis_tl : Basis} (s : Multiseries basis_hd basis_tl) (f g : ℝ → ℝ) : (mk s f).replaceFun g = mk s g

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.replaceFun_toFun {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} (ms : MultiseriesExpansion (basis_hd :: basis_tl)) (f : ℝ → ℝ) : (ms.replaceFun f).toFun = f

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.replaceFun_seq {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} (ms : MultiseriesExpansion (basis_hd :: basis_tl)) (f : ℝ → ℝ) : (ms.replaceFun f).seq = ms.seq

def ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp {basis_hd : ℝ → ℝ} {basis_tl : Basis} (s : Multiseries basis_hd basis_tl) : WithBot ℝ

The leading exponent of a multiseries with non-empty basis. For ms = [] it is ⊥.

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp_nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} : nil.leadingExp = ⊥

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} : (cons exp coef tl).leadingExp = ↑exp

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp_eq_bot {basis_hd : ℝ → ℝ} {basis_tl : Basis} (s : Multiseries basis_hd basis_tl) : s.leadingExp = ⊥ ↔ s = nil

ms.leadingExp = ⊥ iff ms = [].

def ComputeAsymptotics.MultiseriesExpansion.leadingExp {basis_hd : ℝ → ℝ} {basis_tl : Basis} (ms : MultiseriesExpansion (basis_hd :: basis_tl)) : WithBot ℝ

The leading exponent of a multiseries with non-empty basis. For ms = [] it is ⊥.

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.leadingExp_def {basis_hd : ℝ → ℝ} {basis_tl : Basis} (ms : MultiseriesExpansion (basis_hd :: basis_tl)) : ms.leadingExp = ms.seq.leadingExp

@[implicit_reducible]

def ComputeAsymptotics.MultiseriesExpansion.instPreorderProdReal {basis : Basis} : Preorder (ℝ × MultiseriesExpansion basis)

Auxiliary instance for the order on pairs (exp, coef) used below to define Sorted in terms of Stream'.Seq.Pairwise. (exp₁, coef₁) ≤ (exp₂, coef₂) iff exp₁ ≤ exp₂.

inductive ComputeAsymptotics.MultiseriesExpansion.Sorted {basis : Basis} : MultiseriesExpansion basis → Prop

A multiseries ms is Sorted when the exponents at each of its levels are sorted.

• const (ms : MultiseriesExpansion []) : ms.Sorted
• seq {hd : ℝ → ℝ} {tl : List (ℝ → ℝ)} (ms : MultiseriesExpansion (hd :: tl)) (h_coef : ∀ x ∈ ms.seq, x.2.Sorted) (h_Pairwise : Stream'.Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion tl) => x1 > x2) ms.seq) : ms.Sorted

def ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted {basis_hd : ℝ → ℝ} {basis_tl : Basis} (s : Multiseries basis_hd basis_tl) : Prop

A multiseries ms is Sorted when the exponents at each of its levels are sorted.

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.sorted_iff_seq_sorted {basis_hd : ℝ → ℝ} {basis_tl : Basis} {ms : MultiseriesExpansion (basis_hd :: basis_tl)} : ms.Sorted ↔ ms.seq.Sorted

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} : Multiseries.nil.Sorted

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.cons_nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} (h_coef : coef.Sorted) : (Multiseries.cons exp coef Multiseries.nil).Sorted

[(exp, coef)] is Sorted when coef is Sorted.

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} (h_coef : coef.Sorted) (h_comp : tl.leadingExp < ↑exp) (h_tl : tl.Sorted) : (Multiseries.cons exp coef tl).Sorted

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.elim_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} (h : (Multiseries.cons exp coef tl).Sorted) : coef.Sorted ∧ tl.leadingExp < ↑exp ∧ tl.Sorted

If cons (exp, coef) tl is Sorted, then coef and tl are Sorted, and the leading exponent of tl is less than exp.

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.tail {basis_hd : ℝ → ℝ} {basis_tl : Basis} {ms : Multiseries basis_hd basis_tl} (h : ms.Sorted) : ms.tail.Sorted

theorem ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.coind {basis_hd : ℝ → ℝ} {basis_tl : Basis} {s : Multiseries basis_hd basis_tl} (motive : Multiseries basis_hd basis_tl → Prop) (h_base : motive s) (h_step : ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl), motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl) : s.Sorted

Coinduction principle for proving Sorted. Given a predicate motive on multiseries, if motive ms holds (base case) and the predicate "survives" destruction of its argument, then ms is Sorted. Here "survives" means that if x = cons (exp, coef) tl, then motive x must imply coef.Sorted, tl.leadingExp < exp, and motive tl.

theorem ComputeAsymptotics.MultiseriesExpansion.Sorted.nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} (f : ℝ → ℝ) : (mk Multiseries.nil f).Sorted

[] is Sorted.

theorem ComputeAsymptotics.MultiseriesExpansion.Sorted.cons_nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {f : ℝ → ℝ} (h_coef : coef.Sorted) : (mk (Multiseries.cons exp coef Multiseries.nil) f).Sorted

[(exp, coef)] is Sorted when coef is Sorted.

theorem ComputeAsymptotics.MultiseriesExpansion.Sorted.cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} {f : ℝ → ℝ} (h_coef : coef.Sorted) (h_comp : tl.leadingExp < ↑exp) (h_tl : tl.Sorted) : (mk (Multiseries.cons exp coef tl) f).Sorted

cons (exp, coef) tl is Sorted when coef and tl are Sorted and the leading exponent of tl is less than exp.

theorem ComputeAsymptotics.MultiseriesExpansion.Sorted.elim_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} {f : ℝ → ℝ} (h : (mk (Multiseries.cons exp coef tl) f).Sorted) : coef.Sorted ∧ tl.leadingExp < ↑exp ∧ tl.Sorted

If cons (exp, coef) tl is Sorted, then coef and tl are Sorted, and the leading exponent of tl is less than exp.

theorem ComputeAsymptotics.MultiseriesExpansion.Sorted.replaceFun {basis_hd : ℝ → ℝ} {basis_tl : Basis} {ms : MultiseriesExpansion (basis_hd :: basis_tl)} {f : ℝ → ℝ} (h_sorted : ms.Sorted) : (ms.replaceFun f).Sorted

@[irreducible]

def ComputeAsymptotics.MultiseriesExpansion.Approximates {basis : Basis} (ms : MultiseriesExpansion basis) : Prop

Coinductive predicate stating that ms approximates its attached function on basis.

• If basis = [], i.e. ms is just a real number, Approximates holds unconditionally.
• If basis = basis_hd :: basis_tl and ms = nil, then f =ᶠ[atTop] 0.
• If basis = basis_hd :: basis_tl and ms = cons exp coef tl, then f is Majorized with exponent exp by basis_hd, coef approximates its attached function, and tl approximates f - basis_hd ^ exp * coef.toFun.

@[simp]

def ComputeAsymptotics.MultiseriesExpansion.Approximates.const (ms : MultiseriesExpansion []) : ms.Approximates

Constant multiseries always approximates its attached function.

def ComputeAsymptotics.MultiseriesExpansion.Approximates.nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} {f : ℝ → ℝ} (hf : f =ᶠ[Filter.atTop] 0) : (mk Multiseries.nil f).Approximates

Empty multiseries approximates (eventually) zero function.

def ComputeAsymptotics.MultiseriesExpansion.Approximates.cons {basis_hd f : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} (h_coef : coef.Approximates) (h_maj : Tactic.ComputeAsymptotics.Majorized f basis_hd exp) (h_tl : (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates) : (mk (Multiseries.cons exp coef tl) f).Approximates

cons (exp, coef) tl approximates f when coef approximates some function fC, f is majorized with exponent exp by basis_hd, and tl approximates f - fC * basis_hd ^ exp.

theorem ComputeAsymptotics.MultiseriesExpansion.Approximates.coind {basis_hd : ℝ → ℝ} {basis_tl : Basis} {ms : MultiseriesExpansion (basis_hd :: basis_tl)} (motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop) (h_base : motive ms) (h_step : ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)), motive ms → ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[Filter.atTop] 0 ∨ ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl), ms.seq = Multiseries.cons exp coef tl ∧ coef.Approximates ∧ Tactic.ComputeAsymptotics.Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))) : ms.Approximates

theorem ComputeAsymptotics.MultiseriesExpansion.Approximates.elim_nil {f basis_hd : ℝ → ℝ} {basis_tl : Basis} (h : (mk Multiseries.nil f).Approximates) : f =ᶠ[Filter.atTop] 0

If [] approximates f, then f = 0 eventually.

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.Approximates.nil_iff {basis_hd : ℝ → ℝ} {basis_tl : Basis} {f : ℝ → ℝ} : (mk Multiseries.nil f).Approximates ↔ f =ᶠ[Filter.atTop] 0

theorem ComputeAsymptotics.MultiseriesExpansion.Approximates.elim_cons {f basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} (h : (mk (Multiseries.cons exp coef tl) f).Approximates) : coef.Approximates ∧ Tactic.ComputeAsymptotics.Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

If cons (exp, coef) tl approximates f, then f can be Majorized with exponent exp, and there exists function fC such that coef approximates fC and tl approximates f - fC * basis_hd ^ exp.

theorem ComputeAsymptotics.MultiseriesExpansion.Approximates.replaceFun_Approximates {basis_hd : ℝ → ℝ} {basis_tl : Basis} {ms : MultiseriesExpansion (basis_hd :: basis_tl)} {f : ℝ → ℝ} (h_equiv : ms.toFun =ᶠ[Filter.atTop] f) (h_approx : ms.Approximates) : (ms.replaceFun f).Approximates

One can replace f in Approximates with the funcion that eventually equals f.

@[implicit_reducible]

instance ComputeAsymptotics.MultiseriesExpansion.instSetoidConsForallReal (basis_hd : ℝ → ℝ) (basis_tl : Basis) : Setoid (MultiseriesExpansion (basis_hd :: basis_tl))

@[simp]

theorem ComputeAsymptotics.MultiseriesExpansion.equiv_def {basis_hd : ℝ → ℝ} {basis_tl : Basis} {x y : MultiseriesExpansion (basis_hd :: basis_tl)} : x ≈ y ↔ x.seq = y.seq ∧ x.toFun =ᶠ[Filter.atTop] y.toFun