feat(Tactic/ComputeAsymptotics/Multiseries): predicates for Monomial#37414
feat(Tactic/ComputeAsymptotics/Multiseries): predicates for Monomial#37414vasnesterov wants to merge 8 commits intoleanprover-community:masterfrom
Monomial#37414Conversation
PR summary fdd294c699Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
WilliamCoram
left a comment
WilliamCoram
left a comment
There was a problem hiding this comment.
This is looking good. Other than my comments I am a bit unsure of the naming scheme in theorems used:
e.g. I think AllZero_of_nil should be renamed allZero_of_nil to be in lowerCamelCase. This can then be repeated in the rest of the theorems.
If someone else can confirm or deny this (as much for myself as for the PR), please comment.
Mathlib/Tactic/ComputeAsymptotics/Multiseries/Monomial/Predicates.lean
Outdated
Show resolved
Hide resolved
| theorem AllZero_of_replicate {n : ℕ} : AllZero (List.replicate n 0) := by | ||
| cases n <;> simp [AllZero] | ||
|
|
||
| theorem not_FirstNonzeroIsPos_of_AllZero {li : List ℝ} (h : AllZero li) : |
There was a problem hiding this comment.
Do you want a similar theorem for not_FirstNonzeroIsNeg_of_AllZero?
Same goes for the theorem below.
There was a problem hiding this comment.
It, of course, can be proven, but isn't needed for the tactic.
|
Thank you for taking a look! I've renamed some theorems. |
3 participants
Introduce
FirstNonzeroIsPos,FirstNonzeroIsNegandAllZeropredicates on lists of real numbers.When applied to a list of exponents of a monomial in a well-formed basis, this trichotomy
determines its asymptotic behaviour:
FirstNonzeroIsPosmeans it tends to infinity,FirstNonzeroIsNegmeans it tends to zero andAllZeromeans it tends to a constant.This is a part of the
compute_asymptoticstactic (#28291).