-
Notifications
You must be signed in to change notification settings - Fork 5
Expand file tree
/
Copy pathLeanForControl.lean
More file actions
56 lines (56 loc) · 2.92 KB
/
Copy pathLeanForControl.lean
File metadata and controls
56 lines (56 loc) · 2.92 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
import LeanForControl.Analysis.Continuity
import LeanForControl.Analysis.FrechetRemainder
import LeanForControl.Analysis.Integrals
import LeanForControl.Analysis.MonotoneFunctions
import LeanForControl.Analysis.SpectralRadius
import LeanForControl.Comparison.Axioms
import LeanForControl.Comparison.ClassK
import LeanForControl.Comparison.ClassKInfty
import LeanForControl.Comparison.ClassKL
import LeanForControl.Comparison.ClassL
import LeanForControl.Comparison.ComparisonFunctions
import LeanForControl.Dini.DiniDeriv
import LeanForControl.LinearSystems.Basic
import LeanForControl.LinearSystems.Controllability.Controllability
import LeanForControl.LinearSystems.Controllability.Defs
import LeanForControl.LinearSystems.Controllability.Hautus
import LeanForControl.LinearSystems.Controllability.Reachability
import LeanForControl.LinearSystems.KalmanDecomposition.Decomposition
import LeanForControl.LinearSystems.KalmanDecomposition.DecompositionExamples
import LeanForControl.LinearSystems.KalmanDecomposition.Defs
import LeanForControl.LinearSystems.Observability.Defs
import LeanForControl.LinearSystems.Observability.Hautus
import LeanForControl.LinearSystems.Observability.Observability
import LeanForControl.LinearSystems.Solutions.CtsLTI
import LeanForControl.LinearSystems.Solutions.CtsLTV
import LeanForControl.LinearSystems.Solutions.DefsCtsLTV
import LeanForControl.LinearSystems.Solutions.DefsDiscLTV
import LeanForControl.LinearSystems.Solutions.DiscLTV
import LeanForControl.LinearSystems.Stability.Continuous.DefsHurwitz
import LeanForControl.LinearSystems.Stability.Continuous.ExponentialStability
import LeanForControl.LinearSystems.Stability.Continuous.Hurwitz
import LeanForControl.LinearSystems.Stability.Continuous.InstabilityCertificate
import LeanForControl.LinearSystems.Stability.Continuous.LyapunovEquation
import LeanForControl.MatrixAlgebra.Exponential
import LeanForControl.MatrixAlgebra.QuadraticForm
import LeanForControl.MatrixAlgebra.Rank
import LeanForControl.MatrixAlgebra.Spectrum
import LeanForControl.ODEs.ComparisonLemma
import LeanForControl.ODEs.GronwallBellman
import LeanForControl.ODEs.ODE_properties
import LeanForControl.Stability.Autonomous
import LeanForControl.Stability.ClassKDecay
import LeanForControl.Stability.DefsAutonomous
import LeanForControl.Stability.DefsNonAutonomous
import LeanForControl.Stability.KLCharacterization
import LeanForControl.Stability.KLCharacterizationTools
import LeanForControl.Stability.LaSalle
import LeanForControl.Stability.LyapunovBounds
import LeanForControl.Stability.LyapunovIndirect.Chetaev
import LeanForControl.Stability.LyapunovIndirect.DefsDynamics
import LeanForControl.Stability.LyapunovIndirect.Linearization
import LeanForControl.Stability.LyapunovIndirect.LinearizationInstability
import LeanForControl.Stability.LyapunovIndirect.Lyapunov
import LeanForControl.Stability.LyapunovIndirect.NonlinearInstability
import LeanForControl.Stability.NonAutonomous
import LeanForControl.axioms