Skip to content

Split over-long proofs in PLAcceleratedNesterovLean #757

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Vilin97 merged 2 commits into from
Nov 5, 2026
Merged

Split over-long proofs in PLAcceleratedNesterovLean #757

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
26965ac
Split over-long proofs in PLAcceleratedNesterovLean
Vilin97 Nov 5, 2026
3ce4c27
Extract fderiv_kills_normal_of_eqOn from the local convergence proof
Vilin97 Nov 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
590 changes: 165 additions & 425 deletions LeanPool/PLAcceleratedNesterovLean/Convergence/Bootstrap/Main.lean
View file
Open in desktop

Large diffs are not rendered by default.

575 changes: 312 additions & 263 deletions LeanPool/PLAcceleratedNesterovLean/Convergence/GenLocalArgument.lean
View file
Open in desktop

Large diffs are not rendered by default.

1,231 changes: 494 additions & 737 deletions LeanPool/PLAcceleratedNesterovLean/Convergence/LocalGeometry/Main.lean
View file
Open in desktop

Large diffs are not rendered by default.

991 changes: 429 additions & 562 deletions LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/GenMain.lean
View file
Open in desktop

Large diffs are not rendered by default.

687 changes: 7 additions & 680 deletions LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/Main.lean
View file
Open in desktop

Large diffs are not rendered by default.

352 changes: 194 additions & 158 deletions LeanPool/PLAcceleratedNesterovLean/Core/EmbeddedManifold.lean
View file
Open in desktop

Large diffs are not rendered by default.

482 changes: 253 additions & 229 deletions LeanPool/PLAcceleratedNesterovLean/MorseBott/TubularProjection/Derivative.lean
View file
Open in desktop

Large diffs are not rendered by default.

Loading