OAI/Geometry/IsometricImmersion/Metrics/
266 declarations, 0 contain sorry, 0 declared as axioms; 26 files
Files
- ActualLowMetricBudget.lean 4 declarations
- ActualLowMetricFloor.lean 3 declarations
- ActualTestMetricPositive.lean 5 declarations
- AffineTensorNeighborhood.lean 8 declarations
- FixedMetricRemainder.lean 3 declarations
- LocalMetricPCoefficients.lean 7 declarations
- LocalMetricQActive.lean 5 declarations
- LocalMetricQFull.lean 4 declarations
- MetricCompatibility.lean 9 declarations
- MetricHorizontalRequests.lean 2 declarations
- MetricLocality.lean 17 declarations
- MetricPBundleBounds.lean 11 declarations
- MetricPatchOpen.lean 14 declarations
- MetricQSpatialBundle.lean 11 declarations
- MetricSmoothness.lean 9 declarations
- ModelCoercivity.lean 14 declarations
- ModelMetric.lean 12 declarations
- ModelProfile.lean 29 declarations
- PatchTensorPositivity.lean 5 declarations
- PatchTensorRestriction.lean 15 declarations
- RemainderCoefficientBounds.lean 8 declarations
- SmoothMetricRestriction.lean 1 declarations
- StateCoefficientTube.lean 14 declarations
- UniversalMetricP.lean 26 declarations
- UniversalMetricQ.lean 12 declarations
- WarpedMetric.lean 18 declarations