`OAI/Geometry/SurfaceImmersion/Primitive/`

1338 declarations, 0 contain sorry, 0 declared as axioms; 354 files

Files

ActualAnalyticProfiledLoop.lean 1 declarations
ActualAnalyticSurfaceLoop.lean 1 declarations
ActualCircularPeriod.lean 1 declarations
ActualCircularProfile.lean 1 declarations
ActualCrossingInvariant.lean 3 declarations
ActualCrossingPath.lean 1 declarations
ActualFiniteCrossingNormal.lean 1 declarations
ActualFixedFrameLoop.lean 1 declarations
ActualProfileCrossing.lean 2 declarations
ActualProfileCurve.lean 1 declarations
ActualProfileCurveCover.lean 1 declarations
ActualProfiledSurfaceLoop.lean 1 declarations
ActualSupportedSurfaceLoop.lean 1 declarations
AdaptedPhasePrimitiveAtlas.lean 1 declarations
AdaptedPrimitiveGeometry.lean 1 declarations
AdmissibleCrossingPath.lean 2 declarations
AnalyticCurveCrossingLoop.lean 1 declarations
AtlasBoundaryProfile.lean 4 declarations
AtlasJetProfiles.lean 1 declarations
AtlasLeadingProfileStability.lean 3 declarations
AtlasPeriodicAnsatz.lean 5 declarations
AtlasPeriodicMetric.lean 2 declarations
AtlasPrimitiveError.lean 1 declarations
AtlasPrimitiveErrorBound.lean 3 declarations
AtlasPrimitiveExpansion.lean 3 declarations
AtlasPrimitiveLocalErrorBound.lean 1 declarations
AtlasPrimitiveMapBound.lean 2 declarations
AtlasPrimitiveNormal.lean 3 declarations
AtlasPrimitiveOperator.lean 13 declarations
AtlasPrimitiveSeedBounds.lean 4 declarations
AtlasPrimitiveUpdate.lean 2 declarations
BlendedNormalizedLoop.lean 1 declarations
BlendedReparamTurns.lean 6 declarations
BlendedSpatialTurns.lean 6 declarations
BlendedVelocityPath.lean 6 declarations
BoundaryJetCrossings.lean 4 declarations
BoundaryProfileCoordinates.lean 6 declarations
BoundaryProfileFrame.lean 4 declarations
BoundaryProfileGeometry.lean 14 declarations
BoundaryProfileNormal.lean 5 declarations
BoundedPrimitiveAmplitude.lean 4 declarations
CalibratedControlledAngle.lean 1 declarations
CalibratedJetAngle.lean 1 declarations
CenteredAtlasPrimitives.lean 3 declarations
CircularActualCrossings.lean 1 declarations
CircularBoundaryMetricStep.lean 1 declarations
CircularBoundaryParam.lean 13 declarations
CircularBoundaryProfiles.lean 4 declarations
CircularBoundaryRemovalStep.lean 1 declarations
CircularBoundaryTangencies.lean 6 declarations
CircularCurveCover.lean 1 declarations
CircularCycleMetrics.lean 3 declarations
CircularDiskTopology.lean 10 declarations
CircularFamilyGeometry.lean 2 declarations
CircularFamilyProfile.lean 4 declarations
CircularFamilyThreshold.lean 2 declarations
CircularFamilyWeights.lean 2 declarations
CircularFlatBump.lean 17 declarations
CircularFrozenCoefficients.lean 1 declarations
CircularJetProfiles.lean 2 declarations
CircularMetricSequence.lean 2 declarations
CircularPatchDefiners.lean 2 declarations
CircularPhaseBoundaryCurve.lean 3 declarations
CircularPhaseDefiningFamily.lean 1 declarations
CircularPhaseDependence.lean 4 declarations
CircularPhaseLocalDefiner.lean 1 declarations
CircularPhaseTolerance.lean 1 declarations
CircularPrefixMetrics.lean 14 declarations
CircularPrimitiveBoundaryStep.lean 1 declarations
CircularPrimitiveFamily.lean 3 declarations
CircularPrimitiveRealization.lean 1 declarations
CircularPrimitiveSupport.lean 1 declarations
CircularProfilePullback.lean 1 declarations
CircularProfileThreshold.lean 1 declarations
CircularRadiusCovectors.lean 3 declarations
CircularSectionProfiles.lean 1 declarations
CircularSupportedPrimitivePatch.lean 1 declarations
ClosedIntervalTurns.lean 1 declarations
CompactCrossingChoice.lean 1 declarations
CompactCrossingNormal.lean 1 declarations
CompactCrossingPreservation.lean 1 declarations
CompactPeriodicAnsatzBounds.lean 3 declarations
CompactPrimitiveSupport.lean 1 declarations
CompactTurnDichotomy.lean 2 declarations
ConstructSupportedPrimitivePatch.lean 1 declarations
ConstructedCircularPrimitive.lean 1 declarations
ConstructedPrimitiveSupport.lean 1 declarations
ConstructedSurfaceLoop.lean 4 declarations
ControlledInteriorLoop.lean 3 declarations
CorrectedCircularFamily.lean 5 declarations
CrossingChoiceScaling.lean 4 declarations
CrossingComponents.lean 12 declarations
CrossingCoordinateMap.lean 7 declarations
CrossingInvariantScaling.lean 5 declarations
CrossingInvariantThreshold.lean 3 declarations
CrossingNeighborhood.lean 1 declarations
CrossingNormalPath.lean 6 declarations
CrossingPlanes.lean 8 declarations
CrossingPositivePairing.lean 4 declarations
CrossingProjectionBounds.lean 7 declarations
CrossingSafeNormalGluing.lean 1 declarations
CrossingTargetLinear.lean 10 declarations
CrossingThreshold.lean 2 declarations
CurvedAtlasPrimitives.lean 17 declarations
ExactCircularBoundary.lean 1 declarations
ExactCircularCurves.lean 1 declarations
ExactCircularPrimitive.lean 1 declarations
ExactOriginalProfiles.lean 1 declarations
ExactPhaseBoundaryProfiles.lean 1 declarations
ExactPhaseOriginalProfiles.lean 1 declarations
ExactPhasePrimitive.lean 1 declarations
ExactPhasePrimitiveProfiles.lean 1 declarations
ExactPrimitiveMetric.lean 1 declarations
ExactPrimitiveProfiles.lean 1 declarations
ExactProfiledPhasePrimitive.lean 1 declarations
ExactProfiledPrimitive.lean 1 declarations
ExplicitPeriodicFormula.lean 3 declarations
ExteriorClosureProfiles.lean 1 declarations
ExteriorProfileBounds.lean 3 declarations
FiniteBoundaryCrossingSets.lean 6 declarations
FiniteCircularPreparation.lean 1 declarations
FiniteCrossingNeighborhoods.lean 1 declarations
FiniteCrossingNormals.lean 1 declarations
FiniteExteriorCrossings.lean 1 declarations
FinitePeriodicExpansion.lean 2 declarations
FinitePrimitiveOperatorTolerance.lean 1 declarations
FiniteProfileBounds.lean 1 declarations
FrozenCircularData.lean 8 declarations
GenericCircularPhases.lean 1 declarations
GenericCircularRadii.lean 1 declarations
GenericPhaseCrossing.lean 4 declarations
GeometricCircularNormal.lean 1 declarations
GeometricControlledVelocity.lean 2 declarations
GeometricJetVelocity.lean 1 declarations
GlobalCircularNormal.lean 1 declarations
GridIncrementProfile.lean 1 declarations
HigherLongitudinalProfiles.lean 2 declarations
IndependentCircularBoundary.lean 1 declarations
IndependentCircularBoundaryStep.lean 1 declarations
IndependentCircularCurves.lean 1 declarations
IndependentCircularRealization.lean 2 declarations
IndependentConstructedCircular.lean 1 declarations
IndependentExactCircular.lean 1 declarations
IndependentExactOriginalProfiles.lean 1 declarations
IndependentExactPhaseProfiles.lean 1 declarations
IndependentExactProfiledPhase.lean 1 declarations
IndependentPhaseBoundaryProfiles.lean 1 declarations
IndependentPreservingCircular.lean 1 declarations
IndependentPrimitiveNormalMargin.lean 1 declarations
IndependentProfiledFastFamily.lean 1 declarations
IndependentProfiledPhase.lean 1 declarations
InteriorVelocityPath.lean 3 declarations
IntrinsicCrossingNaturality.lean 5 declarations
IntrinsicExteriorCrossings.lean 4 declarations
JetLoopPullback.lean 3 declarations
JetVelocityCoordinates.lean 12 declarations
JetVelocityLoop.lean 6 declarations
LeadingProfileIdentification.lean 3 declarations
LeadingProfileMap.lean 6 declarations
LeadingProfileStability.lean 3 declarations
LinearPhaseDerivativeProfiles.lean 5 declarations
LocalAnsatzProfiles.lean 8 declarations
LocalCircularActualCrossings.lean 1 declarations
LocalCircularCurveCover.lean 1 declarations
LocalCircularFamilyThreshold.lean 1 declarations
LocalCrossingAdjustment.lean 1 declarations
LocalCrossingChoice.lean 1 declarations
LocalFinitePeriodicExpansion.lean 2 declarations
LocalIntrinsicCrossing.lean 6 declarations
LocalPeriodicAnsatzMetric.lean 4 declarations
LocalPeriodicCalculus.lean 25 declarations
LocalPeriodicCoefficientSupport.lean 5 declarations
LocalPeriodicExpansionInit.lean 6 declarations
LocalPeriodicExpansionStep.lean 5 declarations
LocalPeriodicFamilies.lean 28 declarations
LocalPeriodicFamilyAlgebra.lean 21 declarations
LocalPeriodicFastEvaluation.lean 4 declarations
LocalPeriodicFiniteAnsatz.lean 3 declarations
LocalPeriodicFiniteMetricIdentity.lean 2 declarations
LocalPeriodicGlobalization.lean 7 declarations
LocalPeriodicMetricCoefficients.lean 13 declarations
LocalPeriodicMetricRemainder.lean 6 declarations
LocalPeriodicPrimitive.lean 1 declarations
LocalPeriodicTriangularRecursion.lean 5 declarations
LocalizedTwistAngle.lean 5 declarations
LongitudinalCoefficientProfile.lean 1 declarations
LongitudinalCrossing.lean 4 declarations
LoopCompactNormalMargin.lean 1 declarations
LoopDensityBumpSelection.lean 5 declarations
LoopDensityCompact.lean 1 declarations
LoopDensityDirections.lean 2 declarations
LoopDensityLinear.lean 14 declarations
LoopDensityMomentConverse.lean 1 declarations
LoopDensityMoments.lean 1 declarations
LoopDensityParameter.lean 7 declarations
LoopDensityPatching.lean 1 declarations
LoopDensityRelative.lean 1 declarations
LoopDensityTriangle.lean 7 declarations
MixedPeriodicBounds.lean 5 declarations
NonlinearJetProfiles.lean 1 declarations
NonlinearPrimitiveExpansion.lean 1 declarations
PeriodicAnsatzMetric.lean 4 declarations
PeriodicBumpAverage.lean 1 declarations
PeriodicCalculus.lean 3 declarations
PeriodicCoefficientProfiles.lean 5 declarations
PeriodicCoefficientSupport.lean 5 declarations
PeriodicExpansionInit.lean 10 declarations
PeriodicExpansionStep.lean 5 declarations
PeriodicFamilies.lean 37 declarations
PeriodicFamilySupport.lean 3 declarations
PeriodicFastEvaluation.lean 3 declarations
PeriodicFiniteAnsatz.lean 3 declarations
PeriodicFiniteMetricIdentity.lean 2 declarations
PeriodicIntegralOperator.lean 11 declarations
PeriodicLocalizedBump.lean 6 declarations
PeriodicMetricCoefficients.lean 15 declarations
PeriodicMetricCoordinates.lean 2 declarations
PeriodicMetricRemainder.lean 6 declarations
PeriodicNormalStability.lean 2 declarations
PeriodicPrimitive.lean 14 declarations
PeriodicSubspace.lean 6 declarations
PeriodicSupport.lean 7 declarations
PeriodicTriangularRecursion.lean 5 declarations
PeriodicVanishing.lean 3 declarations
PerturbedCircularCutoffs.lean 5 declarations
PhaseAnsatzProfiles.lean 2 declarations
PhaseBoundaryProfile.lean 4 declarations
PhaseCircularPeriod.lean 4 declarations
PhaseCrossingTransversality.lean 4 declarations
PhaseCurveCrossings.lean 2 declarations
PhaseLeadingProfileStability.lean 1 declarations
PhasePreparedCrossings.lean 1 declarations
PhasePrimitiveBoundaryGauss.lean 3 declarations
PhasePrimitiveGlobalTensor.lean 2 declarations
PhasePrimitiveMetricRead.lean 1 declarations
PhasePrimitiveNormalRealization.lean 1 declarations
PhasePrimitiveSupport.lean 4 declarations
PhasePrimitiveTensor.lean 3 declarations
PhaseProfileStability.lean 2 declarations
PositiveAtlasPrimitives.lean 13 declarations
PositiveDensityTurns.lean 3 declarations
PreparedAnalyticProfiles.lean 1 declarations
PreparedCircularDefiners.lean 1 declarations
PreparedCircularDirections.lean 2 declarations
PreparedCircularFamilyGeometry.lean 1 declarations
PreparedCircularPhaseCurves.lean 1 declarations
PreparedCircularSurfaceLoop.lean 1 declarations
PreparedFixedFrameLoop.lean 1 declarations
PreparedPhaseCrossingSlopes.lean 2 declarations
PreparedPointCrossings.lean 1 declarations
PreservingCircularNormal.lean 1 declarations
PreservingCircularPrimitive.lean 1 declarations
PrimitiveAmplitudeChain.lean 1 declarations
PrimitiveAmplitudeParameterBounds.lean 10 declarations
PrimitiveAmplitudeZero.lean 1 declarations
PrimitiveAtlasNormalMargin.lean 1 declarations
PrimitiveCoefficientCoordinates.lean 4 declarations
PrimitiveCoordinateData.lean 4 declarations
PrimitiveCoordinateDerivative.lean 2 declarations
PrimitiveCoordinateGerms.lean 2 declarations
PrimitiveCoordinateTolerance.lean 1 declarations
PrimitiveCycleAssembly.lean 8 declarations
PrimitiveCycleBounds.lean 4 declarations
PrimitiveCycleMetrics.lean 15 declarations
PrimitiveDataC1.lean 1 declarations
PrimitiveDomainWindow.lean 6 declarations
PrimitiveFiberInverse.lean 16 declarations
PrimitiveFrameBounds.lean 5 declarations
PrimitiveGeometricApproximation.lean 1 declarations
PrimitiveIncrementBounds.lean 3 declarations
PrimitiveInitialFamily.lean 3 declarations
PrimitiveMetric.lean 7 declarations
PrimitiveMetricPowers.lean 1 declarations
PrimitiveNormalCoordinates.lean 3 declarations
PrimitiveOperatorConjugation.lean 1 declarations
PrimitiveOperatorMask.lean 1 declarations
PrimitiveOperatorStability.lean 7 declarations
PrimitiveOuterGeometry.lean 1 declarations
PrimitivePatchBoundary.lean 3 declarations
PrimitivePatchBoundaryStep.lean 1 declarations
PrimitivePatchCurves.lean 12 declarations
PrimitivePatchDefiners.lean 1 declarations
PrimitivePatchRealization.lean 1 declarations
PrimitiveProfileStability.lean 5 declarations
PrimitiveSeedBounds.lean 2 declarations
PrimitiveShiftedPowers.lean 3 declarations
PrimitiveSlowErrorProfiles.lean 2 declarations
PrimitiveSlowIncrement.lean 9 declarations
PrimitiveSlowScales.lean 14 declarations
PrimitiveTensorRemainder.lean 1 declarations
PrimitiveTermC1Bounds.lean 7 declarations
PrimitiveWeightedBudget.lean 1 declarations
ProfileCrossingChoice.lean 1 declarations
ProfileCrossingPath.lean 1 declarations
ProfiledNearbyAtlasSmallIncrement.lean 1 declarations
ProfiledPhaseFastFamily.lean 2 declarations
ProfiledPhasePrimitive.lean 1 declarations
ProfiledPrimitiveFastFamily.lean 2 declarations
ProfiledSplitCancellation.lean 1 declarations
ProjectedVelocityFrame.lean 7 declarations
PureRadialCrossing.lean 2 declarations
ReferenceCircularAtlas.lean 2 declarations
ReferenceCircularMargins.lean 6 declarations
ReferenceCircularOperator.lean 8 declarations
RegularCurveLoopRemoval.lean 1 declarations
RestrictedSurfaceLoop.lean 3 declarations
SecondCoefficientProfiles.lean 4 declarations
ShrinkingCircularWeight.lean 8 declarations
SlowPeriodicDerivative.lean 8 declarations
SmallTurnFunction.lean 2 declarations
SpatialLoopAmplitude.lean 15 declarations
SupportedCrossingAdjustment.lean 1 declarations
SupportedPrimitiveExpansion.lean 1 declarations
SupportedPrimitiveGeometry.lean 3 declarations
SupportedPrimitivePatch.lean 2 declarations
SurfaceCircularThreshold.lean 3 declarations
SurfaceCrossingExterior.lean 1 declarations
SurfaceCurveCrossingLoop.lean 1 declarations
SurfaceFiniteCurveLoop.lean 1 declarations
SurfacePrimitiveError.lean 4 declarations
SurfaceVelocityFamily.lean 17 declarations
SurfaceVelocityIdentities.lean 9 declarations
TransverseCircularRadii.lean 3 declarations
TwoMechanismCrossing.lean 2 declarations
UniformCircularPhaseCharts.lean 1 declarations
UniformCircularRealization.lean 1 declarations
UniformCircularStartingFamily.lean 1 declarations
UniformConvexCircularAtlas.lean 2 declarations
UniformCrossingBounds.lean 3 declarations
UniformLongitudinalProfile.lean 1 declarations
UniformMixedProfile.lean 1 declarations
UniformPhasePrimitive.lean 1 declarations
UniformPrimitiveGeometricApproximation.lean 1 declarations
UniformPrimitiveNormal.lean 4 declarations
UniformPrimitiveProfiles.lean 2 declarations
UniformPrimitiveRemainder.lean 1 declarations
UniformScaledLongitudinalProfile.lean 4 declarations
UniformTransverseProfiles.lean 1 declarations
VelocityAngleInterpolation.lean 7 declarations
VelocityCircleLift.lean 7 declarations
VelocityCoordinateData.lean 9 declarations
VelocityFrame.lean 21 declarations
VelocityNormalBounds.lean 6 declarations
VelocityNormalEstimates.lean 5 declarations
VelocityNormalGeometry.lean 11 declarations
VelocityNormalNonvanishing.lean 5 declarations
VelocityPlane.lean 12 declarations
VelocityPlaneBasis.lean 5 declarations
VelocityPlaneCoordinates.lean 4 declarations
VelocityPlaneRays.lean 4 declarations
VelocitySpatialBounds.lean 4 declarations
VelocitySpatialDerivative.lean 4 declarations
VelocityTurnDominance.lean 1 declarations
WeightedPeriodicPrimitive.lean 3 declarations