`OAI/Geometry/SurfaceImmersion/Correction/`

1850 declarations, 0 contain sorry, 0 declared as axioms; 489 files

Files

ActualSmoothedStep.lean 2 declarations
AdaptedSmoothingAtlas.lean 2 declarations
AdaptiveCorrectionSequence.lean 12 declarations
AdaptiveCorrectionStep.lean 8 declarations
AdaptiveExactControl.lean 1 declarations
AdaptiveExactCorrection.lean 3 declarations
AdaptiveOrderControl.lean 3 declarations
AnchoredPreparedCorrection.lean 1 declarations
AnchoredSmoothedIncrement.lean 1 declarations
ArbitraryPhasePolynomial.lean 3 declarations
AssembledCombinedMean.lean 2 declarations
AssembledZeroMean.lean 7 declarations
AtlasCombinedModes.lean 4 declarations
AtlasCorrectionAssembly.lean 1 declarations
AtlasCorrectionBudget.lean 5 declarations
AtlasCorrectionLimit.lean 3 declarations
AtlasFreeMetricSplit.lean 2 declarations
AtlasFreeOscillation.lean 3 declarations
AtlasFreeQuadraticCorrection.lean 1 declarations
AtlasFreeResidual.lean 1 declarations
AtlasGlobalFreeModes.lean 6 declarations
AtlasGlobalPolynomialMean.lean 1 declarations
AtlasLinearizedMetric.lean 4 declarations
AtlasMetricLocalModel.lean 3 declarations
AtlasModeGerms.lean 2 declarations
AtlasModePolynomialQuadratic.lean 1 declarations
AtlasModeQuadraticExpansion.lean 1 declarations
AtlasPhaseMeanDomains.lean 2 declarations
AtlasPolynomialAmplitudeBounds.lean 1 declarations
AtlasPolynomialCalculus.lean 3 declarations
AtlasPolynomialCancellation.lean 1 declarations
AtlasPolynomialCoordinateRead.lean 1 declarations
AtlasPolynomialFreeResidual.lean 1 declarations
AtlasPolynomialFreeSplit.lean 2 declarations
AtlasPolynomialIncrementBound.lean 1 declarations
AtlasPolynomialInputCancellation.lean 1 declarations
AtlasPolynomialInteractionBounds.lean 2 declarations
AtlasPolynomialLinearity.lean 4 declarations
AtlasPolynomialLinearized.lean 3 declarations
AtlasPolynomialLocalModel.lean 3 declarations
AtlasPolynomialMetric.lean 13 declarations
AtlasPolynomialModeMean.lean 3 declarations
AtlasPolynomialNearbyCancellation.lean 1 declarations
AtlasPolynomialNonlinearProfiles.lean 1 declarations
AtlasPolynomialOverlap.lean 2 declarations
AtlasPolynomialOverlapCancellation.lean 1 declarations
AtlasPolynomialQuadraticBounds.lean 1 declarations
AtlasPolynomialRemainderBounds.lean 1 declarations
AtlasPolynomialRepresentation.lean 2 declarations
AtlasPolynomialRestoredRead.lean 1 declarations
AtlasPolynomialSmooth.lean 3 declarations
AtlasPolynomialSupport.lean 2 declarations
AtlasPolynomialTargetProfiles.lean 1 declarations
AtlasPolynomialValueBounds.lean 3 declarations
AtlasPolynomialVariationRepresentation.lean 3 declarations
AtlasPrimitiveMean.lean 9 declarations
AtlasPrimitivePolynomial.lean 4 declarations
AtlasRestoredPolynomialDirection.lean 2 declarations
AtlasRestoredPolynomialRepresentation.lean 2 declarations
AtlasSupportedPolynomialQuadratic.lean 4 declarations
AtlasSupportedPolynomialVariation.lean 2 declarations
BoundedSurfaceCorrection.lean 8 declarations
BundleSmoothing.lean 8 declarations
BundleSmoothingIdentity.lean 4 declarations
BundleSmoothingLinearity.lean 6 declarations
BundleSmoothingTransition.lean 4 declarations
C1ManifoldSmoothing.lean 6 declarations
CatalogGlobalQuadraticCorrection.lean 1 declarations
CenteredPairModels.lean 9 declarations
CenteredSmoothStep.lean 9 declarations
ChartResidualBounds.lean 2 declarations
ChartedAdjustedMean.lean 3 declarations
ChartedAtlasMeanIdentity.lean 1 declarations
ChartedAtlasQuadraticResidual.lean 3 declarations
ChartedCombinedMean.lean 6 declarations
ChartedCombinedMeanBounds.lean 1 declarations
ChartedFiniteMean.lean 2 declarations
ChartedForcedMode.lean 1 declarations
ChartedFreeDisplacement.lean 5 declarations
ChartedFreeFamily.lean 5 declarations
ChartedFreeMetricSplit.lean 2 declarations
ChartedFreeResidual.lean 7 declarations
ChartedFreeSeed.lean 9 declarations
ChartedMeanData.lean 7 declarations
ChartedMeanFamily.lean 3 declarations
ChartedMeanFamilyData.lean 6 declarations
ChartedMeanProfile.lean 2 declarations
ChartedMetricMean.lean 5 declarations
ChartedMetricMeanDifference.lean 1 declarations
ChartedPolynomialMean.lean 1 declarations
ChartedTrialMean.lean 2 declarations
ChartedUniformCombinedMean.lean 1 declarations
ChartedUniformFiniteMean.lean 2 declarations
ChartedUniformFree.lean 3 declarations
ChartedUniformPolynomialMean.lean 1 declarations
ChartedUniformTrialMean.lean 1 declarations
ChartedZeroMean.lean 6 declarations
CircularSmoothingAtlas.lean 16 declarations
CombinedMeanChart.lean 7 declarations
CombinedMeanGeometry.lean 4 declarations
CombinedMeanMajorants.lean 1 declarations
CombinedMeanTensor.lean 2 declarations
CombinedRootMean.lean 1 declarations
CombinedSeedMean.lean 3 declarations
CombinedZeroMean.lean 4 declarations
CompactChartedMeanData.lean 1 declarations
CompactGeometryPolynomialIncrement.lean 1 declarations
CompactMeanBudgets.lean 3 declarations
CompactModeCoefficients.lean 1 declarations
CompactPolynomialSolver.lean 1 declarations
CompactSmoothCutoffs.lean 6 declarations
CompactSurfaceSmoothExtension.lean 1 declarations
CompactTransverseCorrection.lean 1 declarations
ComplexifiedPolynomialOperator.lean 4 declarations
ConjugatedPolynomialOperator.lean 8 declarations
CoordinateLinearizedCalculus.lean 3 declarations
CoordinateLinearizedResidual.lean 2 declarations
CoordinateLinearizedSupport.lean 3 declarations
CoordinateModelGerm.lean 2 declarations
CoordinatePolynomialCalculus.lean 2 declarations
CoordinatePolynomialPullback.lean 7 declarations
CoordinatePolynomialRealization.lean 2 declarations
CoordinateSurfaceModels.lean 4 declarations
CorrectedPolynomialMean.lean 1 declarations
CorrectedPolynomialRootMean.lean 1 declarations
CorrectionBudgetThresholds.lean 1 declarations
CorrectionErrorEnvelope.lean 1 declarations
CorrectionGeometry.lean 3 declarations
CorrectionMetricBounds.lean 3 declarations
CorrectionMetricIdentity.lean 6 declarations
CorrectionScaleAlgebra.lean 9 declarations
CorrectionScaleControl.lean 6 declarations
CorrectionScales.lean 5 declarations
CoupledSmoothing.lean 2 declarations
CovarianceCorrector.lean 30 declarations
CrossAtlasPolynomialRead.lean 1 declarations
CrossAtlasPolynomialRepresentation.lean 1 declarations
CrossAtlasPolynomialTransfer.lean 1 declarations
CrossAtlasRestoredPolynomial.lean 1 declarations
CrossAtlasRestoredPolynomialRead.lean 1 declarations
CutoffTensorPolynomial.lean 3 declarations
DiagonalDefectModel.lean 6 declarations
ExactCorrectionConvergence.lean 2 declarations
ExactCorrectionLimit.lean 8 declarations
ExactCorrectionRecurrence.lean 5 declarations
ExplicitCorrectionBudgetThreshold.lean 2 declarations
ExplicitGlobalQuadraticCorrection.lean 1 declarations
ExtendedCombinedMean.lean 4 declarations
FinishSmoothTail.lean 1 declarations
FiniteAdjustedMean.lean 1 declarations
FiniteAtlasFreeMetric.lean 6 declarations
FiniteAtlasFreeRestore.lean 1 declarations
FiniteCombinedMean.lean 1 declarations
FiniteCorrectionGerms.lean 3 declarations
FiniteMeanFamily.lean 1 declarations
FiniteMeanSums.lean 3 declarations
FiniteMeanThreshold.lean 2 declarations
FiniteMetricPolynomial.lean 7 declarations
FiniteOrderSmoother.lean 5 declarations
FinitePolynomialCancellation.lean 1 declarations
FinitePolynomialPhases.lean 3 declarations
FiniteSmootherApproximation.lean 5 declarations
FiniteSmootherBounds.lean 5 declarations
FiniteSmootherLinearity.lean 4 declarations
FiniteSmootherWeighted.lean 4 declarations
FiniteSpecialPointCorrection.lean 1 declarations
FiniteSurfaceCorrection.lean 5 declarations
FiniteSurfaceCorrectionBounds.lean 1 declarations
FixedBallProfiledAtlasMean.lean 1 declarations
FixedMeanSubstitution.lean 6 declarations
FreeForcedIncrementIdentity.lean 2 declarations
FreeForcedSegment.lean 3 declarations
FullPeriodicCorrector.lean 1 declarations
GeometricAtlasAdjustedMean.lean 1 declarations
GlobalBundleSmoothing.lean 2 declarations
GlobalChartedForcedMode.lean 1 declarations
GlobalModeDifferential.lean 7 declarations
GlobalOscillatoryModes.lean 9 declarations
GlobalQuadraticModes.lean 3 declarations
GlobalShiftedSmoothing.lean 5 declarations
GlobalSmoothedMetricStep.lean 1 declarations
GlobalSmoothingBounds.lean 2 declarations
GoodSmoothingAtlas.lean 5 declarations
GridFreeCorrection.lean 1 declarations
GridFreeMeanIdentity.lean 2 declarations
GridFreeSupport.lean 2 declarations
GridGlobalQuadraticCorrection.lean 1 declarations
GridMeanBudgets.lean 3 declarations
GridMeanData.lean 1 declarations
GridMeanReconstruction.lean 2 declarations
HigherJetPolynomial.lean 1 declarations
IndependentAtlasMean.lean 1 declarations
IndependentPhaseMean.lean 1 declarations
InitialCorrectionStage.lean 3 declarations
InitialLocalCorrection.lean 1 declarations
InitialSmoothTail.lean 2 declarations
InputAtlasFreeQuadraticCorrection.lean 2 declarations
InputPolynomialFreeCorrection.lean 1 declarations
InputPolynomialQuadraticCancellation.lean 1 declarations
InputPolynomialSmallIncrement.lean 1 declarations
JetPolynomialAlgebra.lean 16 declarations
JetPolynomialCovariance.lean 6 declarations
JetPolynomialDerivative.lean 16 declarations
JetPolynomialEvaluation.lean 5 declarations
JetPolynomialFullCorrector.lean 13 declarations
JetPolynomialFullEvaluation.lean 1 declarations
JetPolynomialIntegral.lean 18 declarations
JetPolynomialLinear.lean 5 declarations
JetPolynomialLocality.lean 2 declarations
JetPolynomialOperations.lean 15 declarations
JetPolynomialScalar.lean 15 declarations
JetPolynomialVariation.lean 3 declarations
JetPolynomialVector.lean 21 declarations
LinearChartedMeanData.lean 1 declarations
LinearMeanBudgetsFromBounds.lean 1 declarations
LinearMeanReconstruction.lean 3 declarations
LinearPhaseMeanGeometry.lean 2 declarations
LocalCombinedMean.lean 5 declarations
LocalCombinedMeanBounds.lean 1 declarations
LocalFullPeriodicCorrector.lean 4 declarations
LocalPeriodicCorrector.lean 3 declarations
LocalPeriodicPolynomialExpansion.lean 12 declarations
LocalPerturbedMean.lean 2 declarations
ManifoldCorrectionLimit.lean 5 declarations
ManifoldFreeIncrement.lean 7 declarations
ManifoldSmoothing.lean 9 declarations
ManifoldSmoothingLinearity.lean 6 declarations
MetricGoodSmoothingAtlas.lean 1 declarations
MetricPolynomialIncrement.lean 1 declarations
MetricPolynomialSlowStep.lean 1 declarations
MixedJetPolynomial.lean 13 declarations
MixedPeriodicMean.lean 9 declarations
MixedPolynomialLocality.lean 2 declarations
ModulatedPolynomialJets.lean 10 declarations
NormalizedJetCorrection.lean 6 declarations
NormalizedLinearModel.lean 9 declarations
NormalizedPerturbedMean.lean 3 declarations
NormalizedPolynomialMean.lean 3 declarations
NormalizedPolynomialSupport.lean 4 declarations
OrderwiseCorrectionLimit.lean 5 declarations
PairCurveSmoothParameter.lean 1 declarations
PairModelCoordinates.lean 10 declarations
PeriodicCorrector.lean 7 declarations
PeriodicCorrectorFormula.lean 2 declarations
PeriodicCorrectorSystem.lean 2 declarations
PeriodicPolynomialExpansion.lean 12 declarations
PerturbationTaylorBounds.lean 4 declarations
PerturbedFreeMode.lean 2 declarations
PerturbedFreeModeBounds.lean 1 declarations
PerturbedFreeModeSize.lean 1 declarations
PerturbedFreeOrderBounds.lean 2 declarations
PerturbedFreeUniformBounds.lean 1 declarations
PerturbedMeanBounds.lean 1 declarations
PerturbedMeanDifference.lean 1 declarations
PerturbedMeanTransfer.lean 5 declarations
PerturbedRootMean.lean 1 declarations
PhaseMeanDomains.lean 3 declarations
PhasePrimitiveMeanRealization.lean 1 declarations
PolynomialAdvance.lean 1 declarations
PolynomialAffineDerivative.lean 3 declarations
PolynomialAffineFamily.lean 4 declarations
PolynomialAmplitudeBounds.lean 2 declarations
PolynomialAtlasFree.lean 1 declarations
PolynomialAtlasFreeProfile.lean 1 declarations
PolynomialAtlasMean.lean 1 declarations
PolynomialAtlasSeed.lean 1 declarations
PolynomialAtlasSeedProfile.lean 1 declarations
PolynomialBudgetAlgebra.lean 5 declarations
PolynomialBudgetMeanFamily.lean 3 declarations
PolynomialCancellation.lean 1 declarations
PolynomialChartedFree.lean 1 declarations
PolynomialChartedFreeFamily.lean 1 declarations
PolynomialChartedMeanFamily.lean 1 declarations
PolynomialChartedMetricMean.lean 2 declarations
PolynomialChartedSeed.lean 1 declarations
PolynomialCoefficientExtension.lean 4 declarations
PolynomialCoefficientRecursion.lean 1 declarations
PolynomialConnectionBounds.lean 4 declarations
PolynomialCorrectionBudget.lean 2 declarations
PolynomialCorrectorRepresentation.lean 1 declarations
PolynomialCorrectorSystem.lean 1 declarations
PolynomialCubicRemainder.lean 1 declarations
PolynomialDiagonalVariations.lean 9 declarations
PolynomialDualBounds.lean 4 declarations
PolynomialFiniteAssembly.lean 10 declarations
PolynomialFiniteAtlasMean.lean 1 declarations
PolynomialFiniteAtlasTrial.lean 1 declarations
PolynomialFiniteMeanFamily.lean 3 declarations
PolynomialFixedCancellation.lean 1 declarations
PolynomialFixedOrderThreshold.lean 3 declarations
PolynomialForcedBounds.lean 1 declarations
PolynomialForcedCancellation.lean 1 declarations
PolynomialForcingRepresentation.lean 3 declarations
PolynomialFrameEnvelope.lean 2 declarations
PolynomialFreeModes.lean 1 declarations
PolynomialFreeNormal.lean 4 declarations
PolynomialGeometry.lean 8 declarations
PolynomialInitialCorrection.lean 1 declarations
PolynomialInputNorm.lean 1 declarations
PolynomialInteractionBounds.lean 4 declarations
PolynomialInverseChartJets.lean 5 declarations
PolynomialJetRecursion.lean 7 declarations
PolynomialJetSmoothness.lean 5 declarations
PolynomialLinearMeanBudgets.lean 3 declarations
PolynomialLinearMeanData.lean 1 declarations
PolynomialLinearModes.lean 5 declarations
PolynomialLinearSolver.lean 1 declarations
PolynomialLocalAmplitude.lean 4 declarations
PolynomialLocalMean.lean 2 declarations
PolynomialLocalMeanProfile.lean 2 declarations
PolynomialMeanApproximation.lean 3 declarations
PolynomialMeanCoefficient.lean 6 declarations
PolynomialMeanDifference.lean 3 declarations
PolynomialMeanError.lean 2 declarations
PolynomialMeanIteration.lean 7 declarations
PolynomialMeanPair.lean 6 declarations
PolynomialMeanPairBounds.lean 2 declarations
PolynomialMeanSupport.lean 7 declarations
PolynomialMeanThreshold.lean 1 declarations
PolynomialMeanTransport.lean 4 declarations
PolynomialMetricBounds.lean 1 declarations
PolynomialMetricCoefficients.lean 15 declarations
PolynomialMetricForcedBudgets.lean 6 declarations
PolynomialMetricForcing.lean 11 declarations
PolynomialMetricFreeBudgets.lean 6 declarations
PolynomialMetricRemainder.lean 12 declarations
PolynomialModeBudgets.lean 9 declarations
PolynomialModeConstruction.lean 7 declarations
PolynomialModeResidual.lean 3 declarations
PolynomialNonlinearPhaseFrame.lean 1 declarations
PolynomialNonlinearScales.lean 3 declarations
PolynomialNonlinearSolver.lean 1 declarations
PolynomialNormalBounds.lean 11 declarations
PolynomialPerpBounds.lean 7 declarations
PolynomialPerturbationBounds.lean 5 declarations
PolynomialPerturbationCalculus.lean 7 declarations
PolynomialPerturbationOperator.lean 3 declarations
PolynomialPhaseBounds.lean 1 declarations
PolynomialPhaseChartInverse.lean 2 declarations
PolynomialPhaseFrame.lean 3 declarations
PolynomialPhaseSupport.lean 5 declarations
PolynomialPowerThreshold.lean 1 declarations
PolynomialPreparedInitialization.lean 1 declarations
PolynomialProfileTransfer.lean 10 declarations
PolynomialProfiledSplitCancellation.lean 1 declarations
PolynomialQuadraticCancellation.lean 1 declarations
PolynomialQuadraticFamily.lean 6 declarations
PolynomialQuadraticFamilyBounds.lean 1 declarations
PolynomialQuadraticPhases.lean 10 declarations
PolynomialQuadraticTargetBudget.lean 3 declarations
PolynomialQuadraticTargets.lean 5 declarations
PolynomialQuadraticTensorBounds.lean 1 declarations
PolynomialQuadrature.lean 6 declarations
PolynomialReadProfiles.lean 1 declarations
PolynomialRealReconstruction.lean 4 declarations
PolynomialReconstruction.lean 1 declarations
PolynomialRootBounds.lean 6 declarations
PolynomialRotationFrame.lean 11 declarations
PolynomialScaleSelection.lean 2 declarations
PolynomialSlowFamily.lean 3 declarations
PolynomialSmoothingProfiles.lean 1 declarations
PolynomialSolveData.lean 6 declarations
PolynomialSolveFactors.lean 10 declarations
PolynomialSplitBudgets.lean 4 declarations
PolynomialSupportedMeanData.lean 2 declarations
PolynomialSupportedModeBudgets.lean 4 declarations
PolynomialTaylorBounds.lean 1 declarations
PolynomialTaylorRemainder.lean 5 declarations
PolynomialTensorMean.lean 1 declarations
PolynomialTensorReadBudget.lean 1 declarations
PolynomialTrialAmplitude.lean 1 declarations
PolynomialUnitPerpBounds.lean 1 declarations
PolynomialValueBounds.lean 2 declarations
PolynomialVariationBounds.lean 6 declarations
PolynomialVariationDerivatives.lean 3 declarations
PolynomialVariationScaling.lean 7 declarations
PolynomialZeroPhaseExpansion.lean 7 declarations
PositivePolynomialBounds.lean 9 declarations
PositiveSmoothingAtlas.lean 13 declarations
PreparedCorrection.lean 5 declarations
PrescribedTransverseModel.lean 6 declarations
PrimitiveInitialMean.lean 6 declarations
PrimitiveMeanRealization.lean 1 declarations
PrimitiveMeanStep.lean 10 declarations
ProfiledAtlasAdjustedMean.lean 1 declarations
ProfiledPolynomialSmallIncrement.lean 1 declarations
QuadratureMean.lean 4 declarations
RealPolynomialQuadraticBounds.lean 4 declarations
RealPolynomialVariationBounds.lean 2 declarations
RestoredLinearizedMetric.lean 2 declarations
RestoredPolynomialModeMean.lean 2 declarations
RestoredQuadratureMean.lean 1 declarations
ShiftedSmoothingBounds.lean 6 declarations
SmoothCircularRadius.lean 5 declarations
SmoothCoverCutoff.lean 1 declarations
SmoothMetricGauss.lean 3 declarations
SmoothOrderedPrefix.lean 1 declarations
SmoothParameterIntegral.lean 6 declarations
SmoothPathRegularInterior.lean 1 declarations
SmoothPeriodicCalculus.lean 19 declarations
SmoothPeriodicCorrector.lean 2 declarations
SmoothPeriodicPrimitive.lean 4 declarations
SmoothPhaseChart.lean 2 declarations
SmoothPrimitiveFamily.lean 19 declarations
SmoothSpanSolve.lean 2 declarations
SmoothTransitionDerivativeBound.lean 1 declarations
SmoothZeroFactor.lean 5 declarations
SmoothedInputAdmissibility.lean 1 declarations
SmoothedInputCloseness.lean 1 declarations
SmoothedMetricIncrement.lean 2 declarations
SmoothedMetricStep.lean 8 declarations
SmoothedMetricStepBounds.lean 1 declarations
SmoothingAtlas.lean 6 declarations
SmoothingC1Approximation.lean 3 declarations
SmoothingConvolution.lean 11 declarations
SmoothingDerivativeBounds.lean 2 declarations
SmoothingDerivatives.lean 1 declarations
SmoothingFirstMoment.lean 4 declarations
SmoothingGain.lean 3 declarations
SmoothingKernel.lean 11 declarations
SmoothingLinearMaps.lean 3 declarations
SmoothingLocalSections.lean 1 declarations
SmoothingLocalization.lean 7 declarations
SmoothingMetricCrossBounds.lean 2 declarations
SmoothingMoments.lean 7 declarations
SmoothingNormBounds.lean 3 declarations
SmoothingResidual.lean 5 declarations
SmoothingResidualBounds.lean 2 declarations
SmoothingResidualOperator.lean 2 declarations
SmoothingTailBounds.lean 5 declarations
SmoothingTransition.lean 10 declarations
SpecialPointCorrection.lean 8 declarations
SupportedFreeLinearity.lean 3 declarations
SupportedInitialMode.lean 6 declarations
SupportedMeanError.lean 5 declarations
SupportedModeBounds.lean 2 declarations
SupportedModeOperators.lean 8 declarations
SupportedPolynomialMean.lean 3 declarations
SupportedPolynomialMeanDifference.lean 2 declarations
SupportedPolynomialOperator.lean 3 declarations
SurfaceCircularSmooth.lean 1 declarations
SurfaceMeanPolynomial.lean 10 declarations
SurfaceMeanTensor.lean 6 declarations
TensorAtlasFiniteMean.lean 1 declarations
TensorAtlasMean.lean 13 declarations
TensorAtlasMeanExplicit.lean 1 declarations
TensorFiniteMean.lean 2 declarations
TensorMeanCoordinates.lean 17 declarations
TensorMeanIteration.lean 11 declarations
TensorOperatorSmooth.lean 9 declarations
TensorSmoothing.lean 10 declarations
TensorSmoothingSymmetry.lean 7 declarations
TensorSymmetricMean.lean 1 declarations
UniformAtlasAdjustedMean.lean 1 declarations
UniformAtlasFiniteMean.lean 1 declarations
UniformAtlasMean.lean 3 declarations
UniformAtlasPhaseMeanData.lean 2 declarations
UniformFiniteMean.lean 2 declarations
UniformFreeModeConstants.lean 4 declarations
UniformGeometricAtlasMean.lean 1 declarations
UniformGeometricMeanData.lean 3 declarations
UniformGeometricMeanFamily.lean 1 declarations
UniformInputAtlasMeanData.lean 2 declarations
UniformLinearChartedMeanData.lean 3 declarations
UniformLinearChartedMeanFamily.lean 4 declarations
UniformLinearPerturbedMeanData.lean 2 declarations
UniformLinearPerturbedMeanFamily.lean 1 declarations
UniformLinearPolynomialSolver.lean 1 declarations
UniformMetricMean.lean 3 declarations
UniformMetricMeanDifference.lean 1 declarations
UniformNormalizedMean.lean 4 declarations
UniformPerturbedMean.lean 1 declarations
UniformPolynomialAtlasMeanData.lean 2 declarations
UniformPolynomialCompactFamily.lean 1 declarations
UniformPolynomialNearbyCancellation.lean 1 declarations
UniformPolynomialPhasePrefix.lean 1 declarations
UniformPolynomialPhaseSolver.lean 1 declarations
UniformPolynomialSmallIncrement.lean 1 declarations
UniformPrimitiveMeanRealization.lean 3 declarations
UniformRadiusSmoothedMetricIncrement.lean 2 declarations
UniformRealModeCoefficients.lean 7 declarations
UniformRootMean.lean 1 declarations
UniformSmoothingInputProfiles.lean 1 declarations
UnperturbedFreeModeIdentity.lean 6 declarations
UnperturbedMeanDataFromBounds.lean 1 declarations
UnperturbedMeanIdentity.lean 1 declarations
WeightedJetExpressions.lean 2 declarations
WeightedPolynomialBounds.lean 6 declarations
WeightedPolynomialVariation.lean 4 declarations