OAI/Geometry/TamingCompatibility/Charts/
524 declarations, 0 contain sorry, 0 declared as axioms; 68 files
Files
- AffineBase.lean 18 declarations
- AffineLocal.lean 5 declarations
- BundleTotalSpaceT2.lean 1 declarations
- CenterLocalJet.lean 1 declarations
- ChartComponent.lean 9 declarations
- ChartEnergyIntegral.lean 10 declarations
- ChartLift.lean 7 declarations
- ChartMetric.lean 29 declarations
- ChartMetricBounds.lean 8 declarations
- ChartMetricComparison.lean 3 declarations
- ChartOverlapControl.lean 1 declarations
- ChartReconstruction.lean 2 declarations
- ChartScalarBound.lean 5 declarations
- ChartTestPairing.lean 8 declarations
- ChartUnitaryData.lean 19 declarations
- CoefficientCutoff.lean 7 declarations
- CoordinateIntegrand.lean 7 declarations
- Coordinates.lean 17 declarations
- CriticalChartPairing.lean 1 declarations
- CriticalLocalJet.lean 2 declarations
- EuclideanCoordinateLine.lean 10 declarations
- FiniteCharts.lean 15 declarations
- FirstJetGauge.lean 15 declarations
- GeometricCutoff.lean 13 declarations
- GeometricLocalMass.lean 2 declarations
- HermitianBundleSources.lean 18 declarations
- HermitianChartControl.lean 1 declarations
- HermitianCutoffErrors.lean 8 declarations
- HermitianCutoffEstimates.lean 2 declarations
- HermitianCutoffProfiles.lean 10 declarations
- HermitianCutoffSupported.lean 18 declarations
- HermitianManifoldTrace.lean 3 declarations
- InverseCutoff.lean 5 declarations
- LinearTransport.lean 5 declarations
- LocalDDStarEstimate.lean 3 declarations
- LocalFormalAdjoint.lean 17 declarations
- LocalFrameOperator.lean 5 declarations
- LocalInverse.lean 12 declarations
- LocalMatrixOperator.lean 14 declarations
- LocalSmooth.lean 4 declarations
- LocalSmoothPairing.lean 1 declarations
- LocalWeakPatch.lean 1 declarations
- LocalizedHnat.lean 5 declarations
- ManifoldBoundaryBounds.lean 4 declarations
- ManifoldComplexDifferential.lean 5 declarations
- ManifoldScalarCalculus.lean 4 declarations
- MetricCalculus.lean 17 declarations
- QuantitativeLocalStep.lean 1 declarations
- RadialAtlasProducer.lean 1 declarations
- RadialBundleSources.lean 19 declarations
- RadialCutoff.lean 8 declarations
- RadialCutoffErrors.lean 9 declarations
- RadialCutoffGeometry.lean 3 declarations
- RadialCutoffSupported.lean 16 declarations
- RadialOperatorCutoffs.lean 7 declarations
- RadialUnitCoordinates.lean 13 declarations
- RealTestLocality.lean 4 declarations
- RiemannianChartControl.lean 1 declarations
- RiemannianChartPowerMass.lean 1 declarations
- ScalarChartLift.lean 16 declarations
- ShrinkingCutoff.lean 6 declarations
- SlowLogCutoff.lean 8 declarations
- SquareCutoff.lean 2 declarations
- SummableCutoff.lean 13 declarations
- TripleAtlas.lean 1 declarations
- UniformLocalStep.lean 1 declarations
- UnitTransverseLocal.lean 2 declarations
- UnitaryFrames.lean 15 declarations