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.
• UnitMonomial.toLogFun_isEquivalent_of_nonzero_head: log m.toFun is asymptotically equivalent to its first summand - m[0] • log basis[0] if m[0] ≠ 0. Using this theorem we can prove that the asymptotic behaviour of the monomials is determined by its first non-zero exponent.
• toFun_tendsto_top_of_FirstNonzeroIsPos and its variants are used to infer the limit of t.toFun from FirstNonzeroIsPos/FirstNonzeroIsNeg/AllZero.
• IsLittleO_of_lt_exps and its variants are used to asymptotically compare two monomials.

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)⁻¹

theorem Tactic.ComputeAsymptotics.UnitMonomial.majorized_tail_toFun_head {m : UnitMonomial} {basis_hd : ℝ → ℝ} {basis_tl : Basis} (h_length : List.length m = List.length basis_tl) (h_basis : WellFormedBasis (basis_hd :: basis_tl)) : Majorized (m.toFun basis_tl) basis_hd 0

theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_pos {m : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) : ∀ᶠ (x : ℝ) in Filter.atTop, 0 < m.toFun basis x

theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_ne_zero {m : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) : ∀ᶠ (x : ℝ) in Filter.atTop, m.toFun basis x ≠ 0

theorem Tactic.ComputeAsymptotics.UnitMonomial.zeros_append_toFun {m : UnitMonomial} {left right : Basis} : (List.replicate (List.length left) 0 ++ m).toFun (left ++ right) = m.toFun right

theorem Tactic.ComputeAsymptotics.UnitMonomial.log_toFun_eq_toLogFun {m : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) : Real.log ∘ m.toFun basis =ᶠ[Filter.atTop] m.toLogFun basis

theorem Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_isEquivalent_of_nonzero_head {exps_hd : ℝ} {exps_tl : UnitMonomial} {basis_hd : ℝ → ℝ} {basis_tl : Basis} (h_basis : WellFormedBasis (basis_hd :: basis_tl)) (h_nonzero : exps_hd ≠ 0) : Asymptotics.IsEquivalent Filter.atTop (toLogFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) (exps_hd • Real.log ∘ basis_hd)

theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_tendsto_top_of_head_pos {exps_hd : ℝ} {exps_tl : UnitMonomial} {basis_hd : ℝ → ℝ} {basis_tl : Basis} (h_basis : WellFormedBasis (basis_hd :: basis_tl)) (h_nonzero : 0 < exps_hd) : Filter.Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) Filter.atTop Filter.atTop

theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_tendsto_zero_of_head_neg {exps_hd : ℝ} {exps_tl : UnitMonomial} {basis_hd : ℝ → ℝ} {basis_tl : Basis} (h_basis : WellFormedBasis (basis_hd :: basis_tl)) (h_nonzero : exps_hd < 0) : Filter.Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) Filter.atTop (nhds 0)

theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_tendsto_top_of_firstNonzeroIsPos {m : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : List.length m = List.length basis) (h_firstIsPos : m.FirstNonzeroIsPos) : Filter.Tendsto (m.toFun basis) Filter.atTop Filter.atTop

theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_tendsto_zero_of_firstNonzeroIsNeg {m : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : List.length m = List.length basis) (h_firstIsNeg : m.FirstNonzeroIsNeg) : Filter.Tendsto (m.toFun basis) Filter.atTop (nhds 0)

theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_tendsto_one_of_allZero {m : UnitMonomial} {basis : Basis} (h_allZero : m.AllZero) : Filter.Tendsto (m.toFun basis) Filter.atTop (nhds 1)

theorem Tactic.ComputeAsymptotics.UnitMonomial.isLittleO_of_lt {basis : Basis} {m1 m2 : UnitMonomial} (h_basis : WellFormedBasis basis) (h1 : List.length m1 = List.length basis) (h2 : List.length m2 = List.length basis) (h_lt : m1 < m2) : m1.toFun basis =o[Filter.atTop] m2.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 : UnitMonomial) : { 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

theorem Tactic.ComputeAsymptotics.Monomial.toFun_pos {t : Monomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_coef : 0 < t.coef) : ∀ᶠ (x : ℝ) in Filter.atTop, 0 < t.toFun basis x

If t.coef > 0 then t.toFun is eventually positive.

theorem Tactic.ComputeAsymptotics.Monomial.zeros_append_toFun (coef : ℝ) {exps : UnitMonomial} {left right : Basis} : have t := { coef := coef, unit := List.replicate (List.length left) 0 ++ exps }; t.toFun (left ++ right) = { coef := coef, unit := exps }.toFun right

theorem Tactic.ComputeAsymptotics.Monomial.tendsto_zero_of_coef_zero {coef : ℝ} {exps : UnitMonomial} (basis : Basis) (h_coef : coef = 0) : have t := { coef := coef, unit := exps }; Filter.Tendsto (t.toFun basis) Filter.atTop (nhds 0)

t.toFun tends to 𝓝 0 when t.coef = 0.

theorem Tactic.ComputeAsymptotics.Monomial.toFun_tendsto_zero_of_firstNonzeroIsNeg {coef : ℝ} {exps : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : List.length exps = List.length basis) (h_exps : exps.FirstNonzeroIsNeg) : have t := { coef := coef, unit := exps }; Filter.Tendsto (t.toFun basis) Filter.atTop (nhds 0)

theorem Tactic.ComputeAsymptotics.Monomial.toFun_tendsto_top_of_firstNonzeroIsPos {coef : ℝ} {exps : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : List.length exps = List.length basis) (h_coef : 0 < coef) (h_exps : exps.FirstNonzeroIsPos) : have t := { coef := coef, unit := exps }; Filter.Tendsto (t.toFun basis) Filter.atTop Filter.atTop

theorem Tactic.ComputeAsymptotics.Monomial.toFun_tendsto_bot_of_firstNonzeroIsPos {coef : ℝ} {exps : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : List.length exps = List.length basis) (h_coef : coef < 0) (h_exps : exps.FirstNonzeroIsPos) : have t := { coef := coef, unit := exps }; Filter.Tendsto (t.toFun basis) Filter.atTop Filter.atBot

theorem Tactic.ComputeAsymptotics.Monomial.toFun_tendsto_const_of_allZero {coef : ℝ} {exps : UnitMonomial} {basis : Basis} (h_exps : exps.AllZero) : have t := { coef := coef, unit := exps }; Filter.Tendsto (t.toFun basis) Filter.atTop (nhds coef)

theorem Tactic.ComputeAsymptotics.Monomial.majorized_tail_toFun_head {t : Monomial} {basis_hd : ℝ → ℝ} {basis_tl : Basis} (h_length : List.length t.unit = List.length basis_tl) (h_basis : WellFormedBasis (basis_hd :: basis_tl)) : Majorized (t.toFun basis_tl) basis_hd 0

theorem Tactic.ComputeAsymptotics.Monomial.isLittleO_of_lt_exps {basis : Basis} {t1 t2 : Monomial} (h_basis : WellFormedBasis basis) (h1 : List.length t1.unit = List.length basis) (h2 : List.length t2.unit = List.length basis) (h_coef2 : t2.coef ≠ 0) (h_lt : t1.unit < t2.unit) : t1.toFun basis =o[Filter.atTop] t2.toFun basis

theorem Tactic.ComputeAsymptotics.Monomial.isLittleO_of_lt_exps_left {left right : Basis} {t1 t2 : Monomial} (h_basis : WellFormedBasis (left ++ right)) (h1 : List.length t1.unit = List.length left + List.length right) (h2 : List.length t2.unit = List.length right) (h_coef2 : t2.coef ≠ 0) (h_lt : t1.unit < List.replicate (List.length left) 0 ++ t2.unit) : t1.toFun (left ++ right) =o[Filter.atTop] t2.toFun right

theorem Tactic.ComputeAsymptotics.Monomial.isLittleO_of_lt_exps_right {left right : Basis} {t1 t2 : Monomial} (h_basis : WellFormedBasis (left ++ right)) (h1 : List.length t1.unit = List.length left + List.length right) (h2 : List.length t2.unit = List.length right) (h_coef1 : t1.coef ≠ 0) (h_lt : List.replicate (List.length left) 0 ++ t2.unit < t1.unit) : t2.toFun right =o[Filter.atTop] t1.toFun (left ++ right)