Basic constructions for multiseries

Main definitions

Let [b₁, ..., bₙ] be our basis.

• const c represents a constant multiseries c • b₁⁰ ... bₙ⁰. Then we define zero and one in terms of it.
• monomial k represents a monomial bₖ.
• monomialRpow k r represents a monomial bₖʳ.

For each construction, we provide two definitions: one for Multiseries and one for MultiseriesExpansion. We then prove structural simp-lemmas describing their relationships with MultiseriesExpansion.seq and MultiseriesExpansion.toFun. Finally, we prove that all constructions are Sorted and Approximates their attached functions.

@[irreducible]

def Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const (basis_hd : ℝ → ℝ) (basis_tl : Basis) (c : ℝ) : Multiseries basis_hd basis_tl

Multiseries-part of MultiseriesExpansion.const.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Tactic.ComputeAsymptotics.MultiseriesExpansion.const (basis : Basis) (c : ℝ) : MultiseriesExpansion basis

Multiseries representing a constant.

Equations

• One or more equations did not get rendered due to their size.
• Tactic.ComputeAsymptotics.MultiseriesExpansion.const [] c = Tactic.ComputeAsymptotics.MultiseriesExpansion.ofReal c

def Tactic.ComputeAsymptotics.MultiseriesExpansion.zero {basis : Basis} : MultiseriesExpansion basis

Neutral element for addition. It is 0 : ℝ for the empty basis and [] otherwise.

Equations

• Tactic.ComputeAsymptotics.MultiseriesExpansion.zero = Tactic.ComputeAsymptotics.MultiseriesExpansion.ofReal 0
• Tactic.ComputeAsymptotics.MultiseriesExpansion.zero = Tactic.ComputeAsymptotics.MultiseriesExpansion.mk Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil fun (x : ℝ) => 0

@[implicit_reducible]

instance Tactic.ComputeAsymptotics.MultiseriesExpansion.instZero {basis : Basis} : Zero (MultiseriesExpansion basis)

This instance is needed to create an instance for AddCommMonoid (MultiseriesExpansion basis), which is necessary for using the abel tactic in our proofs.

Equations

• Tactic.ComputeAsymptotics.MultiseriesExpansion.instZero = { zero := Tactic.ComputeAsymptotics.MultiseriesExpansion.zero }

@[implicit_reducible]

instance Tactic.ComputeAsymptotics.MultiseriesExpansion.instZeroMultiseries {basis_hd : ℝ → ℝ} {basis_tl : Basis} : Zero (Multiseries basis_hd basis_tl)

This instance is needed to create an instance for AddCommMonoid (MultiseriesExpansion basis), which is necessary for using the abel tactic in our proofs.

Equations

• Tactic.ComputeAsymptotics.MultiseriesExpansion.instZeroMultiseries = { zero := Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil }

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

Multiseries-part of MultiseriesExpansion.one.

Equations

• Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.one = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const basis_hd basis_tl 1

def Tactic.ComputeAsymptotics.MultiseriesExpansion.one {basis : Basis} : MultiseriesExpansion basis

Neutral element for multiplication.

Equations

• Tactic.ComputeAsymptotics.MultiseriesExpansion.one = Tactic.ComputeAsymptotics.MultiseriesExpansion.const basis 1

@[irreducible]

noncomputable def Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow (basis_hd : ℝ → ℝ) (basis_tl : Basis) (n : ℕ) (r : ℝ) : Multiseries basis_hd basis_tl

Multiseries-part of MultiseriesExpansion.monomialRpow.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

noncomputable def Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow (basis : Basis) (n : ℕ) (r : ℝ) : MultiseriesExpansion basis

Multiseries representing basis[n] ^ r.

Equations

• One or more equations did not get rendered due to their size.
• Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow [] n r = default

noncomputable def Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomial (basis_hd : ℝ → ℝ) (basis_tl : Basis) (n : ℕ) : Multiseries basis_hd basis_tl

Multiseries-part of MultiseriesExpansion.monomial.

Equations

• Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomial basis_hd basis_tl n = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow basis_hd basis_tl n 1

noncomputable def Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial (basis : Basis) (n : ℕ) : MultiseriesExpansion basis

Multiseries representing basis[n].

Equations

• Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial basis n = Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow basis n 1

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.zero_def {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} : 0 = mk Multiseries.nil fun (x : ℝ) => 0

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.zero_def {basis_hd : ℝ → ℝ} {basis_tl : Basis} : 0 = nil

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const_def {basis_hd : ℝ → ℝ} {basis_tl : Basis} (c : ℝ) : const basis_hd basis_tl c = cons 0 (MultiseriesExpansion.const basis_tl c) nil

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.const_toFun' {basis : Basis} {c : ℝ} : (const basis c).toFun = fun (x : ℝ) => c

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.const_seq {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} {c : ℝ} : (const (basis_hd :: basis_tl) c).seq = Multiseries.const basis_hd basis_tl c

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.zero_toFun {basis : Basis} : zero.toFun = 0

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.one_def {basis_hd : ℝ → ℝ} {basis_tl : Basis} : one = cons 0 MultiseriesExpansion.one nil

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.one_toFun {basis : Basis} : one.toFun = 1

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.one_seq {basis_hd : ℝ → ℝ} {basis_tl : Basis} : one.seq = Multiseries.one

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const_sorted {basis_hd : ℝ → ℝ} {basis_tl : Basis} {c : ℝ} : (const basis_hd basis_tl c).Sorted

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.const_sorted {basis : Basis} {c : ℝ} : (const basis c).Sorted

Constants are well-ordered.

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.zero_sorted {basis : Basis} : Sorted 0

Zero is well-ordered.

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.one_sorted {basis_hd : ℝ → ℝ} {basis_tl : Basis} : one.Sorted

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.one_sorted {basis : Basis} : one.Sorted

one is Sorted.

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.const_approximates {c : ℝ} {basis : Basis} (h_basis : WellFormedBasis basis) : (const basis c).Approximates

The constant multiseries approximates the constant function.

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.zero_approximates {basis : Basis} : zero.Approximates

zero approximates the zero function.

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.one_approximates {basis : Basis} (h_basis : WellFormedBasis basis) : one.Approximates

one approximates the unit function.

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow_toFun {basis : Basis} {n : Fin (List.length basis)} {r : ℝ} : (monomialRpow basis (↑n) r).toFun = basis[n] ^ r

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow_seq {basis_hd : ℝ → ℝ} {basis_tl : Basis} {n : ℕ} {r : ℝ} : (monomialRpow (basis_hd :: basis_tl) n r).seq = Multiseries.monomialRpow basis_hd basis_tl n r

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow_sorted {basis_hd : ℝ → ℝ} {basis_tl : Basis} {n : ℕ} {r : ℝ} : (monomialRpow basis_hd basis_tl n r).Sorted

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow_sorted {basis : Basis} {n : ℕ} {r : ℝ} : (monomialRpow basis n r).Sorted

monomial is well-ordered.

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow_approximates {basis : Basis} {n : Fin (List.length basis)} {r : ℝ} (h_basis : WellFormedBasis basis) : (monomialRpow basis (↑n) r).Approximates

monomialRpow approximates the monomial function.

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial_toFun {basis : Basis} {n : ℕ} (h : n < List.length basis) : (monomial basis n).toFun = basis[n]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial_toFun' {basis : Basis} {n : Fin (List.length basis)} : (monomial basis ↑n).toFun = basis[n]

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial_seq {basis_hd : ℝ → ℝ} {basis_tl : Basis} {n : ℕ} : (monomial (basis_hd :: basis_tl) n).seq = Multiseries.monomial basis_hd basis_tl n

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomial_sorted {basis_hd : ℝ → ℝ} {basis_tl : Basis} {n : ℕ} : (monomial basis_hd basis_tl n).Sorted

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial_sorted {basis : Basis} {n : ℕ} : (monomial basis n).Sorted

monomial is well-ordered.

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial_approximates {basis : Basis} {n : Fin (List.length basis)} (h_basis : WellFormedBasis basis) : (monomial basis ↑n).Approximates

monomial approximates the monomial function.