Predicates on monomials

In this file we define UnitMonomial: type to represent monomials without coefficient as a list of its exponents. [e₁, e₂, ..., eₙ] corresponds to basis[0] ^ e₁ * ... * basis[n] ^ eₙ where basis is the basis of functions.

Then we define some predicates for these lists:

1. FirstNonzeroIsPos li means that the first non-zero element of the list li is positive.
2. FirstNonzeroIsNeg li means that the first non-zero element of the list li is negative.
3. AllZero li means that all elements in li are zero.

This trichotomy determines the asymptotic behaviour of a monomial: FirstNonzeroIsPos means it tends to infinity, FirstNonzeroIsNeg means it tends to zero and AllZero means it tends to a constant.

@[reducible, inline]

abbrev Tactic.ComputeAsymptotics.UnitMonomial : Type

Unit monomial, represented as a list of its exponents. [e₁, e₂, ..., eₙ] corresponds to basis[0] ^ e₁ * ... * basis[n] ^ eₙ where basis is the basis of functions.

Equations

• Tactic.ComputeAsymptotics.UnitMonomial = List ℝ

inductive Tactic.ComputeAsymptotics.UnitMonomial.Sign : Type

Type representing a sign of the first non-zero exponent, returned by sign.

• pos : Sign
• neg : Sign
• zero : Sign

noncomputable def Tactic.ComputeAsymptotics.UnitMonomial.sign : UnitMonomial → Sign

Sign of the first non-zero exponent of a unit monomial.

Equations

• One or more equations did not get rendered due to their size.
• Tactic.ComputeAsymptotics.UnitMonomial.sign [] = Tactic.ComputeAsymptotics.UnitMonomial.Sign.zero

def Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos (m : UnitMonomial) : Prop

Predicate stating that the first non-zero exponent is positive.

Equations

• m.FirstNonzeroIsPos = (m.sign = Tactic.ComputeAsymptotics.UnitMonomial.Sign.pos)

def Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg (m : UnitMonomial) : Prop

Predicate stating that the first non-zero exponent is negative.

Equations

• m.FirstNonzeroIsNeg = (m.sign = Tactic.ComputeAsymptotics.UnitMonomial.Sign.neg)

def Tactic.ComputeAsymptotics.UnitMonomial.AllZero (m : UnitMonomial) : Prop

Predicate stating that all exponents are zero.

Equations

• m.AllZero = (m.sign = Tactic.ComputeAsymptotics.UnitMonomial.Sign.zero)

theorem Tactic.ComputeAsymptotics.UnitMonomial.AllZero.nil : AllZero []

@[simp]

theorem Tactic.ComputeAsymptotics.UnitMonomial.AllZero.cons_iff {hd : ℝ} {tl : UnitMonomial} : AllZero (hd :: tl) ↔ hd = 0 ∧ tl.AllZero

theorem Tactic.ComputeAsymptotics.UnitMonomial.AllZero.of_tail {hd : ℝ} {tl : UnitMonomial} (h_hd : hd = 0) (h_tl : tl.AllZero) : AllZero (hd :: tl)

theorem Tactic.ComputeAsymptotics.UnitMonomial.AllZero.replicate {n : ℕ} : AllZero (List.replicate n 0)

theorem Tactic.ComputeAsymptotics.UnitMonomial.AllZero.not_FirstNonzeroIsPos {li : UnitMonomial} (h : li.AllZero) : ¬li.FirstNonzeroIsPos

theorem Tactic.ComputeAsymptotics.UnitMonomial.AllZero.not_FirstNonzeroIsNeg {li : UnitMonomial} (h : li.AllZero) : ¬li.FirstNonzeroIsNeg

@[simp]

theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.not_nil : ¬FirstNonzeroIsPos []

@[simp]

theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.cons_iff {hd : ℝ} {tl : UnitMonomial} : FirstNonzeroIsPos (hd :: tl) ↔ 0 < hd ∨ hd = 0 ∧ tl.FirstNonzeroIsPos

theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.of_head {hd : ℝ} (tl : UnitMonomial) (h_hd : 0 < hd) : FirstNonzeroIsPos (hd :: tl)

theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.of_tail {hd : ℝ} {tl : UnitMonomial} (h_hd : hd = 0) (h_tl : tl.FirstNonzeroIsPos) : FirstNonzeroIsPos (hd :: tl)

theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.not_AllZero {li : UnitMonomial} (h : li.FirstNonzeroIsPos) : ¬li.AllZero

theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.not_FirstNonzeroIsNeg {li : UnitMonomial} (h : li.FirstNonzeroIsPos) : ¬li.FirstNonzeroIsNeg

@[simp]

theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.not_nil : ¬FirstNonzeroIsNeg []

@[simp]

theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.cons_iff {hd : ℝ} {tl : UnitMonomial} : FirstNonzeroIsNeg (hd :: tl) ↔ hd < 0 ∨ hd = 0 ∧ tl.FirstNonzeroIsNeg

theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.of_head {hd : ℝ} (tl : UnitMonomial) (h_hd : hd < 0) : FirstNonzeroIsNeg (hd :: tl)

theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.of_tail {hd : ℝ} {tl : UnitMonomial} (h_hd : hd = 0) (h_tl : tl.FirstNonzeroIsNeg) : FirstNonzeroIsNeg (hd :: tl)

theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.not_AllZero {li : UnitMonomial} (h : li.FirstNonzeroIsNeg) : ¬li.AllZero

theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.not_FirstNonzeroIsPos {li : UnitMonomial} (h : li.FirstNonzeroIsNeg) : ¬li.FirstNonzeroIsPos