Skip to content

feat(Analysis/Asymptotics): if u is eventually positive and u ~ v then v is eventually positive#37621

Open
vasnesterov wants to merge 5 commits intoleanprover-community:masterfrom
vasnesterov:equivalent_eventually_pos
Open

feat(Analysis/Asymptotics): if u is eventually positive and u ~ v then v is eventually positive#37621
vasnesterov wants to merge 5 commits intoleanprover-community:masterfrom
vasnesterov:equivalent_eventually_pos

Conversation

@vasnesterov
Copy link
Copy Markdown
Collaborator

@vasnesterov vasnesterov commented Apr 3, 2026 •
edited
Loading

Prove that Asymptotics.IsEquivalent respects (non)positivity and (non)negativity of functions.

Open in Gitpod

@vasnesterov vasnesterov added the t-analysis Analysis (normed *, calculus) label Apr 3, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 3, 2026 •
edited
Loading

PR summary 20c47e339c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsEquivalent.eventually_neg
+ IsEquivalent.eventually_nonneg
+ IsEquivalent.eventually_nonpos
+ IsEquivalent.eventually_pos
+ IsEquivalent.exists_pos_eq_mul

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 relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@vihdzp
Copy link
Copy Markdown
Collaborator

vihdzp commented Apr 3, 2026

Can we also have the versions for ≤, and for eventually negative?

@vasnesterov
Copy link
Copy Markdown
Collaborator Author

vasnesterov commented Apr 4, 2026

Can we also have the versions for ≤, and for eventually negative?

Sure, done.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@vasnesterov @vihdzp