OAI/Geometry/SmoothYau/Limits/
193 declarations, 0 contain sorry, 0 declared as axioms; 37 files
Files
- ActualProfileMassPos.lean 3 declarations
- C1ExtensionNearCompact.lean 1 declarations
- ChartExtDualNorm.lean 2 declarations
- ClosedPhaseMatrixValid.lean 3 declarations
- CompactActualMetricPackets.lean 1 declarations
- CompactActualMetricPacketsSupported.lean 1 declarations
- CompactActualWaveNoncancellation.lean 2 declarations
- CompactActualWavesSubregionsSupported.lean 3 declarations
- CompactExponentialEnvelopeLogBound.lean 1 declarations
- CompactExteriorBackgroundDomination.lean 1 declarations
- CompactFiberLocalCompBound.lean 2 declarations
- CompactFullProfileMargin.lean 23 declarations
- CompactMetricPacketSignGain.lean 1 declarations
- CompactNormalForwardBound.lean 2 declarations
- CompactNormalImageNeighborhood.lean 1 declarations
- CompactProfileCanonicalSmallBall.lean 4 declarations
- CompactProfileUnitLipschitz.lean 5 declarations
- CompactStrictProfileRatio.lean 1 declarations
- ContinuousGradientIterated.lean 1 declarations
- CoordinateForm.lean 18 declarations
- CubicConstantNonneg.lean 6 declarations
- CutoffFactorCompactRaw.lean 12 declarations
- ExistsCompactSignedEnvelope.lean 3 declarations
- FrameDualNorm.lean 9 declarations
- IntegrableCompactTsupport.lean 2 declarations
- LocalMetricInverse.lean 6 declarations
- ManifoldChartPush.lean 6 declarations
- ManifoldSobolevInclusionCoordinate.lean 11 declarations
- OscDualNorm.lean 4 declarations
- PhaseImagVector.lean 8 declarations
- PlanePairMap.lean 12 declarations
- RadialMetricDualNorm.lean 3 declarations
- RealMatrixCauchy.lean 6 declarations
- RestrictedPinningPencil.lean 7 declarations
- ScalarCauchyCross.lean 11 declarations
- SphericalFixedFormNorm.lean 4 declarations
- SupportedPinningTensor.lean 7 declarations