`OAI/Geometry/RCD/Harmonic/`

741 declarations, 0 contain sorry, 0 declared as axioms; 351 files

Files

ACAffinePairing.lean 1 declarations
ActualGramEnvelope.lean 1 declarations
ActualProjectionConfiguration.lean 9 declarations
ActualProjectionOuter.lean 1 declarations
ActualProjectionThreshold.lean 2 declarations
ActualProjectionUnits.lean 3 declarations
ActualRadialError.lean 1 declarations
ActualRadialHarmonic.lean 1 declarations
ActualRadialPairing.lean 1 declarations
ActualSharpProjection.lean 3 declarations
ActualTwoCenterProjection.lean 1 declarations
AffineCenterBounds.lean 4 declarations
AffineChange.lean 3 declarations
AffineCommutatorIdentity.lean 2 declarations
AffineCommutatorResidual.lean 2 declarations
AffineCompactness.lean 5 declarations
AffineConstantBound.lean 1 declarations
AffineEvaluation.lean 2 declarations
AffineForcingBound.lean 1 declarations
AffineGrowthOnInterval.lean 1 declarations
AffineImprovementTransfer.lean 1 declarations
AffineMomentConvergence.lean 1 declarations
AffineOperatorBound.lean 1 declarations
AffinePathDerivative.lean 1 declarations
AffinePathMeans.lean 1 declarations
AffineProjection.lean 16 declarations
AffineScaleChoice.lean 1 declarations
AffineSpatialSelection.lean 1 declarations
AffineValuePairings.lean 7 declarations
AffineVariationSelection.lean 2 declarations
AnnularHarmonicReplacement.lean 1 declarations
AverageHarmonicSource.lean 2 declarations
AverageQuadraticError.lean 1 declarations
AveragedEndpointPairing.lean 1 declarations
AveragedLpPairing.lean 7 declarations
BalancedQuadraticError.lean 2 declarations
BoundedGramTraceDefect.lean 2 declarations
BoundedHarmonicCompactness.lean 1 declarations
BoundedHarmonicNorm.lean 1 declarations
BoundedHarmonicRecoveryStrong.lean 1 declarations
BoundedHarmonicStrongRecovery.lean 1 declarations
BoundedHarmonicValueLimit.lean 1 declarations
BoundedScalarProduct.lean 4 declarations
BoundedTransverseFormula.lean 1 declarations
BoundedTransversePotentials.lean 1 declarations
CaccioppoliSourceMass.lean 1 declarations
CanonicalAffineCenter.lean 1 declarations
CanonicalAffineDifference.lean 1 declarations
CanonicalDyadicCenters.lean 1 declarations
CanonicalRadialSize.lean 2 declarations
CappedPairingL2.lean 1 declarations
CenteredAffineDifference.lean 2 declarations
CenteredBoundedGram.lean 1 declarations
CenteredColumns.lean 5 declarations
CenteredCompactDirection.lean 1 declarations
CenteredFirstOrderMetricCompactness.lean 1 declarations
CenteredHamiltonJacobiPairing.lean 1 declarations
CenteredHarmonicCompactness.lean 1 declarations
CenteredHarmonicDirection.lean 2 declarations
CenteredProjectionRows.lean 3 declarations
ColumnRepresentatives.lean 2 declarations
CommutatorRepresentatives.lean 1 declarations
CompactDifferencePairing.lean 1 declarations
CompactHarmonicTransfer.lean 1 declarations
CompactMixedTransfer.lean 2 declarations
CompactRadialPairingIdentity.lean 1 declarations
CompactRadialWeight.lean 1 declarations
CompactRecoveryCoefficient.lean 1 declarations
CompressedRadialTime.lean 3 declarations
ConstantDirectionError.lean 2 declarations
ContinuousAffineImprovement.lean 2 declarations
ContinuousApproximateRepresentative.lean 1 declarations
ContinuousHamiltonJacobiComparison.lean 1 declarations
ContinuousRadialMoment.lean 1 declarations
ControlledCoefficientPathSelection.lean 1 declarations
CurvatureHarmonicLimit.lean 1 declarations
CurvatureHarmonicVariation.lean 1 declarations
DefectSegment.lean 1 declarations
DirectionRecoveryScale.lean 4 declarations
DirectionSmallness.lean 1 declarations
DirectionalToGramError.lean 1 declarations
DistanceQuadraticPathLimit.lean 1 declarations
DualSegmentEnvelope.lean 1 declarations
DyadicAffineCoefficient.lean 1 declarations
DyadicCenteredRadial.lean 2 declarations
DyadicDistanceReplacements.lean 3 declarations
DyadicRadialCoefficient.lean 1 declarations
DyadicRadialMatrices.lean 1 declarations
DyadicRadialSummability.lean 1 declarations
DyadicRadialTargets.lean 3 declarations
DyadicRootDirectionConvergence.lean 1 declarations
DyadicRootDirectionData.lean 1 declarations
DyadicRootGramConvergence.lean 1 declarations
DyadicRootHarmonicLimit.lean 1 declarations
DyadicRootLinearLimit.lean 1 declarations
EuclideanAffineImprovement.lean 1 declarations
EuclideanHarmonicCompactExtension.lean 4 declarations
EuclideanHarmonicContraction.lean 1 declarations
EuclideanHarmonicL1.lean 1 declarations
EuclideanHarmonicModel.lean 8 declarations
EuclideanHarmonicSquare.lean 2 declarations
EuclideanHarmonicWideExtension.lean 1 declarations
EuclideanQuadraticDefect.lean 6 declarations
EuclideanRadialAverageDerivative.lean 1 declarations
EuclideanRadialGreen.lean 2 declarations
EuclideanRadialMean.lean 2 declarations
EuclideanRadialWeight.lean 13 declarations
EventualQuadraticError.lean 2 declarations
ExactAnnularContraction.lean 2 declarations
ExpandingHarmonicCompactness.lean 1 declarations
ExpandingHarmonicLimit.lean 1 declarations
FiniteGramIsometricLimit.lean 1 declarations
FiniteHarmonicLimits.lean 2 declarations
FiniteHarmonicSubsequence.lean 2 declarations
FiniteMeasuredHarmonicSequence.lean 1 declarations
FirstOrderAbsoluteAffineMean.lean 1 declarations
FirstOrderAffineMean.lean 1 declarations
FirstOrderBarrierMass.lean 1 declarations
FirstOrderCoefficientPaths.lean 1 declarations
FirstOrderColumnEndpoint.lean 1 declarations
FirstOrderCompactRepresentative.lean 1 declarations
FirstOrderDistanceDefect.lean 1 declarations
FirstOrderEuclideanLimit.lean 1 declarations
FirstOrderFromConvergingGrams.lean 1 declarations
FirstOrderFromScaledFamily.lean 1 declarations
FirstOrderGramDefectLimit.lean 1 declarations
FirstOrderInteriorRestriction.lean 1 declarations
FirstOrderIsometricCompactness.lean 1 declarations
FirstOrderLimitNoSupport.lean 1 declarations
FirstOrderLocalization.lean 3 declarations
FirstOrderMetricBounds.lean 1 declarations
FirstOrderMetricCompactness.lean 1 declarations
FirstOrderMetricLimit.lean 1 declarations
FirstOrderMetricLimitIsometry.lean 1 declarations
FirstOrderMovingNoSupport.lean 1 declarations
FirstOrderNoSupport.lean 1 declarations
FirstOrderPathVelocity.lean 1 declarations
FirstOrderSmallScaleApproximation.lean 1 declarations
FirstOrderSubsequenceApproximation.lean 1 declarations
FirstOrderSupportThreshold.lean 1 declarations
FirstOrderTransverseBarrier.lean 1 declarations
FirstOrderUniformAffineMean.lean 1 declarations
FirstOrderVelocityErrorLimit.lean 1 declarations
ForcingCoefficient.lean 2 declarations
FullMassPinching.lean 3 declarations
GeometricProjectionOuter.lean 1 declarations
GramDefect.lean 5 declarations
GramDefectLocality.lean 1 declarations
GramDirectionalError.lean 5 declarations
GramL1Continuity.lean 3 declarations
GramProductMeasure.lean 1 declarations
GramQuadraticDefect.lean 2 declarations
GramSourceEstimate.lean 2 declarations
GramTraceDefect.lean 4 declarations
HarmonicAffineImprovement.lean 5 declarations
HarmonicAffineNondegeneracy.lean 1 declarations
HarmonicAffineSequence.lean 4 declarations
HarmonicBoundaryIdentification.lean 1 declarations
HarmonicBoundaryLayer.lean 1 declarations
HarmonicBoundaryUniqueness.lean 1 declarations
HarmonicContinuousRepresentative.lean 1 declarations
HarmonicCorrection.lean 1 declarations
HarmonicCountableCompactness.lean 1 declarations
HarmonicCurvatureBounds.lean 1 declarations
HarmonicEndpointBound.lean 1 declarations
HarmonicGramSourceComparison.lean 1 declarations
HarmonicGrams.lean 22 declarations
HarmonicInteriorMean.lean 2 declarations
HarmonicInteriorRepresentative.lean 1 declarations
HarmonicLayerMassBound.lean 1 declarations
HarmonicLevelDecay.lean 1 declarations
HarmonicLevelMoment.lean 1 declarations
HarmonicLevelStep.lean 1 declarations
HarmonicLinearRecovery.lean 1 declarations
HarmonicLinearSharp.lean 1 declarations
HarmonicLinearWeightedDefect.lean 1 declarations
HarmonicMeanConstruction.lean 3 declarations
HarmonicMeanValueInput.lean 2 declarations
HarmonicModelCompactness.lean 1 declarations
HarmonicMomentCompactnessInput.lean 1 declarations
HarmonicMomentConstruction.lean 1 declarations
HarmonicOpenBallCompactness.lean 1 declarations
HarmonicOpenBallL2Compactness.lean 2 declarations
HarmonicOperatorEvolution.lean 2 declarations
HarmonicQuadraticPotential.lean 5 declarations
HarmonicRadialBound.lean 1 declarations
HarmonicRecoveryStrong.lean 2 declarations
HarmonicReplacementFamily.lean 1 declarations
HarmonicSmallNorm.lean 1 declarations
HarmonicSourceIntegral.lean 5 declarations
HarmonicStrongRecovery.lean 1 declarations
HarmonicUnitMean.lean 1 declarations
HarmonicValueAffineCompactness.lean 1 declarations
HoleDefectCharge.lean 1 declarations
HomogeneousAffineImprovement.lean 5 declarations
InnerHarmonicLimit.lean 1 declarations
InnerHarmonicNormBound.lean 1 declarations
IntegrableRadialTail.lean 1 declarations
IntegratedPolarization.lean 2 declarations
IntegratedRadialDensity.lean 1 declarations
InteriorQuadraticComparison.lean 2 declarations
InteriorQuadraticDefect.lean 4 declarations
InwardConstantEstimate.lean 1 declarations
L1LocalLimitPairing.lean 2 declarations
L2ProbabilityPairing.lean 2 declarations
LocalAffineMoments.lean 6 declarations
LocalCaccioppoli.lean 2 declarations
LocalConstantHarmonic.lean 2 declarations
LocalL2Restriction.lean 8 declarations
LocalProjectionMeasure.lean 2 declarations
LocalRadialDerivative.lean 5 declarations
LocalRadialSmallness.lean 2 declarations
LocalResidualOuterBound.lean 1 declarations
LocalUniformDifference.lean 1 declarations
LocalVelocityIdentification.lean 3 declarations
LogCosQuadratic.lean 6 declarations
LogCoshQuadratic.lean 6 declarations
MeanDirectionFromPairings.lean 1 declarations
MeanGramControl.lean 6 declarations
MeanGramInverse.lean 5 declarations
MeasuredRadialL2.lean 1 declarations
MetricQuadraticError.lean 2 declarations
MixedGramL1.lean 2 declarations
NearColumnDistance.lean 1 declarations
NearColumnNorm.lean 1 declarations
NearbyGramColumn.lean 1 declarations
NearbyMeanGrams.lean 3 declarations
NeighborhoodGramEnvelope.lean 3 declarations
NonlinearPairingVariation.lean 2 declarations
OperatorQuadraticDerivative.lean 15 declarations
PathAffineResidual.lean 5 declarations
PinchingEnvelope.lean 15 declarations
PinchingFromProjection.lean 2 declarations
PinchingPairingRestriction.lean 2 declarations
PinchingTail.lean 1 declarations
PointedAffineLimitApproximation.lean 1 declarations
PointedAffineValueLimit.lean 1 declarations
PointedRadialDistance.lean 2 declarations
ProbabilityDensityPairing.lean 1 declarations
ProductProjection.lean 1 declarations
ProductProjectionSmallFactor.lean 2 declarations
ProjectionFailureSequence.lean 2 declarations
ProjectionLimitContradiction.lean 1 declarations
ProjectionRadialRows.lean 2 declarations
ProjectionResidualValues.lean 2 declarations
QuadraticDistanceFeature.lean 7 declarations
QuadraticErrorL1Limit.lean 1 declarations
QuadraticGramError.lean 2 declarations
QuadraticInteriorError.lean 2 declarations
QuadraticMeanScaling.lean 6 declarations
QuadraticModelValues.lean 4 declarations
QuadraticRadialError.lean 2 declarations
QuadraticRadialGrowth.lean 1 declarations
QuadraticRateOptimization.lean 1 declarations
QuadraticSegmentCost.lean 1 declarations
QuadraticUniformBounds.lean 3 declarations
QuantitativeAffineMean.lean 5 declarations
QuantitativeQuadraticMean.lean 2 declarations
RadialAverageTimeDerivative.lean 1 declarations
RadialBallComparison.lean 2 declarations
RadialCompactnessSequence.lean 2 declarations
RadialContinuousL2Time.lean 1 declarations
RadialContractionFactor.lean 10 declarations
RadialContractionMoments.lean 1 declarations
RadialDensityEnvelope.lean 1 declarations
RadialDerivativeError.lean 4 declarations
RadialDerivativeNorms.lean 2 declarations
RadialDyadicBudget.lean 7 declarations
RadialErrorUnits.lean 3 declarations
RadialFirstVariation.lean 1 declarations
RadialHarmonicApproximation.lean 2 declarations
RadialLinearCoefficient.lean 1 declarations
RadialLinearCombination.lean 4 declarations
RadialLinearRepresentatives.lean 2 declarations
RadialMixedLimit.lean 1 declarations
RadialMixedRecoveryLimit.lean 1 declarations
RadialMomentBound.lean 1 declarations
RadialPairingSize.lean 1 declarations
RadialQuadraticL2Limit.lean 3 declarations
RadialQuadraticLimit.lean 3 declarations
RadialSquaredDistance.lean 2 declarations
RadialTime.lean 1 declarations
RadialTimeAverageRepresentative.lean 1 declarations
RadialTimeCapacity.lean 3 declarations
RadialTimeReplacement.lean 1 declarations
RadialTimeSupport.lean 4 declarations
RadialValueVolume.lean 1 declarations
RadialVariationBound.lean 1 declarations
RadialVolumeProfile.lean 3 declarations
RadialVolumeUnits.lean 6 declarations
RecoveryHarmonicSwap.lean 1 declarations
ReplaceHarmonicSequence.lean 1 declarations
RescaledRadialFunction.lean 5 declarations
ResidualCollapse.lean 1 declarations
ResidualOuterBound.lean 2 declarations
ResidualSamplingError.lean 4 declarations
ScaledAffineMeanLimit.lean 1 declarations
ScaledForcingCoefficient.lean 3 declarations
ScaledGramEnvelope.lean 1 declarations
ScaledHarmonicAffine.lean 1 declarations
ScaledHarmonicMass.lean 1 declarations
ScaledHarmonicValueConvergence.lean 1 declarations
ScaledMeanPinching.lean 1 declarations
ScaledNeighborhoodGram.lean 3 declarations
ScaledPinchingField.lean 1 declarations
ScaledProjectionData.lean 5 declarations
ScaledProjectionEnvironment.lean 1 declarations
ScaledProjectionOuter.lean 1 declarations
ScaledRadialEnvironment.lean 1 declarations
SharpProjectionFamily.lean 2 declarations
SignedRadialWeight.lean 4 declarations
SmallRadialVolume.lean 1 declarations
SmoothHarmonicModelCompactness.lean 1 declarations
SpaceTimeLocalSlope.lean 1 declarations
SubtypeL2PairingLimit.lean 1 declarations
SupportedCoefficientL2Error.lean 1 declarations
TimeAveragePairing.lean 1 declarations
TimeQuadraticRate.lean 3 declarations
TransformedColumns.lean 4 declarations
TransverseBarrierLocalization.lean 1 declarations
TransverseBarrierLower.lean 2 declarations
TransverseIntegralBound.lean 1 declarations
TransversePositivePart.lean 1 declarations
TwoCenterAffineRecovery.lean 1 declarations
TwoCenterCommutator.lean 3 declarations
TwoCenterDirectionEstimate.lean 1 declarations
TwoCenterProjectionBudget.lean 3 declarations
UnboundedCaccioppoli.lean 3 declarations
UniformCanonicalCenters.lean 1 declarations
UniformCenteredRadial.lean 1 declarations
UniformLocalDifferencePairing.lean 1 declarations
UniformLocalL1Pairing.lean 1 declarations
UniformRadialCoefficient.lean 1 declarations
UniformRadialMatrices.lean 1 declarations
UniformRadialSummability.lean 1 declarations
UniformResidualOuterBound.lean 1 declarations
UniformSharpProjection.lean 1 declarations
UpperLevelCaccioppoli.lean 2 declarations
VanishingScalarDefect.lean 1 declarations
VanishingVariationAffineLimit.lean 4 declarations
WeightedAffineComposition.lean 4 declarations
WeightedAffinePotential.lean 1 declarations
WeightedCoreConvergence.lean 1 declarations
WeightedDirectionalBound.lean 2 declarations
WeightedDirectionalVanishing.lean 1 declarations
WeightedInwardConstants.lean 1 declarations
WeightedMixedError.lean 2 declarations
WeightedQuadraticGluing.lean 1 declarations
WeightedRadialRigidity.lean 3 declarations
WeightedUnitDefect.lean 1 declarations
YoungPairingLimit.lean 2 declarations