OAI/Geometry/WeakMTW/Potentials/
152 declarations, 0 contain sorry, 0 declared as axioms; 43 files
Files
- ChartForwardLipschitz.lean 1 declarations
- ChartLocalLipschitz.lean 2 declarations
- CompactFamilyControl.lean 2 declarations
- CompactSmoothControl.lean 2 declarations
- CovectorFlow.lean 6 declarations
- DiagonalEnvelope.lean 6 declarations
- FiniteGlobalSupport.lean 4 declarations
- GlobalSupportTheorem.lean 1 declarations
- GradientCoordinates.lean 2 declarations
- IntermediateAtlas.lean 2 declarations
- IntermediateCoordinates.lean 1 declarations
- IntermediateCovectors.lean 4 declarations
- IntermediateDefinitions.lean 3 declarations
- IntermediateDuality.lean 8 declarations
- IntermediateGradient.lean 5 declarations
- IntermediateGrowth.lean 2 declarations
- IntermediateGrowthLocal.lean 4 declarations
- IntermediateGrowthMetric.lean 1 declarations
- IntermediateMomentumLipschitz.lean 3 declarations
- IntermediateParameterFamily.lean 5 declarations
- IntermediatePoleLipschitz.lean 1 declarations
- IntermediateRegularity.lean 2 declarations
- IntermediateStatement.lean 1 declarations
- IntermediateTheorem.lean 1 declarations
- IntermediateUniformBounds.lean 7 declarations
- IntermediateUniformLipschitz.lean 2 declarations
- IntermediateUniformRegularity.lean 1 declarations
- LiftedSectionDefinitions.lean 4 declarations
- LiftedSections.lean 10 declarations
- LiftedSectionsTheorem.lean 1 declarations
- OrdinarySubgradientCapture.lean 2 declarations
- OrdinarySubgradientIdentity.lean 5 declarations
- ParametricEnvelopeBounds.lean 1 declarations
- PositiveEnvelope.lean 4 declarations
- PotentialActiveLogs.lean 11 declarations
- PotentialDefinitions.lean 7 declarations
- PotentialFiniteReduction.lean 3 declarations
- PotentialGraphGlobal.lean 6 declarations
- QuadraticEnvelope.lean 3 declarations
- ReverseGeodesic.lean 8 declarations
- SmoothEnvelope.lean 5 declarations
- SmoothMetricLipschitz.lean 2 declarations
- UniformLocalLipschitz.lean 1 declarations