OAI/Analysis/BiholderTransport/Geodesics/
155 declarations, 0 contain sorry, 0 declared as axioms; 38 files
Files
- BranchExtension.lean 3 declarations
- ChartLipschitz.lean 2 declarations
- CompleteSpray.lean 1 declarations
- DoubleMountain.lean 4 declarations
- EndpointIdentity.lean 4 declarations
- ExpInteriorUnique.lean 2 declarations
- GaussLemma.lean 3 declarations
- GeodesicBasics.lean 5 declarations
- GeodesicExistence.lean 5 declarations
- GeodesicSpray.lean 8 declarations
- GlobalGauss.lean 3 declarations
- GoodContact.lean 1 declarations
- GraphGlobalMinimal.lean 3 declarations
- InjectivityOpen.lean 4 declarations
- IntegratedGauss.lean 2 declarations
- MetricCurveLocal.lean 1 declarations
- MetricCurveSpeed.lean 1 declarations
- MetricGeodesicLift.lean 7 declarations
- MetricSegments.lean 7 declarations
- MinimizingChartParameters.lean 6 declarations
- MinimizingCoordinateLimit.lean 2 declarations
- MinimizingSubinterval.lean 3 declarations
- NoCorner.lean 4 declarations
- NormalEndpointLog.lean 7 declarations
- OriginalMass.lean 3 declarations
- RayAdvance.lean 4 declarations
- ReverseSpectrum.lean 5 declarations
- ShortGradient.lean 6 declarations
- SplitMinimizingAction.lean 2 declarations
- SprayActionMinimum.lean 3 declarations
- SprayDistanceBound.lean 12 declarations
- SprayEnergy.lean 6 declarations
- SprayMinimizerUnique.lean 5 declarations
- SprayMinimizing.lean 2 declarations
- SprayNonconjugacy.lean 1 declarations
- SprayProjection.lean 12 declarations
- SprayScaling.lean 4 declarations
- UniformFixedCrossing.lean 2 declarations