OAI/Geometry/WeakMTW/Geodesics/
160 declarations, 0 contain sorry, 0 declared as axioms; 43 files
Files
- BundleMinimizerCompactness.lean 7 declarations
- CompactGeodesic.lean 2 declarations
- CompleteExistence.lean 6 declarations
- CostGeodesicTaylor.lean 1 declarations
- DistanceSplitting.lean 2 declarations
- EnergyFirstVariation.lean 1 declarations
- ExtendedMinimizers.lean 2 declarations
- FanEnergySmooth.lean 2 declarations
- FiberSmooth.lean 3 declarations
- FibreNonfocal.lean 4 declarations
- FlowFirstVariation.lean 1 declarations
- FlowVariationInjective.lean 4 declarations
- GaussChartFan.lean 2 declarations
- GaussGlobal.lean 2 declarations
- GaussLemma.lean 1 declarations
- GeneralFirstVariation.lean 1 declarations
- GeodesicDistance.lean 5 declarations
- GeodesicFlow.lean 9 declarations
- GeodesicScaling.lean 2 declarations
- GlobalFirstVariation.lean 2 declarations
- GlobalFlow.lean 3 declarations
- HopfRinow.lean 3 declarations
- InitialScaling.lean 9 declarations
- InjectivityUniqueness.lean 2 declarations
- IntrinsicExistence.lean 3 declarations
- IntrinsicExp.lean 16 declarations
- IntrinsicGlue.lean 8 declarations
- IntrinsicOn.lean 5 declarations
- IntrinsicUniqueness.lean 9 declarations
- LocalFanVariation.lean 6 declarations
- LocalFlow.lean 1 declarations
- LocalGeodesic.lean 1 declarations
- MinimizerCapture.lean 4 declarations
- MinimizerCompactness.lean 8 declarations
- MinimizingCorner.lean 2 declarations
- MinimizingSegments.lean 4 declarations
- NoCorner.lean 2 declarations
- NonconjugateBranches.lean 5 declarations
- ShortChartAction.lean 3 declarations
- ShortFan.lean 2 declarations
- ShortFlowCoordinates.lean 3 declarations
- ShortStates.lean 1 declarations
- UniformNormal.lean 1 declarations