Trimming of multiseries

A multiseries is trimmed when its leading coefficient (the head of its expansion) is itself trimmed and non-zero. For a trimmed multiseries, the leading monomial captures the main asymptotic behavior of the approximated function.

Main definitions

• IsZero: a multiseries represents the zero function — it is either the real number 0 (for the empty basis) or has an empty underlying sequence (.nil).
• Trimmed and Multiseries.Trimmed: a multiseries is trimmed in the sense above. The former is defined inductively for MultiseriesExpansion, and the latter for Multiseries is derived from it.

We also prove structural lemmas relating these predicates to seq and to the cons/nil constructors.

inductive Tactic.ComputeAsymptotics.MultiseriesExpansion.IsZero {basis : Basis} : MultiseriesExpansion basis → Prop

A multiseries is zero if it is the real constant 0 or has an empty sequence.

• const {c : MultiseriesExpansion []} (hc : c.toReal = 0) : c.IsZero
• nil {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} (f : ℝ → ℝ) : (mk Multiseries.nil f).IsZero

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.IsZero.const_iff {c : MultiseriesExpansion []} : c.IsZero ↔ c.toReal = 0

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.IsZero.iff_seq_eq_nil {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} {ms : MultiseriesExpansion (basis_hd :: basis_tl)} : ms.IsZero ↔ ms.seq = Multiseries.nil

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.IsZero.approximates_zero {basis : Basis} {ms : MultiseriesExpansion basis} (h_zero : ms.IsZero) (h_approx : ms.Approximates) : ms.toFun =ᶠ[Filter.atTop] 0

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.IsZero.not_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} {f : ℝ → ℝ} : ¬(mk (Multiseries.cons exp coef tl) f).IsZero

inductive Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed {basis : Basis} : MultiseriesExpansion basis → Prop

We call a multiseries Trimmed if it is either a constant, .nil, or cons (exp, coef) tl where coef is trimmed and is not zero. Intuitively, when a multiseries is trimmed, its leading monomial gives the main asymptotic behavior of the approximated function.

• const {c : ℝ} : Trimmed c
• nil {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} {f : ℝ → ℝ} : (mk Multiseries.nil f).Trimmed
• cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} {f : ℝ → ℝ} (h_trimmed : coef.Trimmed) (h_ne_zero : ¬coef.IsZero) : (mk (Multiseries.cons exp coef tl) f).Trimmed

def Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Trimmed {basis_hd : ℝ → ℝ} {basis_tl : Basis} (ms : Multiseries basis_hd basis_tl) : Prop

We call a Multiseries Trimmed if it is either .nil or cons (exp, coef) tl where coef is trimmed and is not zero.

Equations

• ms.Trimmed = (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk ms 0).Trimmed

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.trimmed_iff_seq_trimmed {basis_hd : ℝ → ℝ} {basis_tl : Basis} (ms : MultiseriesExpansion (basis_hd :: basis_tl)) : ms.Trimmed ↔ ms.seq.Trimmed

@[simp]

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Trimmed.nil {basis_hd : ℝ → ℝ} {basis_tl : Basis} : Multiseries.nil.Trimmed

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Trimmed.cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} (h_coef : coef.Trimmed) (h_ne_zero : ¬coef.IsZero) : (Multiseries.cons exp coef tl).Trimmed

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Trimmed.elim_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} (h : (Multiseries.cons exp coef tl).Trimmed) : coef.Trimmed ∧ ¬coef.IsZero

If cons (exp, coef) tl is trimmed, then coef is trimmed and is not zero.

theorem Tactic.ComputeAsymptotics.MultiseriesExpansion.elim_cons {basis_hd : ℝ → ℝ} {basis_tl : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl} {tl : Multiseries basis_hd basis_tl} {f : ℝ → ℝ} (h : (mk (Multiseries.cons exp coef tl) f).Trimmed) : coef.Trimmed ∧ ¬coef.IsZero

If cons (exp, coef) tl is trimmed, then coef is trimmed and is not zero.