`OAI/Geometry/SurfaceImmersion/Atlas/`

1216 declarations, 0 contain sorry, 0 declared as axioms; 368 files

Files

ActualPhaseGoodness.lean 1 declarations
AnchoredAtlasIncrement.lean 2 declarations
AnchoredAtlasPhases.lean 5 declarations
AnchoredGridCover.lean 1 declarations
AnchoredGridPhases.lean 1 declarations
AtlasAmplitudeReadBounds.lean 1 declarations
AtlasAmplitudeSupport.lean 1 declarations
AtlasBackgroundLowerBound.lean 2 declarations
AtlasCatalogCancellation.lean 1 declarations
AtlasCombinedCancellation.lean 1 declarations
AtlasCompactPhaseWeights.lean 1 declarations
AtlasFiniteCancellation.lean 4 declarations
AtlasGlobalQuadratic.lean 4 declarations
AtlasGoodPhaseCancellation.lean 1 declarations
AtlasImmersionGeometry.lean 4 declarations
AtlasIncrementBound.lean 2 declarations
AtlasIncrementIdentity.lean 1 declarations
AtlasInputBaseline.lean 1 declarations
AtlasInputPhaseCancellation.lean 2 declarations
AtlasJetCoordinateRelation.lean 9 declarations
AtlasJetReadBounds.lean 1 declarations
AtlasLinearMapBounds.lean 3 declarations
AtlasLowJetNeighborhood.lean 1 declarations
AtlasMetricBounds.lean 3 declarations
AtlasMetricExpansion.lean 5 declarations
AtlasMetricJetFamily.lean 2 declarations
AtlasMetricJetMargins.lean 3 declarations
AtlasMetricLimit.lean 6 declarations
AtlasMetricLowerBound.lean 1 declarations
AtlasMetricRead.lean 2 declarations
AtlasMetricReadGerms.lean 3 declarations
AtlasNearbyPhaseCancellation.lean 2 declarations
AtlasNormalProjection.lean 14 declarations
AtlasNormalProjectionBounds.lean 8 declarations
AtlasNormalizationBounds.lean 5 declarations
AtlasNormalizationStability.lean 3 declarations
AtlasOuterDomains.lean 1 declarations
AtlasOuterPlateau.lean 1 declarations
AtlasPhaseCatalog.lean 9 declarations
AtlasPhaseChartBounds.lean 1 declarations
AtlasPhaseJetBounds.lean 1 declarations
AtlasPhaseNormalMargin.lean 1 declarations
AtlasPhaseReadBounds.lean 1 declarations
AtlasPhaseStability.lean 2 declarations
AtlasProjectionStability.lean 2 declarations
AtlasPureMargins.lean 2 declarations
AtlasQuadraticBounds.lean 1 declarations
AtlasQuadraticTargets.lean 5 declarations
AtlasReadGerms.lean 3 declarations
AtlasSecondFormMargin.lean 2 declarations
AtlasSelfTensorRead.lean 1 declarations
AtlasSphericalTensorBound.lean 2 declarations
AtlasSupportedWeights.lean 7 declarations
AtlasTensorDerivatives.lean 2 declarations
AtlasTensorLocalBounds.lean 1 declarations
AtlasTensorTransition.lean 9 declarations
AtlasUniformNorm.lean 3 declarations
AtlasWeightedBounds.lean 3 declarations
AxisParameterCoordinates.lean 5 declarations
BundleAtlasBounds.lean 3 declarations
BundleCutoffCoordinates.lean 4 declarations
CatalogPhaseBounds.lean 1 declarations
CenteredAtlasDifferentials.lean 4 declarations
CenteredConvexPhase.lean 16 declarations
CenteredParabolicChart.lean 11 declarations
ChartDisplacement.lean 4 declarations
ChartFullLinearization.lean 3 declarations
ChartGermImmersion.lean 1 declarations
ChartImmersionReplacement.lean 1 declarations
ChartMapReplacement.lean 1 declarations
ChartPushforward.lean 5 declarations
ChartReadSupport.lean 2 declarations
ChartSecondFormBounds.lean 2 declarations
ChartedLeadingTensor.lean 4 declarations
ChartedPartitionLeading.lean 3 declarations
ChartedTrialAmplitude.lean 3 declarations
ChartedTrialMajorants.lean 1 declarations
ChartedUniformAmplitude.lean 1 declarations
ChartedUniformMajorants.lean 1 declarations
ChartedUniformSeed.lean 1 declarations
CombinedTensorBounds.lean 1 declarations
CompactCoordinatePullback.lean 2 declarations
CompactCurvePhaseParameters.lean 3 declarations
CompactLocalChart.lean 1 declarations
CompactPhaseCancellation.lean 1 declarations
CompactPhaseChart.lean 1 declarations
CompactPhaseCurveVectors.lean 5 declarations
CompactPhaseDiskTopology.lean 2 declarations
CompactPhaseFamily.lean 8 declarations
CompactPhasePartition.lean 6 declarations
CompactPhaseSolverFamily.lean 1 declarations
CompactPhaseSolvers.lean 1 declarations
CompactPhaseWeights.lean 2 declarations
CompactTimeChart.lean 1 declarations
ConvexPhaseDecomposition.lean 10 declarations
ConvexQuadraticPhase.lean 23 declarations
CoordinateAxisDerivative.lean 1 declarations
CoordinateC1Bounds.lean 1 declarations
CoordinateGauss.lean 4 declarations
CoordinateImmersionReplacement.lean 1 declarations
CoordinateInverseGerm.lean 1 declarations
CoordinateIsometryMetric.lean 2 declarations
CoordinateNonlinearBounds.lean 5 declarations
CoordinatePushforward.lean 5 declarations
CoordinateQuadraticExpansion.lean 9 declarations
CoordinateRegularReplacement.lean 1 declarations
CoordinateSardThree.lean 4 declarations
CoordinateTaylorIdentity.lean 5 declarations
CoordinateTensorPullback.lean 16 declarations
CoordinateTransverseDerivative.lean 2 declarations
CorrectedSeedCoordinates.lean 4 declarations
CrossAtlasBounds.lean 3 declarations
CrossAtlasExactGeometry.lean 1 declarations
CrossAtlasJetRelation.lean 8 declarations
CrossAtlasOuterGeometry.lean 3 declarations
CrossAtlasShiftedBounds.lean 1 declarations
CrossAtlasTensorBounds.lean 2 declarations
CrossAtlasTensorTransition.lean 8 declarations
CrossPhaseExteriorControl.lean 1 declarations
CurvePhaseCriticalValues.lean 3 declarations
CurvePhaseParameterGraph.lean 6 declarations
CutoffFlatJetBound.lean 1 declarations
CutoffQuadraticBounds.lean 2 declarations
DisjointAtlasBounds.lean 1 declarations
EmbeddingNeighborhoodChart.lean 1 declarations
EuclideanChartRead.lean 5 declarations
ExtendedPhaseChart.lean 2 declarations
FastPhaseBounds.lean 4 declarations
FiniteAtlasIncrement.lean 5 declarations
FiniteChartTranslationBound.lean 2 declarations
FiniteCriticalQuadraticPhases.lean 3 declarations
FinitePhaseCurveDefiners.lean 1 declarations
FinitePointChartBalls.lean 1 declarations
FixedAtlasSmallIncrement.lean 1 declarations
FixedAtlasStartingFamily.lean 1 declarations
FixedChartGeometry.lean 4 declarations
FixedChartNonlinearSolver.lean 3 declarations
FlatJetWeightedBound.lean 1 declarations
FlatTransverseCutoff.lean 1 declarations
GenericAtlasPhases.lean 2 declarations
GenericCoordinateLevels.lean 3 declarations
GenericCurvePhases.lean 4 declarations
GenericIndependentPhases.lean 1 declarations
GenericPulledPhases.lean 1 declarations
GeometricAtlasSmallIncrement.lean 1 declarations
GlobalPhaseGerms.lean 4 declarations
GoodPhaseC2Stability.lean 4 declarations
GoodPhaseCover.lean 3 declarations
GoodPhaseNeighborhood.lean 2 declarations
GoodPhaseSolver.lean 1 declarations
GoodPhaseStability.lean 6 declarations
GoodPhaseTargetSplit.lean 1 declarations
GoodQuadraticAtlasPhases.lean 1 declarations
GridAdjustedIncrement.lean 1 declarations
GridAtlasMetric.lean 1 declarations
GridCardinality.lean 2 declarations
GridCellGeometry.lean 1 declarations
GridCutoffBounds.lean 1 declarations
GridCutoffSupport.lean 7 declarations
GridGeometricIncrement.lean 1 declarations
GridIncrementEnvelope.lean 10 declarations
GridPhaseCutoffs.lean 4 declarations
GridRestoredGeometry.lean 6 declarations
GridSupportedCutoffs.lean 4 declarations
HalfIntervalChart.lean 1 declarations
ImmersedAtlasNormal.lean 3 declarations
IndependentExactPhase.lean 1 declarations
IndependentPhaseProjections.lean 5 declarations
IndependentShrinkingWeights.lean 1 declarations
IndependentTensorReadTolerance.lean 1 declarations
IndependentUniformPhase.lean 1 declarations
InducedMetricReadTolerance.lean 1 declarations
InputAtlasSmallIncrement.lean 2 declarations
IntervalInteriorCutoff.lean 1 declarations
IntrinsicPhaseChartGeometry.lean 2 declarations
JetMetricCoordinatePullback.lean 4 declarations
JetPhaseChartFromReal.lean 8 declarations
JoinTimeCharts.lean 1 declarations
LineChartEndpointObstruction.lean 2 declarations
LinearMetricChartReconstruction.lean 2 declarations
LinearPhaseBudgets.lean 1 declarations
LinearPhaseChart.lean 8 declarations
LinearPhaseCutoffBounds.lean 3 declarations
LinearPhaseDerivativeBounds.lean 3 declarations
LinearPhaseTwoJetBounds.lean 3 declarations
LocalAnsatzMetricLimit.lean 6 declarations
LocalGenericAtlasPhases.lean 1 declarations
LocalReferencePhaseBasis.lean 1 declarations
LocalizedCoordinatePullback.lean 6 declarations
LogarithmicCutoff.lean 8 declarations
LogarithmicCutoffDerivative.lean 1 declarations
LowJetCoordinateChange.lean 21 declarations
MatchedSubsetChart.lean 1 declarations
MetricAtlasReference.lean 5 declarations
MetricChartReconstruction.lean 1 declarations
MetricGoodPhaseData.lean 2 declarations
MetricReadBounds.lean 2 declarations
MixedAtlasGeometry.lean 2 declarations
NoncriticalPhaseBudgets.lean 1 declarations
NoncriticalPhaseCover.lean 3 declarations
NonlinearAtlasAnsatz.lean 7 declarations
NonlinearAtlasErrorBound.lean 2 declarations
NonlinearAtlasMapBound.lean 1 declarations
NonlinearAtlasMetric.lean 2 declarations
NonlinearPhaseFrameMargins.lean 4 declarations
NonparallelPhaseCovectors.lean 6 declarations
NormalDefectCoordinates.lean 7 declarations
OneFiberChart.lean 1 declarations
OuterChartDifferential.lean 2 declarations
OuterPhaseConvexity.lean 1 declarations
OuterPhaseGeometry.lean 5 declarations
PairChartSard.lean 4 declarations
PairCurveChartDerivative.lean 1 declarations
ParabolicPhaseChart.lean 11 declarations
PhaseAnsatzNormal.lean 3 declarations
PhaseBasisPerturbation.lean 11 declarations
PhaseBoundaryAvoidance.lean 1 declarations
PhaseBoundaryCurve.lean 12 declarations
PhaseBoundaryMatching.lean 1 declarations
PhaseChartBounds.lean 1 declarations
PhaseChartGeometry.lean 5 declarations
PhaseChartJetTransfer.lean 2 declarations
PhaseChartNormalField.lean 2 declarations
PhaseChartNormalTransport.lean 2 declarations
PhaseChartRealization.lean 4 declarations
PhaseChartStability.lean 3 declarations
PhaseChartTransition.lean 4 declarations
PhaseCoordinateCovector.lean 3 declarations
PhaseCovectorFamily.lean 6 declarations
PhaseCovectorRead.lean 1 declarations
PhaseCurvePairGeometry.lean 4 declarations
PhaseDenominatorNeighborhood.lean 4 declarations
PhaseDiskNormalGluing.lean 2 declarations
PhaseDiskSupport.lean 1 declarations
PhaseExteriorControl.lean 4 declarations
PhaseExteriorDomain.lean 4 declarations
PhaseExteriorPreservation.lean 2 declarations
PhaseFrameMargins.lean 4 declarations
PhaseFrontierAvoidance.lean 1 declarations
PhaseGaussBound.lean 1 declarations
PhaseGaussRepresentative.lean 1 declarations
PhaseMarginCompact.lean 4 declarations
PhaseMetricConvexity.lean 3 declarations
PhaseMetricPositive.lean 1 declarations
PhaseMetricRead.lean 5 declarations
PhaseMetricRegion.lean 1 declarations
PhaseMetricRegularity.lean 2 declarations
PhaseNormalLift.lean 2 declarations
PhaseNormalNeighborhood.lean 2 declarations
PhaseNormalTripleMargin.lean 2 declarations
PhaseOrdinaryCoordinates.lean 4 declarations
PhaseOuterImmersion.lean 3 declarations
PhaseParameterBalls.lean 1 declarations
PhaseReparametrization.lean 5 declarations
PhaseSphericalGeometry.lean 1 declarations
PhaseSupportCoordinates.lean 6 declarations
PhaseTargetCongruence.lean 1 declarations
PhaseTransitionCocycle.lean 6 declarations
PhaseTransitionRegularity.lean 1 declarations
PhaseTransitionVectors.lean 2 declarations
PhaseTransverseDefiner.lean 4 declarations
PlaneCommonCoordinate.lean 7 declarations
PlaneCurveCoordinates.lean 4 declarations
PreferredNormalPhasePullback.lean 6 declarations
PreparedPointCoordinates.lean 1 declarations
PrescribedAtlasPatch.lean 1 declarations
PrescribedAtlasPlateau.lean 1 declarations
QuadraticCutoffBounds.lean 13 declarations
QuadraticJetCutoff.lean 10 declarations
QuadraticPhaseCatalog.lean 3 declarations
QualitativePhaseTransfer.lean 2 declarations
RadialFormCoordinateTransfer.lean 1 declarations
RealPhaseChart.lean 7 declarations
RealTensorChart.lean 5 declarations
ReferenceCoordinateData.lean 4 declarations
ReferencePhaseC1.lean 1 declarations
RegularCoordinateSard.lean 1 declarations
RegularCurveCoordinates.lean 1 declarations
RegularPlaneChart.lean 1 declarations
RegularThreeChart.lean 1 declarations
RelativePhaseCancellation.lean 1 declarations
RestoredPhaseGeometry.lean 2 declarations
RestrictedPhasePartition.lean 2 declarations
RestrictedPhaseTransition.lean 1 declarations
ScalarCoordinateAugmentation.lean 1 declarations
ScalarSubmersionChart.lean 1 declarations
SelectedGridGeometry.lean 5 declarations
ShrinkingAtlasWeightBounds.lean 1 declarations
ShrinkingJetCutoff.lean 6 declarations
ShrinkingWeightBounds.lean 2 declarations
ShrinkingWeightContinuity.lean 7 declarations
ShrinkingWeightMultiplier.lean 1 declarations
SpatialPhaseBasis.lean 8 declarations
SphericalCoordinateSecondForm.lean 1 declarations
SphericalMetricPhaseData.lean 7 declarations
SubmersionFiberLineChart.lean 1 declarations
SupportedAtlasDifferential.lean 3 declarations
SupportedAtlasMetric.lean 4 declarations
SupportedAtlasRestore.lean 4 declarations
SupportedChartEquiv.lean 7 declarations
SupportedChartPullback.lean 5 declarations
SupportedChartTransport.lean 8 declarations
SupportedCoordinateChange.lean 6 declarations
SupportedPhaseMetric.lean 1 declarations
SupportedPhaseOperators.lean 6 declarations
SupportedTensorChart.lean 10 declarations
SupportedWeightedSeminorm.lean 6 declarations
SurfaceChartPairStability.lean 1 declarations
SurfaceChartRepresentative.lean 1 declarations
SurfaceChartTranslationBound.lean 2 declarations
SurfaceCompactCoordinateMap.lean 1 declarations
SurfaceCoordinateTranslation.lean 2 declarations
SurfaceCurveCoordinates.lean 1 declarations
SurfaceJetCoordinates.lean 9 declarations
SurfaceLocalCoordinateMap.lean 1 declarations
SurfacePhaseAmplitude.lean 1 declarations
SurfacePhaseCharts.lean 10 declarations
SurfaceRealPhaseChart.lean 2 declarations
TangentMetricBounds.lean 6 declarations
TargetCoordinateChoice.lean 1 declarations
TensorChartBounds.lean 6 declarations
TensorChartRead.lean 5 declarations
TensorCoordinatePullbackBounds.lean 4 declarations
TensorFiberCoordinates.lean 10 declarations
TensorPhaseDecomposition.lean 6 declarations
TensorPhaseDifferential.lean 5 declarations
TensorPlaneCoordinates.lean 9 declarations
TensorPlaneWeight.lean 5 declarations
TensorReadReconstruction.lean 2 declarations
TensorRootPhases.lean 6 declarations
ThinPairCoordinates.lean 1 declarations
TimeCoordinateBlend.lean 3 declarations
TimeCoordinateTransition.lean 1 declarations
TransverseCompactCurveCharts.lean 5 declarations
TransverseCutoff.lean 6 declarations
TransverseSheetCoordinates.lean 2 declarations
TriangularTimeCoordinates.lean 4 declarations
UniformAtlasConvexPhases.lean 1 declarations
UniformCenteredCharts.lean 2 declarations
UniformCompactPhaseCancellation.lean 1 declarations
UniformCompactPhaseFamily.lean 2 declarations
UniformFiniteAtlasCancellation.lean 1 declarations
UniformLinearPhaseBudgets.lean 4 declarations
UniformMetricPhaseGeometry.lean 3 declarations
UniformNearbyAtlasSmallIncrement.lean 2 declarations
UniformNearbyPhaseCancellation.lean 2 declarations
UniformPhaseChartBounds.lean 1 declarations
UniformPhaseChartSolver.lean 2 declarations
UniformPhaseSolverPrefix.lean 2 declarations
UniformRadiusAtlasIncrement.lean 1 declarations
UnorderedPairChart.lean 1 declarations
VectorChartRead.lean 7 declarations
WeightedActualJets.lean 2 declarations
WeightedAngularJets.lean 8 declarations
WeightedAtlasPhases.lean 5 declarations
WeightedCoefficientVariation.lean 2 declarations
WeightedComplexMixedJets.lean 2 declarations
WeightedInverseJacobian.lean 7 declarations
WeightedInverseSqrt.lean 3 declarations
WeightedLowCoefficients.lean 2 declarations
WeightedMixedJets.lean 1 declarations
WeightedModulatedJets.lean 5 declarations
WeightedMultilinearVariations.lean 3 declarations
WeightedPhaseExpressions.lean 3 declarations
WeightedProjectionLinearization.lean 4 declarations
WeightedRealAlgebra.lean 4 declarations
WeightedReciprocal.lean 2 declarations
ZeroSliceLineChart.lean 2 declarations