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 : ℝ → ℝ.

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