`OAI/Geometry/RCD/Coordinates/`

1287 declarations, 0 contain sorry, 0 declared as axioms; 510 files

Files

ACCoordinateEndpointEnergy.lean 1 declarations
ACFrameEndpointPairing.lean 1 declarations
ACFrameEnergyPairing.lean 2 declarations
ActualCovectorFit.lean 1 declarations
ActualDyadicFitStep.lean 1 declarations
ActualDyadicFitUnits.lean 1 declarations
ActualFitCommutator.lean 1 declarations
ActualRadialCovector.lean 1 declarations
ActualRegularFlatness.lean 3 declarations
AdjacentMeanComparison.lean 1 declarations
AffineFitDifference.lean 2 declarations
AffineFitPerturbation.lean 4 declarations
AffineFitRecurrence.lean 5 declarations
AffineFitSmoothing.lean 2 declarations
AllScaleCoordinateDistance.lean 3 declarations
AnnularSquareLimit.lean 1 declarations
BilinearDiagonalBound.lean 2 declarations
BilinearHeatEnvelope.lean 3 declarations
BilinearIntervalAverage.lean 1 declarations
BochnerFrameCompletion.lean 5 declarations
BochnerFrameDefect.lean 1 declarations
BoundedFrameBarrier.lean 1 declarations
BoundedHeatLogRegular.lean 1 declarations
BoundedLocalCoordinates.lean 7 declarations
BoundedRegularBochnerMass.lean 1 declarations
BoundedRegularGramEnergy.lean 1 declarations
BoundedRegularLocalization.lean 1 declarations
BoundedRegularMixedHessianDensity.lean 1 declarations
BoundedRegularNormalization.lean 1 declarations
BoundedRegularPrescribedHessian.lean 1 declarations
BoundedSourceIntegral.lean 2 declarations
BoundedSplittingCoordinates.lean 3 declarations
CanonicalCenteredFits.lean 1 declarations
CanonicalCoordinateHeatInput.lean 1 declarations
CenteredBoundedFrame.lean 2 declarations
CenteredCoordinateNorm.lean 2 declarations
CenteredFirstOrderFrame.lean 1 declarations
CenteredFrameGramBound.lean 1 declarations
CenteredNormalization.lean 3 declarations
CenteredSplitting.lean 9 declarations
ChartTopology.lean 3 declarations
CoarseFineCoordinateDistance.lean 2 declarations
CommonFrameRadialFits.lean 4 declarations
CompactFactorRegularity.lean 1 declarations
CompactHeatGaugeNormalization.lean 2 declarations
CompactHeatOsmoticRegular.lean 1 declarations
CompactRadialPullback.lean 1 declarations
ComparableRadiusNormalization.lean 2 declarations
ComparableRadiusSplitting.lean 2 declarations
ConditionalMain.lean 8 declarations
ControlledNormalization.lean 2 declarations
CoordinateBilinear.lean 3 declarations
CoordinateEllipsoids.lean 5 declarations
CoordinateHeatInput.lean 4 declarations
CoordinateImageMass.lean 1 declarations
CoordinatePathVelocity.lean 2 declarations
CoordinateTargetNorm.lean 2 declarations
CovectorCoefficientRecovery.lean 1 declarations
CovectorCommutator.lean 1 declarations
CovectorConstantRecovery.lean 2 declarations
CovectorRadialSmallness.lean 2 declarations
CurvedHeatRegularSource.lean 1 declarations
CurvedRegularShiftedHessian.lean 1 declarations
DiagonalMeanSelection.lean 1 declarations
DifferentialBounds.lean 6 declarations
DifferentialStep.lean 7 declarations
DyadicCenterDecay.lean 1 declarations
DyadicCovectorGrowth.lean 1 declarations
DyadicFitVolumeUnits.lean 2 declarations
DyadicMeanControl.lean 4 declarations
DyadicNormalizedError.lean 3 declarations
DyadicNormalizedFamily.lean 1 declarations
DyadicNormalizedGradient.lean 1 declarations
DyadicNormalizedLipschitz.lean 1 declarations
DyadicRadialFit.lean 2 declarations
DyadicRadialFitEstimates.lean 6 declarations
DyadicRadialFits.lean 5 declarations
DyadicRootEventualSplitting.lean 1 declarations
DyadicTransformationReduction.lean 2 declarations
EuclideanAffineTaylor.lean 4 declarations
EuclideanCoordinateBound.lean 1 declarations
EuclideanCoordinateTests.lean 3 declarations
EuclideanCovectorIsometry.lean 1 declarations
EuclideanDensityNormalization.lean 1 declarations
EuclideanGevreyCutoff.lean 3 declarations
EuclideanWeakHarmonicRegularity.lean 5 declarations
ExactNormalizationComparison.lean 2 declarations
FactorialMajorant.lean 12 declarations
FieldEstimates.lean 4 declarations
FiniteBilinearAE.lean 3 declarations
FiniteDepthNormalization.lean 2 declarations
FiniteNormalizerGrowth.lean 3 declarations
FirstFailingDyadicScale.lean 1 declarations
FirstFailingRootFrame.lean 2 declarations
FirstFailingSequence.lean 1 declarations
FirstOrderCoordinateDistance.lean 1 declarations
FirstOrderFrameConvergence.lean 1 declarations
FirstOrderFrameErrorIntegral.lean 1 declarations
FirstOrderHeatFrameEnergy.lean 1 declarations
FirstOrderInnerCoordinates.lean 1 declarations
FirstOrderRegularFamily.lean 1 declarations
FiveGeometricInputs.lean 1 declarations
FixedGaugeHeatRegular.lean 1 declarations
FixedGaugeRegularGradient.lean 1 declarations
FixedResidualNormalization.lean 4 declarations
FlatSplittingApproximation.lean 2 declarations
FourGeometricInputs.lean 1 declarations
FrameCoefficientBound.lean 2 declarations
FrameCoefficientExcess.lean 3 declarations
FrameEnergyError.lean 3 declarations
FramePathEndpointEnergy.lean 2 declarations
FramePathNormalizedEndpoint.lean 1 declarations
FrameResidualDefect.lean 2 declarations
FrameResidualEnergy.lean 2 declarations
FrameTestPlanVelocityDefect.lean 1 declarations
FrameVelocityDefect.lean 2 declarations
FrameVelocityError.lean 3 declarations
FrameVelocityErrorLimit.lean 1 declarations
FrameVelocityErrorLocality.lean 2 declarations
FramedAffineProjection.lean 2 declarations
FramedDyadicFit.lean 1 declarations
FramedPointValues.lean 2 declarations
FramedRadialCandidate.lean 1 declarations
FramedRadialEnergy.lean 2 declarations
FramedRadialSmallness.lean 1 declarations
FramedRadialValue.lean 2 declarations
FrozenCutoffDerivatives.lean 2 declarations
FrozenInverseCosts.lean 4 declarations
FrozenJetTransport.lean 11 declarations
FrozenNorms.lean 14 declarations
FullScaleCoordinateDistance.lean 3 declarations
FullSplittingCoordinates.lean 1 declarations
GammaCoordinateForm.lean 4 declarations
GeometricInputCoordinates.lean 1 declarations
GevreyCompactBump.lean 5 declarations
GevreyConvolution.lean 1 declarations
GevreyCutoffConstruction.lean 1 declarations
GevreyExpGlue.lean 8 declarations
GlobalFrameDefect.lean 2 declarations
GoodSplittingSet.lean 1 declarations
GramNormalization.lean 6 declarations
HalfRestrictedMean.lean 7 declarations
HarmonicCoordinateGram.lean 1 declarations
HarmonicCoordinatePair.lean 1 declarations
HarmonicCoordinateValueLimit.lean 2 declarations
HarmonicFitStep.lean 1 declarations
HarmonicFrameApproximation.lean 1 declarations
HarmonicGlobalFrameDefect.lean 1 declarations
HausdorffLowerNormalization.lean 1 declarations
HausdorffMeasureRegularity.lean 1 declarations
HausdorffUpperNormalization.lean 1 declarations
HeatFrameGramBound.lean 1 declarations
HeatFrameUniformEnergy.lean 1 declarations
HeatHamiltonRegularized.lean 2 declarations
HeatHarmonicFrameGram.lean 1 declarations
HeatLiYauParameterRegularized.lean 1 declarations
HeatLiYauRegularized.lean 1 declarations
HeatNormalizationVolume.lean 2 declarations
HeatRegularSourceGram.lean 1 declarations
HeatRegularizedEntropy.lean 3 declarations
HessianCoordinateForm.lean 4 declarations
InitialAnalyticBounds.lean 3 declarations
InitialHarmonicCoordinates.lean 1 declarations
InitialSplittingConstruction.lean 1 declarations
InitialSplittingSequence.lean 1 declarations
InnerCoordinateSequence.lean 1 declarations
IntervalBilinearEnergy.lean 4 declarations
IntervalVectorExtension.lean 4 declarations
InverseDerivative.lean 14 declarations
InverseJetBounds.lean 20 declarations
InverseMajorant.lean 9 declarations
InverseMetricFrames.lean 6 declarations
IterationLimit.lean 13 declarations
IterationOpenness.lean 2 declarations
JetStep.lean 6 declarations
KernelBridgeNormalization.lean 2 declarations
KernelHeatBoundedRegularity.lean 1 declarations
LaplacianCoordinateForm.lean 4 declarations
LimitChart.lean 3 declarations
LinearNormalization.lean 2 declarations
LinearRadialFits.lean 7 declarations
LocalConstantRepresentative.lean 1 declarations
LocalCoordinateExtension.lean 2 declarations
LocalCoordinateImageMass.lean 2 declarations
LocalFramePathVelocity.lean 1 declarations
LocalHarmonicFrameDefect.lean 1 declarations
LocalPoissonRegularExtension.lean 1 declarations
LocalPositiveBilinearMeasure.lean 1 declarations
LongBoundedSource.lean 1 declarations
MatrixNormConversion.lean 5 declarations
MatrixTransverseDefect.lean 2 declarations
MeasuredCoordinateInput.lean 1 declarations
MeasuredCoordinates.lean 2 declarations
MeasuredRescalingFromCoordinates.lean 1 declarations
MetricDyadicNormalization.lean 2 declarations
MetricIteration.lean 17 declarations
MetricLimitHausdorffNormalization.lean 1 declarations
NearRegularDistanceSources.lean 1 declarations
NearRegularPoissonFamily.lean 1 declarations
NearbyExactFrames.lean 1 declarations
NearbyNormalizedPlan.lean 1 declarations
NonlinearIteration.lean 2 declarations
NormalizationComposition.lean 4 declarations
NormalizationCumulative.lean 4 declarations
NormalizationRebase.lean 6 declarations
NormalizedBochnerMass.lean 2 declarations
NormalizedCoordinateFrames.lean 4 declarations
NormalizedCutoffDifference.lean 1 declarations
NormalizedDensityLaw.lean 4 declarations
NormalizedDirectionError.lean 4 declarations
NormalizedDirichletError.lean 2 declarations
NormalizedDistancePoisson.lean 1 declarations
NormalizedDistanceSourceLimit.lean 1 declarations
NormalizedExponentialTilt.lean 1 declarations
NormalizedFitEnergy.lean 1 declarations
NormalizedFrameDerivative.lean 1 declarations
NormalizedFrameEndpoint.lean 1 declarations
NormalizedFrameRadialSmallness.lean 3 declarations
NormalizedHarmonicHeatMass.lean 1 declarations
NormalizedHarmonicLinearLimit.lean 2 declarations
NormalizedHausdorffImage.lean 2 declarations
NormalizedHeatEntropy.lean 4 declarations
NormalizedHeatMassLimit.lean 1 declarations
NormalizedHeatMeanLimit.lean 2 declarations
NormalizedJetStep.lean 8 declarations
NormalizedL1FromL2.lean 1 declarations
NormalizedL2LimitBound.lean 2 declarations
NormalizedL2ProductError.lean 1 declarations
NormalizedL2SobolevMoment.lean 1 declarations
NormalizedLawCompression.lean 2 declarations
NormalizedLevelAlgebra.lean 3 declarations
NormalizedLocalEnergy.lean 1 declarations
NormalizedLocalL1Domination.lean 1 declarations
NormalizedLocalL2.lean 4 declarations
NormalizedMeanDirectionError.lean 1 declarations
NormalizedOptimalSubplan.lean 1 declarations
NormalizedOuterDirectionError.lean 1 declarations
NormalizedPairing.lean 4 declarations
NormalizedPlanLocalMass.lean 1 declarations
NormalizedPlanMeanEnergy.lean 1 declarations
NormalizedPoissonCommutator.lean 2 declarations
NormalizedPoissonEstimates.lean 1 declarations
NormalizedPoissonEulerGradient.lean 2 declarations
NormalizedPositiveWeights.lean 2 declarations
NormalizedProbabilityLaw.lean 4 declarations
NormalizedProductError.lean 1 declarations
NormalizedProjectionConfiguration.lean 1 declarations
NormalizedProjectionResidual.lean 2 declarations
NormalizedQuotientError.lean 1 declarations
NormalizedRadialCandidate.lean 1 declarations
NormalizedRadialError.lean 4 declarations
NormalizedRecoveryRadialSwap.lean 1 declarations
NormalizedResidualOuter.lean 2 declarations
NormalizedSobolevMoment.lean 1 declarations
NormalizedSourceGradient.lean 2 declarations
NormalizedSubplanData.lean 1 declarations
NormalizedSubplanNodes.lean 1 declarations
NormalizedSupportedCompression.lean 1 declarations
NormalizedTiltLpVariation.lean 6 declarations
NormalizedTorsion.lean 2 declarations
NormalizedTransportDefect.lean 1 declarations
NormalizedUniformL2.lean 1 declarations
NormalizedUniformMean.lean 1 declarations
NormalizedUpdate.lean 6 declarations
OpenCoordinates.lean 16 declarations
OpenLimitChart.lean 1 declarations
OpenRegularCutoff.lean 1 declarations
OuterNormalizedSquareLimit.lean 2 declarations
OutwardCovectorGrowth.lean 1 declarations
OverlappingExactFrames.lean 2 declarations
PairGeometry.lean 3 declarations
PatchAssembly.lean 21 declarations
PatchBudget.lean 1 declarations
PatchCenters.lean 4 declarations
PatchCover.lean 14 declarations
PatchCoverData.lean 22 declarations
PatchDirectionalBounds.lean 14 declarations
PatchGeometryMonotone.lean 1 declarations
PatchJetBounds.lean 16 declarations
PatchLocalization.lean 8 declarations
PatchSecondDerivative.lean 6 declarations
PointwiseMetricIteration.lean 6 declarations
PoissonBilinearMeasure.lean 1 declarations
PoissonSpanCoordinates.lean 5 declarations
PositiveBilinearIntegralLower.lean 1 declarations
PositiveBilinearMeasure.lean 17 declarations
PositiveForms.lean 4 declarations
ProjectionAffineNormalization.lean 1 declarations
ProjectionCoordinateValues.lean 1 declarations
ProjectionMeasuredCoordinates.lean 3 declarations
Proper.lean 3 declarations
PullbackDensityLaws.lean 5 declarations
QuadraticCoordinateGradient.lean 4 declarations
QuadraticMetricError.lean 3 declarations
RadialCoefficientMatrix.lean 3 declarations
RadialFitCoordinates.lean 12 declarations
RadialFitEnvelope.lean 2 declarations
RadialFitFromCorrection.lean 1 declarations
RadialFitRecurrence.lean 1 declarations
RadialFitRestriction.lean 2 declarations
RadialFitSmallness.lean 1 declarations
RadialFrameChange.lean 1 declarations
RadialFrameLocalization.lean 1 declarations
RadialMatrixEstimates.lean 1 declarations
RebasedRadialFits.lean 4 declarations
RegularActualImageGoodSets.lean 1 declarations
RegularActualImageMass.lean 1 declarations
RegularActualPatches.lean 9 declarations
RegularBilinearData.lean 3 declarations
RegularBochnerDirectional.lean 1 declarations
RegularBochnerForm.lean 2 declarations
RegularBochnerFrame.lean 1 declarations
RegularBochnerFrameDefect.lean 1 declarations
RegularBochnerLocalSource.lean 1 declarations
RegularBochnerMeasure.lean 3 declarations
RegularBochnerMeasureLaplacian.lean 1 declarations
RegularBochnerPositivity.lean 1 declarations
RegularBochnerShiftedDirectional.lean 1 declarations
RegularBochnerSquare.lean 2 declarations
RegularBochnerSquareFamily.lean 1 declarations
RegularBochnerSquarePair.lean 1 declarations
RegularBochnerWeakDirectional.lean 1 declarations
RegularBochnerWeakSquare.lean 1 declarations
RegularBoundedCoarseFineSets.lean 1 declarations
RegularCenterRadialData.lean 2 declarations
RegularCompactCutoff.lean 8 declarations
RegularControlledNormalization.lean 1 declarations
RegularCoreBochner.lean 2 declarations
RegularCoreFrameDefect.lean 1 declarations
RegularCoreGradientProduct.lean 1 declarations
RegularCoreHessianBound.lean 1 declarations
RegularCoreMixedFullBall.lean 1 declarations
RegularCoreMixedHessian.lean 1 declarations
RegularCoreRepresentative.lean 1 declarations
RegularCoreShiftedHessian.lean 1 declarations
RegularCoreShiftedMeasure.lean 1 declarations
RegularCoreWeakHessian.lean 1 declarations
RegularCoreWeakMeasure.lean 1 declarations
RegularCutoffDerivatives.lean 1 declarations
RegularCutoffJets.lean 2 declarations
RegularDirichletCore.lean 4 declarations
RegularDistanceReplacements.lean 1 declarations
RegularDistanceSources.lean 1 declarations
RegularDyadicData.lean 2 declarations
RegularEllipsoids.lean 3 declarations
RegularEuclideanHausdorff.lean 2 declarations
RegularFinitePatchCover.lean 2 declarations
RegularFiniteSpan.lean 1 declarations
RegularFrameDefect.lean 1 declarations
RegularFrameGeometry.lean 7 declarations
RegularFrozenMass.lean 2 declarations
RegularFrozenMetrics.lean 8 declarations
RegularGoodCoordinateSets.lean 1 declarations
RegularGoodCoordinateSetsBounded.lean 1 declarations
RegularGoodSplittingSets.lean 1 declarations
RegularGramEnergy.lean 1 declarations
RegularHeatCutoff.lean 1 declarations
RegularHeatFrameGeometry.lean 4 declarations
RegularHeatNormalization.lean 4 declarations
RegularHessianCore.lean 1 declarations
RegularImageGoodSets.lean 1 declarations
RegularImageMassEstimate.lean 2 declarations
RegularInitialChart.lean 2 declarations
RegularInnerGoodCoordinates.lean 1 declarations
RegularIterationPairs.lean 1 declarations
RegularLargeGoodSets.lean 1 declarations
RegularLimitBallBounds.lean 1 declarations
RegularLimitBallMass.lean 1 declarations
RegularLimitChart.lean 1 declarations
RegularLimitEuclideanNeighborhood.lean 1 declarations
RegularLimitFiniteEuclidean.lean 1 declarations
RegularLimitInnerProductBall.lean 1 declarations
RegularLimitMidpointFamily.lean 1 declarations
RegularLimitMidpointGeometry.lean 1 declarations
RegularLimitQuadraticMidpoint.lean 1 declarations
RegularLinearRadialData.lean 1 declarations
RegularMassMatrices.lean 6 declarations
RegularMassScale.lean 2 declarations
RegularMassSmallness.lean 2 declarations
RegularMeanPinching.lean 2 declarations
RegularMeanPinchingNeighborhood.lean 1 declarations
RegularMetricLimitMeasure.lean 1 declarations
RegularMovingVolume.lean 2 declarations
RegularMovingVolumeRatio.lean 1 declarations
RegularNearbyFrozen.lean 2 declarations
RegularNearbyMidpoints.lean 1 declarations
RegularNeighborhoodBilinear.lean 4 declarations
RegularNeighborhoodHeat.lean 1 declarations
RegularNetGeometry.lean 4 declarations
RegularNetSeparation.lean 3 declarations
RegularOpenCoordinates.lean 5 declarations
RegularPairBochner.lean 1 declarations
RegularPairCommutator.lean 2 declarations
RegularPairCoordinates.lean 2 declarations
RegularPairDirection.lean 3 declarations
RegularPairEndpoints.lean 2 declarations
RegularPairFrames.lean 1 declarations
RegularPairGradient.lean 1 declarations
RegularPairMass.lean 1 declarations
RegularPairPinching.lean 1 declarations
RegularPairProjection.lean 1 declarations
RegularPairingChoiceBound.lean 1 declarations
RegularPairingShiftedBound.lean 1 declarations
RegularPatchCenters.lean 2 declarations
RegularPatchCumulative.lean 2 declarations
RegularPatchHeatComparison.lean 2 declarations
RegularPatchIteration.lean 2 declarations
RegularPatchMassEnvelope.lean 3 declarations
RegularPatchMassSum.lean 3 declarations
RegularPatchSelection.lean 2 declarations
RegularPinchingField.lean 2 declarations
RegularPinchingFrame.lean 2 declarations
RegularPinchingSmallness.lean 2 declarations
RegularPointedFlatness.lean 4 declarations
RegularPointedMidpoint.lean 1 declarations
RegularProjectionConfiguration.lean 1 declarations
RegularProjectionEnvironment.lean 3 declarations
RegularProjectionRows.lean 3 declarations
RegularQuadraticMidpoints.lean 1 declarations
RegularQuadraticTransportPaths.lean 1 declarations
RegularRadialEnvironment.lean 1 declarations
RegularRawMassSmallness.lean 2 declarations
RegularRebasedRadialData.lean 1 declarations
RegularSelectedMass.lean 4 declarations
RegularSharpNeighborhood.lean 1 declarations
RegularSharpProjection.lean 1 declarations
RegularSharpSources.lean 1 declarations
RegularShiftedCentralMass.lean 1 declarations
RegularShiftedNormalization.lean 1 declarations
RegularShiftedNormalizationSum.lean 3 declarations
RegularSquareLaplacian.lean 2 declarations
RegularSquareSourceData.lean 1 declarations
RegularTangents.lean 6 declarations
RegularTestAlgebra.lean 1 declarations
RegularTripleHessian.lean 1 declarations
RegularUniformDirection.lean 1 declarations
RegularVolumeConvergence.lean 1 declarations
RegularVolumeNonpositive.lean 1 declarations
RegularWorkingChart.lean 5 declarations
RegularizedEntropyFirstVariation.lean 1 declarations
RegularizedEntropySecant.lean 1 declarations
RegularizedFisherContinuity.lean 1 declarations
RegularizedFisherInterpolation.lean 2 declarations
RegularizedGram.lean 8 declarations
RegularizedHamiltonIntegrability.lean 2 declarations
RegularizedMonotoneHeat.lean 5 declarations
RelativeErrorNormalization.lean 3 declarations
RenyiChordNormalization.lean 1 declarations
RenyiNormalizedComparison.lean 1 declarations
RenyiScalarNormalization.lean 1 declarations
RestrictedCommutatorFit.lean 1 declarations
ScalarBochnerCoordinates.lean 1 declarations
ScaledChartPinching.lean 1 declarations
ScaledCoordinates.lean 5 declarations
ScaledPatchCumulative.lean 1 declarations
ScaledPatchIteration.lean 1 declarations
ScaledRegularBilinear.lean 1 declarations
ScaledRegularData.lean 3 declarations
ScaledRegularizer.lean 1 declarations
ScaledSelectedCumulative.lean 1 declarations
ScaledSeparatedSources.lean 3 declarations
ScaledSharpNeighborhood.lean 1 declarations
ScalingDualPotential.lean 1 declarations
ScalingNormalizationLimit.lean 1 declarations
SevenGeometricInputs.lean 1 declarations
ShiftedLogarithmJets.lean 1 declarations
ShiftedLogarithmRegularData.lean 1 declarations
SixGeometricInputs.lean 1 declarations
SobolevFramePathEnergy.lean 4 declarations
SobolevFramePlanVariation.lean 1 declarations
SplittingApproximation.lean 6 declarations
SplittingCoordinateLipschitz.lean 1 declarations
SymmetricDomination.lean 2 declarations
TaylorControl.lean 5 declarations
ThreeGeometricInputs.lean 1 declarations
TimeAverageLinearMap.lean 3 declarations
TimeIntervalAverage.lean 5 declarations
Transformation.lean 1 declarations
TransformationInput.lean 2 declarations
TransverseCoordinateDefect.lean 1 declarations
TransverseCoordinateEnergy.lean 1 declarations
TransverseFrameData.lean 1 declarations
TwoCenterCommutatorFit.lean 3 declarations
TwoCenterRadialFits.lean 4 declarations
TwoFrozenPairingVariation.lean 1 declarations
TwoGeometricInputs.lean 1 declarations
UniformCenteredFits.lean 1 declarations
UniformControlledNormalization.lean 2 declarations
UniformNormalizedInnerTests.lean 1 declarations
UniformPlanPullback.lean 1 declarations
UniformPolarizedError.lean 3 declarations
UniformProductConvergence.lean 1 declarations
UniformRegularDistanceReplacements.lean 1 declarations
UniformRegularFlatnessInput.lean 1 declarations
UniformRegularPoissonDefect.lean 1 declarations
UniformTransformation.lean 1 declarations
UnitCoordinateDirections.lean 3 declarations
ValueLimitNormalization.lean 1 declarations
VanishingDiagonalCost.lean 1 declarations
VanishingRadiusCost.lean 1 declarations
VolumeProfileRegularity.lean 5 declarations
VolumeRegularity.lean 1 declarations
VolumeRigidityMain.lean 1 declarations
WeightedBilinearMeasure.lean 14 declarations
WeightedConvolution.lean 9 declarations
WeightedFitSmoothing.lean 2 declarations
WeightedFramedProjection.lean 2 declarations
WeightedInverse.lean 11 declarations
WeightedSquaredFitCenters.lean 1 declarations
WorkingNormalizerBound.lean 2 declarations