OAI/Geometry/Immersion/ClosedSurface/
1056 declarations, 0 contain sorry, 0 declared as axioms; 97 files
Files
- AssembledMean.lean 6 declarations
- AtlasDecomposition.lean 6 declarations
- AtlasDenominators.lean 3 declarations
- AtlasLabels.lean 5 declarations
- AtlasMargins.lean 6 declarations
- AtlasPartition.lean 2 declarations
- AtlasPhases.lean 11 declarations
- AtlasWeights.lean 6 declarations
- ChartModel.lean 13 declarations
- ChartTransition.lean 12 declarations
- CompactPartition.lean 5 declarations
- ComplexPullback.lean 16 declarations
- CoordinateBounds.lean 1 declarations
- CoordinateMargins.lean 5 declarations
- CrossModes.lean 18 declarations
- DenominatorBounds.lean 5 declarations
- DirectionStability.lean 8 declarations
- DoubleModes.lean 7 declarations
- ExplicitIncrement.lean 2 declarations
- ExtendedCancellation.lean 5 declarations
- FiniteIncrement.lean 6 declarations
- FiniteMean.lean 11 declarations
- ForcedModes.lean 18 declarations
- ForcedSolve.lean 10 declarations
- FreeAmplitude.lean 9 declarations
- FreeCharts.lean 11 declarations
- FreeMean.lean 4 declarations
- FreeSolve.lean 5 declarations
- GeometryBounds.lean 8 declarations
- GlobalPartition.lean 8 declarations
- GoodAtlas.lean 4 declarations
- GoodDirections.lean 8 declarations
- GoodPhases.lean 7 declarations
- GradientBounds.lean 9 declarations
- GridBumps.lean 12 declarations
- GridCover.lean 8 declarations
- GridPartition.lean 14 declarations
- GridPhases.lean 4 declarations
- ImmersionJets.lean 7 declarations
- JacobianBounds.lean 5 declarations
- JetBounds.lean 20 declarations
- LengthMargins.lean 8 declarations
- LocalMean.lean 12 declarations
- LocalPhaseData.lean 5 declarations
- Main.lean 5 declarations
- MeanBilinearity.lean 10 declarations
- MeanDifferences.lean 9 declarations
- MeanError.lean 10 declarations
- MeanSupport.lean 11 declarations
- MetricAmplitude.lean 5 declarations
- MetricBounds.lean 8 declarations
- MetricCoordinates.lean 4 declarations
- MetricModel.lean 6 declarations
- MetricPatches.lean 6 declarations
- MetricPullback.lean 12 declarations
- MetricTensors.lean 15 declarations
- ModeBounds.lean 71 declarations
- ModeDifferences.lean 8 declarations
- ModeScaling.lean 15 declarations
- NormalFrame.lean 18 declarations
- NormalJets.lean 8 declarations
- NormalProjection.lean 6 declarations
- OscillationBounds.lean 9 declarations
- OscillatoryModel.lean 129 declarations
- PhaseCancellation.lean 5 declarations
- PhaseCoordinates.lean 9 declarations
- PhaseDecomposition.lean 3 declarations
- PhaseDifferentials.lean 6 declarations
- PhaseGrid.lean 15 declarations
- PhaseMean.lean 18 declarations
- PhasePatches.lean 3 declarations
- PhaseStock.lean 12 declarations
- PhaseWeights.lean 4 declarations
- PolynomialPhases.lean 3 declarations
- PositiveBasis.lean 9 declarations
- ProjectionBounds.lean 8 declarations
- ProjectionStability.lean 7 declarations
- PullbackBounds.lean 10 declarations
- QuadraticCorrection.lean 8 declarations
- QuadraticError.lean 11 declarations
- QuadraticMean.lean 32 declarations
- QuadraticSupport.lean 10 declarations
- RealBounds.lean 9 declarations
- RealModes.lean 27 declarations
- RootMean.lean 11 declarations
- SecondForms.lean 16 declarations
- SmallRealization.lean 2 declarations
- SmoothCoordinates.lean 12 declarations
- SquarePartition.lean 2 declarations
- SupportedCancellation.lean 10 declarations
- TangentDecomposition.lean 5 declarations
- TensorBounds.lean 6 declarations
- TensorCoordinates.lean 8 declarations
- UniformIncrement.lean 7 declarations
- UniformMean.lean 4 declarations
- WeightMargins.lean 7 declarations
- WeightedBounds.lean 37 declarations