OAI/Geometry/IsometricImmersion/Estimates/
98 declarations, 0 contain sorry, 0 declared as axioms; 19 files
Files
- ActualHighEquation.lean 8 declarations
- ActualQApplicability.lean 1 declarations
- ActualQCompactBounds.lean 2 declarations
- ActualQMomentLower.lean 4 declarations
- ActualQMomentPositive.lean 1 declarations
- ActualQPointBounds.lean 1 declarations
- ActualQWeightedRemainder.lean 6 declarations
- ActualRemainderFactors.lean 12 declarations
- ActualRemainderRegularity.lean 3 declarations
- BoundedClassHyperbolicity.lean 4 declarations
- BoundedClassQFloor.lean 2 declarations
- BoundedClassQLow.lean 1 declarations
- FixedRadiusCutBounds.lean 2 declarations
- HighFactorOrders.lean 11 declarations
- LargestBlockLinearization.lean 9 declarations
- MixedRemainderFactors.lean 9 declarations
- MovingSourceBounds.lean 2 declarations
- RemainderAreaBudget.lean 9 declarations
- UniversalQRaw.lean 11 declarations