Computing limits of monomials

In this file we define the Monomial structure, representing monomials in a basis, i.e. coef * b₁ ^ e₁ * ... * bₙ ^ eₙ where [b₁, ..., bₙ] is a well-formed basis.

In the tactic implementation, we use Monomial to connect multiseries with real functions. In this file we show how to find a limit of Monomial and how to asymptotically compare two Monomials.

Main definitions

• Monomial: type to represent monomials.
• UnitMonomial.toFun/Monomial.toFun: converts structures to real functions.

structure Tactic.ComputeAsymptotics.Monomial : Type

Structure for representing monomials with coefficients.

• coef : ℝ

  Real coefficient of the monomial.

• unit : UnitMonomial

  Unit part of the monomial.

noncomputable def Tactic.ComputeAsymptotics.UnitMonomial.toFun (m : UnitMonomial) (basis : Basis) : ℝ → ℝ

Function corresponding to a monomial.

Equations

• m.toFun basis x = (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) => b x ^ exp) m basis).prod

noncomputable def Tactic.ComputeAsymptotics.UnitMonomial.toLogFun (m : UnitMonomial) (basis : Basis) : ℝ → ℝ

Logarithm of function represented by a monomial, i.e. m[0] * log basis[0] + ... + m[n] * log basis[n].

Equations

• m.toLogFun basis x = (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) => exp * Real.log (b x)) m basis).sum

@[simp]

theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_nil (basis : Basis) : toFun [] basis = 1

@[simp]

theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_nil_basis (m : UnitMonomial) : m.toFun [] = 1

@[simp]

theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_cons (exp : ℝ) (tl : UnitMonomial) (basis_hd : ℝ → ℝ) (basis_tl : Basis) : toFun (exp :: tl) (basis_hd :: basis_tl) = basis_hd ^ exp * tl.toFun basis_tl

@[simp]

theorem Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_nil (basis : Basis) : toLogFun [] basis = 0

@[simp]

theorem Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_nil_basis (m : UnitMonomial) : m.toLogFun [] = 0

@[simp]

theorem Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_cons (exp : ℝ) (tl : UnitMonomial) (basis_hd : ℝ → ℝ) (basis_tl : Basis) : toLogFun (exp :: tl) (basis_hd :: basis_tl) = exp • Real.log ∘ basis_hd + tl.toLogFun basis_tl

noncomputable def Tactic.ComputeAsymptotics.UnitMonomial.mul (m1 m2 : UnitMonomial) : UnitMonomial

Multiplication of unit monomials.

Equations

• m1.mul m2 = List.zipWith (fun (x1 x2 : ℝ) => x1 + x2) m1 m2

noncomputable def Tactic.ComputeAsymptotics.UnitMonomial.inv (m : UnitMonomial) : UnitMonomial

Inversion of a unit monomial.

Equations

• m.inv = List.map (fun (x : ℝ) => -x) m

theorem Tactic.ComputeAsymptotics.UnitMonomial.mul_length {m1 m2 : UnitMonomial} (h : List.length m1 = List.length m2) : List.length (m1.mul m2) = List.length m1

@[simp]

theorem Tactic.ComputeAsymptotics.UnitMonomial.inv_length (m : UnitMonomial) : List.length m.inv = List.length m

theorem Tactic.ComputeAsymptotics.UnitMonomial.mul_toFun {m1 m2 : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : List.length m1 = List.length m2) : (m1.mul m2).toFun basis =ᶠ[Filter.atTop] m1.toFun basis * m2.toFun basis

theorem Tactic.ComputeAsymptotics.UnitMonomial.inv_toFun {m : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) : m.inv.toFun basis =ᶠ[Filter.atTop] (m.toFun basis)⁻¹

noncomputable def Tactic.ComputeAsymptotics.Monomial.toFun (t : Monomial) (basis : Basis) : ℝ → ℝ

Converts t : Monomial to real function represented by the corresponding monomial, i.e. t.coef * basis[0]^t.exps[0] * basis[1]^t.exps[1] * .... It is always assumed that t.exps.length = basis.length, but some theorems below do not require this assumption.

Equations

• t.toFun basis = t.coef • t.unit.toFun basis

@[simp]

theorem Tactic.ComputeAsymptotics.Monomial.nil_toFun {coef : ℝ} {basis : Basis} : { coef := coef, unit := [] }.toFun basis = fun (x : ℝ) => coef

@[simp]

theorem Tactic.ComputeAsymptotics.Monomial.cons_toFun {coef exp : ℝ} {m : UnitMonomial} {basis_hd : ℝ → ℝ} {basis_tl : Basis} : { coef := coef, unit := exp :: m }.toFun (basis_hd :: basis_tl) = basis_hd ^ exp * { coef := coef, unit := m }.toFun basis_tl

theorem Tactic.ComputeAsymptotics.Monomial.zero_coef_toFun {t : Monomial} (basis : Basis) (h_coef : t.coef = 0) : t.toFun basis = 0

If t.coef = 0, then t.toFun is zero.

theorem Tactic.ComputeAsymptotics.Monomial.zero_coef_toFun' (basis : Basis) (exps : List ℝ) : { coef := 0, unit := exps }.toFun basis = 0

If t.coef = 0, then t.toFun is zero.

noncomputable def Tactic.ComputeAsymptotics.Monomial.neg (t : Monomial) : Monomial

Negation of a monomial.

Equations

• t.neg = { coef := -t.coef, unit := t.unit }

noncomputable def Tactic.ComputeAsymptotics.Monomial.mul (t1 t2 : Monomial) : Monomial

Multiplication of monomials.

Equations

• t1.mul t2 = { coef := t1.coef * t2.coef, unit := t1.unit.mul t2.unit }

noncomputable def Tactic.ComputeAsymptotics.Monomial.smul (t : Monomial) (c : ℝ) : Monomial

Scales a monomial by a real factor c.

Equations

• t.smul c = { coef := c * t.coef, unit := t.unit }

noncomputable def Tactic.ComputeAsymptotics.Monomial.inv (t : Monomial) : Monomial

Inversion operation for monomials.

Equations

• t.inv = { coef := t.coef⁻¹, unit := t.unit.inv }

theorem Tactic.ComputeAsymptotics.Monomial.neg_toFun {t : Monomial} {basis : Basis} : t.toFun basis = -t.neg.toFun basis

Flipping the sign of coef flips the sign of toFun. The theorem is stated in this form, because it allows one to rewrite the t.toFun basis expression. It is used below in cases where we want to reduce the case of t.coef < 0 to t.coef > 0.

theorem Tactic.ComputeAsymptotics.Monomial.mul_toFun {t1 t2 : Monomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : List.length t1.unit = List.length t2.unit) : (t1.mul t2).toFun basis =ᶠ[Filter.atTop] t1.toFun basis * t2.toFun basis

theorem Tactic.ComputeAsymptotics.Monomial.smul_toFun {t : Monomial} {basis : Basis} (c : ℝ) : (t.smul c).toFun basis = c • t.toFun basis

theorem Tactic.ComputeAsymptotics.Monomial.inv_toFun {t : Monomial} {basis : Basis} (h_basis : WellFormedBasis basis) : t.inv.toFun basis =ᶠ[Filter.atTop] (t.toFun basis)⁻¹

@[simp]

theorem Tactic.ComputeAsymptotics.Monomial.inv_length (t : Monomial) : List.length t.inv.unit = List.length t.unit