OAI/Geometry/WeakHessian/Calculus/
165 declarations, 0 contain sorry, 0 declared as axioms; 51 files
Files
- CompactAnchoredControl.lean 4 declarations
- CompactCoreAnnihilator.lean 2 declarations
- CompactCoreEquation.lean 1 declarations
- CompactCoreForm.lean 1 declarations
- CompactCoreIdentity.lean 1 declarations
- CompactCoreLocalization.lean 2 declarations
- CompactCoreRegularity.lean 1 declarations
- CompactCost.lean 3 declarations
- CompactEVI.lean 1 declarations
- CompactHopf.lean 4 declarations
- CompactHopfCurve.lean 2 declarations
- CompactHopfDualLimit.lean 3 declarations
- CompactLipDense.lean 3 declarations
- CompactOriginalCore.lean 1 declarations
- CompactSlopeApprox.lean 3 declarations
- CompactThickenedIndicator.lean 3 declarations
- ControlNorm.lean 9 declarations
- DerivSinSubMul.lean 14 declarations
- DominatedCompactRerouting.lean 1 declarations
- DriftRadialLimit.lean 2 declarations
- DualLimits.lean 6 declarations
- ELpNormSq.lean 8 declarations
- FormLimits.lean 8 declarations
- GammaLimits.lean 5 declarations
- IntegralEvalDifference.lean 2 declarations
- IntegralHopfInitial.lean 3 declarations
- IntegralSqFatou.lean 1 declarations
- InverseSqrtIntegral.lean 3 declarations
- LipschitzDerivQuadraticRemainder.lean 3 declarations
- LipschitzMulCompact.lean 3 declarations
- LipschitzPointLimit.lean 3 declarations
- LocalDistribution.lean 1 declarations
- NoncompactCost.lean 3 declarations
- NoncompactOptimal.lean 2 declarations
- NormLpSqIntegral.lean 2 declarations
- NormSqLintegralEnorm.lean 4 declarations
- NormalizedRadial.lean 4 declarations
- NormalizedRoots.lean 3 declarations
- PotentialCompactness.lean 1 declarations
- QuadraticCompactness.lean 1 declarations
- QuadraticCostLimit.lean 3 declarations
- RadialGammaLimit.lean 2 declarations
- ReversePoincareIntegral.lean 1 declarations
- RightEndpointDerivative.lean 1 declarations
- RnDerivRestrictReference.lean 5 declarations
- RnDerivSmul.lean 3 declarations
- ScalarLocalBound.lean 2 declarations
- ScalarSecondDifference.lean 12 declarations
- TendstoIntegralBoundedPairing.lean 3 declarations
- TriangularFoldNorm.lean 4 declarations
- VariableDissipationLimits.lean 2 declarations