Documentation

Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates

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.

source
@[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.

Instances For
    source
    inductive Tactic.ComputeAsymptotics.UnitMonomial.Sign :
    Type

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

    Instances For
      source
      noncomputable def Tactic.ComputeAsymptotics.UnitMonomial.sign :
      UnitMonomial → Sign

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

      Instances For
        source
        def Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos (m : UnitMonomial) :
        Prop

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

        Instances For
          source
          def Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg (m : UnitMonomial) :
          Prop

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

          Instances For
            source
            def Tactic.ComputeAsymptotics.UnitMonomial.AllZero (m : UnitMonomial) :
            Prop

            Predicate stating that all exponents are zero.

            Instances For
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.AllZero.nil :
              AllZero []
              source
              @[simp]
              theorem Tactic.ComputeAsymptotics.UnitMonomial.AllZero.cons_iff {hd : ℝ} {tl : UnitMonomial} :
              AllZero (hd :: tl) ↔ hd = 0 ∧ tl.AllZero
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.AllZero.of_tail {hd : ℝ} {tl : UnitMonomial} (h_hd : hd = 0) (h_tl : tl.AllZero) :
              AllZero (hd :: tl)
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.AllZero.replicate {n : ℕ} :
              AllZero (List.replicate n 0)
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.AllZero.not_FirstNonzeroIsPos {li : UnitMonomial} (h : li.AllZero) :
              ¬li.FirstNonzeroIsPos
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.AllZero.not_FirstNonzeroIsNeg {li : UnitMonomial} (h : li.AllZero) :
              ¬li.FirstNonzeroIsNeg
              source
              @[simp]
              theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.not_nil :
              ¬FirstNonzeroIsPos []
              source
              @[simp]
              theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.cons_iff {hd : ℝ} {tl : UnitMonomial} :
              FirstNonzeroIsPos (hd :: tl) ↔ 0 < hd ∨ hd = 0 ∧ tl.FirstNonzeroIsPos
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.of_head {hd : ℝ} (tl : UnitMonomial) (h_hd : 0 < hd) :
              FirstNonzeroIsPos (hd :: tl)
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.of_tail {hd : ℝ} {tl : UnitMonomial} (h_hd : hd = 0) (h_tl : tl.FirstNonzeroIsPos) :
              FirstNonzeroIsPos (hd :: tl)
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.not_AllZero {li : UnitMonomial} (h : li.FirstNonzeroIsPos) :
              ¬li.AllZero
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.not_FirstNonzeroIsNeg {li : UnitMonomial} (h : li.FirstNonzeroIsPos) :
              ¬li.FirstNonzeroIsNeg
              source
              @[simp]
              theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.not_nil :
              ¬FirstNonzeroIsNeg []
              source
              @[simp]
              theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.cons_iff {hd : ℝ} {tl : UnitMonomial} :
              FirstNonzeroIsNeg (hd :: tl) ↔ hd < 0 ∨ hd = 0 ∧ tl.FirstNonzeroIsNeg
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.of_head {hd : ℝ} (tl : UnitMonomial) (h_hd : hd < 0) :
              FirstNonzeroIsNeg (hd :: tl)
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.of_tail {hd : ℝ} {tl : UnitMonomial} (h_hd : hd = 0) (h_tl : tl.FirstNonzeroIsNeg) :
              FirstNonzeroIsNeg (hd :: tl)
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.not_AllZero {li : UnitMonomial} (h : li.FirstNonzeroIsNeg) :
              ¬li.AllZero
              source
              theorem Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.not_FirstNonzeroIsPos {li : UnitMonomial} (h : li.FirstNonzeroIsNeg) :
              ¬li.FirstNonzeroIsPos