Skip to content

feat(Stability/Floquet): formalize basic Floquet theory and spectral stability #68

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

Open
AdoHaha wants to merge 10 commits into
base: main
Choose a base branch
from
Open

feat(Stability/Floquet): formalize basic Floquet theory and spectral stability #68

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
796914b
feat(Analysis/ODE/GlobalExistence): prove unique, add_apply, and add_…
Sep 7, 2026
dae4c72
feat(InputOutput): prove isGraph_inputOutput and isGraph_inputState
Sep 7, 2026
336ee32
feat(ODE): prove linear_fundamental_solution and linear_fundamental_s…
Sep 7, 2026
87e7e02
feat(Dynamics): prove isCompleteVectorField for IsLinearlyBddVectorField
Sep 7, 2026
c41d20c
feat(Stability): formalize basic Floquet theory
Sep 8, 2026
e9265ce
feat(Stability): add dynamic stability and complex eigenvalue theorem…
Sep 8, 2026
a7dfa09
fix(Stability/Floquet): generalize unstable roots to |ρ| > 1 and add …
Sep 8, 2026
1151515
docs(Stability/Floquet): clarify conditional scope, scalar roots, and…
Sep 8, 2026
021762c
Merge upstream main into Floquet theory branch
Sep 30, 2026
a8a39c4
Keep closed-loop graph proofs scoped to PR 71
Sep 30, 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
3 changes: 2 additions & 1 deletion DynamicalSystems.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,9 @@ import DynamicalSystems.Mathlib.Dynamics.Basic
import DynamicalSystems.Mathlib.Topology.Antitone
import DynamicalSystems.Mathlib.Topology.LimitSet
import DynamicalSystems.Stability.Basic
import DynamicalSystems.Stability.Hamiltonian
import DynamicalSystems.Stability.Example
import DynamicalSystems.Stability.Floquet
import DynamicalSystems.Stability.Hamiltonian
import DynamicalSystems.Stability.LaSalle
import DynamicalSystems.Stability.Linearization
import DynamicalSystems.Stability.Lyapunov
Expand Down
Loading
Loading