feat(Tactic/ComputeAsymptotics/Multiseries): compute limits of Monomials#37415
feat(Tactic/ComputeAsymptotics/Multiseries): compute limits of Monomials#37415vasnesterov wants to merge 3 commits intoleanprover-community:masterfrom
Monomials#37415Conversation
PR summary fdd294c699
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis | 1772 | 1775 | +3 (+0.17%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Tactic |
2 |
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis |
3 |
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates (new file) |
1777 |
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (new file) |
1778 |
Declarations diff
+ AllZero
+ AllZero.cons_iff
+ AllZero_of_nil
+ AllZero_of_replicate
+ AllZero_of_tail
+ FirstNonzeroIsNeg
+ FirstNonzeroIsNeg_of_head
+ FirstNonzeroIsNeg_of_tail
+ FirstNonzeroIsPos
+ FirstNonzeroIsPos_of_head
+ FirstNonzeroIsPos_of_tail
+ IsLittleO_of_lt
+ IsLittleO_of_lt_exps
+ IsLittleO_of_lt_exps_left
+ IsLittleO_of_lt_exps_right
+ Monomial
+ UnitMonomial
+ cons_toFun
+ logToFun_eq_toLogFun
+ logToFun_isEquivalent_of_nonzero_head
+ mul_length
+ neg
+ neg_toFun
+ nil_toFun
+ not_FirstNonzeroIsPos_of_AllZero
+ not_FirstNonzeroIsPos_of_FirstNonzeroIsNeg
+ pow_isLittleO_pow_of_log
+ smul
+ smul_toFun
+ tail_pow_Majorized_head
+ tendsto_zero_of_coef_zero
+ toFun_cons
+ toFun_ne_zero
+ toFun_nil
+ toFun_nil_basis
+ toFun_tendsto_bot_of_FirstNonzeroIsPos
+ toFun_tendsto_const_of_AllZero
+ toFun_tendsto_one_of_AllZero
+ toFun_tendsto_top_of_head_pos
+ toFun_tendsto_zero_of_head_neg
+ toLogFun
+ toLogFun_cons
+ toLogFun_nil
+ toLogFun_nil_basis
+ zero_coef_toFun
+ zero_coef_toFun'
++ inv
++ inv_length
++ inv_toFun
++ mul
++ mul_toFun
++ tail_toFun_IsLittleO_head
++ toFun
++ toFun_pos
++ toFun_tendsto_top_of_FirstNonzeroIsPos
++ toFun_tendsto_zero_of_FirstNonzeroIsNeg
++ zeros_append_toFun
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
mathlib-dependent-issues
bot
added
the
blocked-by-other-PR
|
This PR/issue depends on:
|
There was a problem hiding this comment.
These look (superficially) reasonable to me. Maybe there is some potential to clean up a bit more and make some proves shorter, but I'll look at that when the dependencies are merged.
The capitalisation of theorems needs to be fixed in this PR likewise to the other PRs.
2 participants
Prove
UnitMonomial.logToFun_isEquivalent_of_nonzero_head:log m.toFunis asymptotically equivalentto its first summand -
m[0] • log basis[0]ifm[0] ≠ 0. Using this theorem we can prove thatthe asymptotic behavior of a monomial is determined by its first non-zero exponent.
toFun_tendsto_top_of_FirstNonzeroIsPosand its variants: used to infer the limit oft.toFunfromFirstNonzeroIsPos/FirstNonzeroIsNeg/AllZero.IsLittleO_of_lt_expsand its variants: used to asymptotically compare two monomials.Monomial#37411This is a part of the
compute_asymptoticstactic (#28291).