Formalize Lyapunov's indirect method (rebased onto current main) - #17
Merged
Merged
Conversation
…ndirect/ Consolidates the 13 new files PR #15 introduced (previously scattered across LinearSystems/, Stability/, and Analysis/) into one directory, and updates their internal imports and the root LeanForControl.lean import list to match. Renames Analysis/Linearization.lean to FrechetRemainder.lean to avoid colliding with the existing Stability/Linearization.lean basename. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
# Conflicts: # LeanForControl/Stability/plan.md # README.md # blueprint/src/content.tex
AnandGokhale
added a commit
that referenced
this pull request
Sep 22, 2026
Two independent fixes: - Add back the complexification helper that main's independent Hurwitz rewrite had dropped; three Lyapunov-indirect-method files (merged via PR #17) still reference it by name. This was left uncommitted in the reorg branch before that branch got pushed and merged. - ComparisonLemma.lean was written against the old Icc-based IsIntegralSolution and never updated after it was changed to quantify over uIcc. Add an ordering hypothesis to isIntegralSolution_of_hasDerivAt and use the unconditional left_mem_uIcc in comparison_claim_1. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
AnandGokhale
added a commit
that referenced
this pull request
Sep 22, 2026
AnandGokhale
added a commit
that referenced
this pull request
Sep 24, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Rebases and relocates PR #15's Lyapunov's indirect method work (originally branched
2026-09-10, before
main's subsequent directory reorg) so it merges cleanly onto currentmain.LeanForControl/Stability/LyapunovIndirect/, instead of leaving them scattered acrossLinearSystems/,Stability/, andAnalysis/.Analysis/Linearization.leantoFrechetRemainder.leanto avoid colliding withthe existing
Stability/Linearization.leanbasename.LeanForControl.leanimport list to match, and topoint at the paths
main's own Hurwitz reorg moved things to(
LinearSystems/Stability/Continuous/{Hurwitz,DefsHurwitz}.lean).complexificationhelper (asStability/LyapunovIndirect/DefsComplexification.lean)that
main's independent Hurwitz rewrite had dropped in favor of inliningA.map (algebraMap ℝ ℂ)— three of PR Formalize both branches of Lyapunov's indirect method #15's files depended on the named version.README.md,blueprint/src/content.tex, andStability/plan.md(the latter by dropping stale "planned" sections for Chetaev'stheorem and linearization that PR Formalize both branches of Lyapunov's indirect method #15 had already implemented).
Builds clean except for the pre-existing
ComparisonLemma.leanregression already onmain(unrelated to this PR, to be fixed separately).Supersedes #15.
Test plan
lake buildsucceeds for every file this PR touches or addssorry/admit