OAI/Geometry/NearbyLagrangian/
1508 declarations, 0 contain sorry, 0 declared as axioms; 93 files
Files
- AnalyticObstruction.lean 7 declarations
- BalancedCoordinates.lean 11 declarations
- BalancedStability.lean 18 declarations
- ClosedRealization.lean 9 declarations
- CompleteFlow.lean 11 declarations
- CoreEndpoint.lean 1 declarations
- CotangentForms.lean 23 declarations
- CotangentLifts.lean 8 declarations
- CotangentModel.lean 17 declarations
- CotangentProducts.lean 19 declarations
- CriticalLocus.lean 10 declarations
- CriticalSections.lean 13 declarations
- CylinderCutoffs.lean 13 declarations
- CylinderEquations.lean 3 declarations
- CylinderFamilies.lean 16 declarations
- CylinderRegularity.lean 9 declarations
- CylinderTransport.lean 7 declarations
- Evolution.lean 17 declarations
- FamilyApproximation.lean 12 declarations
- FiberHomotopy.lean 17 declarations
- FiberJets.lean 14 declarations
- FiniteTransport.lean 7 declarations
- FlatCotangent.lean 29 declarations
- FlowLevels.lean 10 declarations
- GeneratingAction.lean 27 declarations
- GeneratingEmbeddings.lean 15 declarations
- GeneratingGeometry.lean 17 declarations
- HamiltonianCharts.lean 11 declarations
- HamiltonianFlow.lean 30 declarations
- HomogeneousCritical.lean 17 declarations
- HomogeneousFunctions.lean 28 declarations
- HomogeneousTails.lean 8 declarations
- Immersions.lean 12 declarations
- ImplicitRoots.lean 4 declarations
- IntrinsicCylinder.lean 21 declarations
- IntrinsicRealization.lean 16 declarations
- Isotopies.lean 27 declarations
- JetApproximation.lean 4 declarations
- JetTopology.lean 9 declarations
- Latitude.lean 39 declarations
- LiouvilleDifferentials.lean 7 declarations
- Main.lean 86 imports, no declarations
- MainReduction.lean 4 declarations
- MixedGraphs.lean 11 declarations
- MomentumSeparation.lean 9 declarations
- MorseTransport.lean 6 declarations
- NearIdentity.lean 16 declarations
- NegativeEquivalence.lean 14 declarations
- NegativeSuspension.lean 21 declarations
- OpenCylinders.lean 27 declarations
- ParameterFlows.lean 8 declarations
- Phase.lean 14 declarations
- PhaseConjugacy.lean 15 declarations
- PhaseErrors.lean 26 declarations
- PhaseRegularity.lean 24 declarations
- PicardPaths.lean 10 declarations
- PolarCharts.lean 26 declarations
- PositiveSquares.lean 18 declarations
- ProductSymplectic.lean 6 declarations
- QuadraticStability.lean 28 declarations
- RadialBlending.lean 23 declarations
- RadialTrapping.lean 13 declarations
- Radialization.lean 18 declarations
- RealizationFamilies.lean 11 declarations
- RealizationInjectivity.lean 3 declarations
- RealizationRegularity.lean 10 declarations
- RelativeApproximation.lean 4 declarations
- Restoration.lean 16 declarations
- RestoredRestriction.lean 10 declarations
- SmoothCore.lean 35 declarations
- SmoothFamilies.lean 23 declarations
- SmoothTubeApproximation.lean 8 declarations
- SphereCollapse.lean 32 declarations
- SphereFields.lean 10 declarations
- SphereHeights.lean 23 declarations
- SphereSuspension.lean 33 declarations
- SquareCoordinates.lean 17 declarations
- Stabilization.lean 18 declarations
- StableFibers.lean 59 declarations
- StandardNegative.lean 25 declarations
- StepData.lean 38 declarations
- Superposition.lean 16 declarations
- SupportedEvolution.lean 21 declarations
- SuspensionEquivalence.lean 33 declarations
- SymplecticCylinder.lean 15 declarations
- TameBounds.lean 16 declarations
- TelescopeClasses.lean 16 declarations
- TelescopeKernel.lean 14 declarations
- TimeMesh.lean 8 declarations
- TransportCutoffs.lean 19 declarations
- TubeClasses.lean 31 declarations
- TubeKernel.lean 2 declarations
- VerticalChanges.lean 12 declarations