OAI/Analysis/BiholderTransport/CostGeometry/
104 declarations, 0 contain sorry, 0 declared as axioms; 41 files
Files
- ActualPole.lean 4 declarations
- ActualPoleKernel.lean 1 declarations
- BranchActiveGrowth.lean 2 declarations
- BranchCost.lean 1 declarations
- BranchCost2.lean 6 declarations
- BranchGrowth.lean 3 declarations
- BranchJetSecond.lean 1 declarations
- CostGradient.lean 1 declarations
- CostSmooth.lean 1 declarations
- CrossingUniform.lean 1 declarations
- CurveAdvance.lean 5 declarations
- CurvedQuadratic.lean 1 declarations
- DividedAction.lean 1 declarations
- DividedPullback.lean 1 declarations
- ExactTemplateCurvature.lean 6 declarations
- FirstCutLower.lean 4 declarations
- FirstCutSegment.lean 2 declarations
- GraphOpen.lean 1 declarations
- LimitIsolation.lean 3 declarations
- LinearRadialDerivative.lean 1 declarations
- LocalBranchJetBound.lean 1 declarations
- OuterCurvature.lean 6 declarations
- OuterNonconjugacy.lean 1 declarations
- PoleLipschitz.lean 1 declarations
- PrecutExtension.lean 4 declarations
- ProjectionContinuation.lean 3 declarations
- QuantitativeDividedAction.lean 3 declarations
- RadialBounds.lean 1 declarations
- RadialSingular.lean 3 declarations
- RadialVelocityMetricEqualities.lean 2 declarations
- SectionDiameter.lean 1 declarations
- Slack.lean 1 declarations
- SplitEndpoint.lean 2 declarations
- SplitStationary.lean 4 declarations
- SplitTrial.lean 7 declarations
- StrictDividedAction.lean 6 declarations
- UniformFiniteRadialScale.lean 3 declarations
- UniformLocalGap.lean 4 declarations
- UniformRegularSplit.lean 2 declarations
- UniformReverseGain.lean 1 declarations
- UpperTest.lean 2 declarations