`OAI/Geometry/RCD/Metric/`

674 declarations, 0 contain sorry, 0 declared as axioms; 333 files

Files

ActualImageMassDensity.lean 1 declarations
AlmostEuclideanSourceBudget.lean 2 declarations
AnnularDerivativeComparison.lean 1 declarations
AnnularVolume.lean 2 declarations
AnnularVolumeRatio.lean 1 declarations
ApproximatePacking.lean 1 declarations
ApproximationRestriction.lean 1 declarations
AverageMassEnvelope.lean 2 declarations
AverageMassInitial.lean 1 declarations
AverageMassTime.lean 4 declarations
AveragedDensityFubini.lean 1 declarations
BallAverageBad.lean 3 declarations
BallL2Exhaustion.lean 1 declarations
BallLimitGluing.lean 1 declarations
BallMassFubini.lean 1 declarations
BoundaryExteriorBall.lean 1 declarations
BoundedCompactApproximation.lean 1 declarations
BoundedContinuousL2Approximation.lean 1 declarations
BoundedDensityLp.lean 1 declarations
BoundedFiniteDensity.lean 1 declarations
BoundedIsodiametric.lean 3 declarations
BoundedPositiveMeasure.lean 1 declarations
BoundedRegionVolume.lean 1 declarations
BoundedSupportIntegralRepresentative.lean 1 declarations
BoundedTimeAverageIntegral.lean 1 declarations
BoundedVolumeBudget.lean 1 declarations
CanonicalBallMassLower.lean 1 declarations
CanonicalUniformBallBridge.lean 1 declarations
CenteredBallCompactness.lean 1 declarations
CenteredMetricLimit.lean 1 declarations
ClosedBallMassLimit.lean 1 declarations
ClosedThickeningMass.lean 1 declarations
CoarseEvolutionBound.lean 1 declarations
CoarseFineImageHoleVolume.lean 1 declarations
CoarseFineSourceMass.lean 1 declarations
CommonDensityMinorization.lean 2 declarations
CommonMeasuredApproximations.lean 1 declarations
CompactCenterVolumePower.lean 1 declarations
CompactDensityTimeIntegral.lean 2 declarations
CompactFactorBackwardRatio.lean 1 declarations
CompactFactorCenteredCompactness.lean 2 declarations
CompactFactorDerivative.lean 1 declarations
CompactFactorExtension.lean 6 declarations
CompactFactorInitialValue.lean 1 declarations
CompactFactorIntegrableEnvelope.lean 1 declarations
CompactFactorL2.lean 1 declarations
CompactFactorNonnegativeData.lean 1 declarations
CompactFactorNonnegativeL2.lean 1 declarations
CompactFactorScaledSource.lean 1 declarations
CompactFactorTimeMonotone.lean 1 declarations
CompactFactorTimeTail.lean 1 declarations
CompactFiberProbability.lean 1 declarations
CompactHoleBallCover.lean 1 declarations
CompactSupportedL2Limit.lean 1 declarations
CompactWeightedDensityIntegral.lean 1 declarations
CompactWeightedDensityL2.lean 2 declarations
ComparisonModel.lean 13 declarations
ComponentDistanceNodes.lean 2 declarations
ComponentHalfDistance.lean 1 declarations
ConcentratedTimeLimit.lean 1 declarations
ConcentratingProbability.lean 1 declarations
ConstantDensityMeasure.lean 2 declarations
ConstantDensitySetMass.lean 1 declarations
ContainingMassL2Error.lean 1 declarations
ContainingMassUniformL2.lean 1 declarations
ConvexImageNoSupport.lean 1 declarations
ConvexPackingDimension.lean 1 declarations
ConvexPackingFiniteDimensional.lean 1 declarations
ConvexPackingGrid.lean 3 declarations
ConvexUnitSupport.lean 1 declarations
CountablePointedCompactness.lean 1 declarations
CountableTimeCompactness.lean 1 declarations
CurvedShiftedDensity.lean 1 declarations
DensityLawSupport.lean 2 declarations
DerivativeValueCompactness.lean 2 declarations
DiagonalMeasuredApproximation.lean 1 declarations
DimensionalEvolution.lean 1 declarations
DimensionalRateContinuity.lean 3 declarations
DimensionalRateIntegralLimit.lean 1 declarations
DimensionalRatePair.lean 3 declarations
DistanceEikonal.lean 2 declarations
DistanceSourceBudget.lean 5 declarations
DistanceSourceMeasure.lean 1 declarations
DominatedCompactProbability.lean 2 declarations
DominatedProbabilityCompactness.lean 3 declarations
DyadicDistanceSources.lean 8 declarations
DyadicFlatnessLimit.lean 1 declarations
DyadicInteriorBalls.lean 2 declarations
DyadicMassComparison.lean 1 declarations
DyadicMassReindex.lean 3 declarations
DyadicPointedRigidity.lean 2 declarations
DyadicVolumeLower.lean 1 declarations
EndpointWeightApproximation.lean 2 declarations
EuclideanAbsoluteContinuousBalls.lean 2 declarations
EuclideanApproximateMinimizer.lean 1 declarations
EuclideanBallDensity.lean 4 declarations
EuclideanBallDensityLaw.lean 7 declarations
EuclideanBallHausdorffCost.lean 3 declarations
EuclideanBallMeanDerivative.lean 2 declarations
EuclideanBoundaryLayerLimit.lean 1 declarations
EuclideanCompactConvolution.lean 2 declarations
EuclideanDimensionGap.lean 8 declarations
EuclideanDyadicGrowthRigidity.lean 1 declarations
EuclideanFineBallCover.lean 1 declarations
EuclideanFiniteMeasureCompactness.lean 1 declarations
EuclideanGreenIdentity.lean 4 declarations
EuclideanHoleBall.lean 1 declarations
EuclideanInteriorSmoothExtension.lean 1 declarations
EuclideanMollifierSequence.lean 10 declarations
EuclideanPackingGrid.lean 3 declarations
EuclideanPairCompactness.lean 1 declarations
EuclideanPairCost.lean 3 declarations
EuclideanSegmentError.lean 2 declarations
EuclideanSubquadraticRigidity.lean 1 declarations
EventualPointedCompatibility.lean 1 declarations
EvolutionInitialLimit.lean 2 declarations
ExpandingPointedCompactness.lean 1 declarations
ExpandingPointedValueLimit.lean 1 declarations
ExponentialDensityIntegrals.lean 3 declarations
ExtraFactorObstruction.lean 7 declarations
FiniteCoverIntegral.lean 2 declarations
FiniteDensityMeasure.lean 4 declarations
FiniteMeasureClosedBound.lean 1 declarations
FiniteMeasureCut.lean 2 declarations
FiniteMetricValues.lean 2 declarations
FiniteSeparationCode.lean 8 declarations
FiniteSignedRadon.lean 3 declarations
FixedGaugeLocalBounds.lean 1 declarations
FixedGaugeLocalSourceMass.lean 1 declarations
FixedGaugeScaledPotential.lean 3 declarations
FullMassScaling.lean 2 declarations
GlobalVolumeGrowth.lean 3 declarations
GoodSetInteriorPoint.lean 1 declarations
HamiltonJacobiDensity.lean 1 declarations
HausdorffAlmostCover.lean 1 declarations
HausdorffOpenUpper.lean 1 declarations
HoleBallSelection.lean 1 declarations
HoleBallVolumeCover.lean 1 declarations
HoleFamilyCharge.lean 1 declarations
HoleImageGeometry.lean 3 declarations
HoleMassCharge.lean 1 declarations
HoleSourceBall.lean 2 declarations
ImageMassDensityBound.lean 1 declarations
ImageMassErrorLimit.lean 1 declarations
InjectiveHilbertMeasurable.lean 2 declarations
InnerBallValueMoments.lean 1 declarations
InnerConstantMeasure.lean 4 declarations
InnerIsometryApproximation.lean 1 declarations
InnerMeasuredApproximation.lean 1 declarations
InnerMeasuredSubsequence.lean 2 declarations
IntegralSquareProduct.lean 2 declarations
IntegratedRCDVolume.lean 1 declarations
InteriorBallMassIdentification.lean 1 declarations
IntervalMassDrop.lean 7 declarations
InverseMeasureUnique.lean 1 declarations
InwardDistance.lean 9 declarations
InwardLocality.lean 4 declarations
IsometricBallMeasure.lean 5 declarations
L1SequentialLimit.lean 1 declarations
L2ClippingApproximation.lean 6 declarations
L2IntegralRepresentative.lean 1 declarations
L2LevelMeasure.lean 2 declarations
LimitSupportTransfer.lean 1 declarations
LocalBallMeanDerivative.lean 2 declarations
LocalBallMeasureOrder.lean 2 declarations
LocalContractionAbsoluteContinuity.lean 1 declarations
LocalContractionDomination.lean 1 declarations
LocalContractionVolumeBound.lean 1 declarations
LocalDensityGluing.lean 2 declarations
LocalDensityOrder.lean 2 declarations
LocalDensitySource.lean 4 declarations
LocalIsometryDensityTransfer.lean 1 declarations
LocalMeasureProduct.lean 1 declarations
LocalSignedMeasureEquality.lean 1 declarations
LocalSignedMeasureOrder.lean 1 declarations
LocalToGlobalIsodiametric.lean 1 declarations
LocalizedLimitNorm.lean 1 declarations
LocalizedMeasuredValueLimit.lean 1 declarations
LocalizedPointedConvergence.lean 1 declarations
LogDensitySlack.lean 1 declarations
LogInverseDensity.lean 1 declarations
LongAverageMass.lean 1 declarations
LongAverageMassIntegral.lean 3 declarations
LongTimeMassSum.lean 2 declarations
LowerCurvatureVolume.lean 7 declarations
MeasurablePairSeparation.lean 1 declarations
MeasurablePointedApproximation.lean 2 declarations
MeasurablePointedSequence.lean 1 declarations
MeasuredAnnularMass.lean 2 declarations
MeasuredApproximation.lean 4 declarations
MeasuredBallLaw.lean 5 declarations
MeasuredBallSetIntegrals.lean 3 declarations
MeasuredCompactDensitySources.lean 1 declarations
MeasuredCompactDensitySupport.lean 1 declarations
MeasuredDensityPair.lean 1 declarations
MeasuredDensityPairSupport.lean 1 declarations
MeasuredDensitySources.lean 2 declarations
MeasuredEndpointLimit.lean 1 declarations
MeasuredValueLimitNorm.lean 1 declarations
MetricBallLaw.lean 4 declarations
MetricBallLawCompactness.lean 2 declarations
MetricInnerLawSubsequence.lean 1 declarations
MetricLawCompactness.lean 1 declarations
MetricLawMass.lean 3 declarations
MetricLawMassGeneral.lean 3 declarations
MetricLimit.lean 8 declarations
MetricLimitAbsoluteContinuity.lean 2 declarations
MetricLimitBallImage.lean 1 declarations
MetricLimitConstantDensity.lean 1 declarations
MetricLimitConvexImage.lean 1 declarations
MetricLimitDistanceIdentification.lean 1 declarations
MetricLimitIsodiametric.lean 1 declarations
MetricLimitLocalContraction.lean 1 declarations
MetricLimitLocalDensity.lean 1 declarations
MetricProbabilityClosedMass.lean 4 declarations
MetricSequentialCauchy.lean 1 declarations
ModelFiveBallBound.lean 1 declarations
ModelScaleControl.lean 1 declarations
ModelVolumeComparison.lean 3 declarations
MonotoneSpatialMeasurable.lean 2 declarations
MovingCompactness.lean 1 declarations
MovingPointedCompactness.lean 1 declarations
MovingPointedData.lean 1 declarations
MovingPointedLimitApproximation.lean 6 declarations
MovingPointedLimitProper.lean 3 declarations
MovingPointedNets.lean 8 declarations
NearMaximalDistanceSources.lean 1 declarations
NearbySmallBallMass.lean 1 declarations
NegativeLogDensityMass.lean 2 declarations
NoExtraFactor.lean 2 declarations
NonnegativeVolumeComparison.lean 2 declarations
PointedApproximationLifts.lean 2 declarations
PointedBallSandwich.lean 2 declarations
PointedBoundedLifts.lean 1 declarations
PointedCenteredLimit.lean 1 declarations
PointedCompactness.lean 1 declarations
PointedDualCompactness.lean 1 declarations
PointedDualLimit.lean 2 declarations
PointedEndpointCompactness.lean 1 declarations
PointedFunctionCompactness.lean 1 declarations
PointedFunctionTransfer.lean 1 declarations
PointedInnerNeighborhood.lean 1 declarations
PointedInteriorBallMass.lean 2 declarations
PointedIsometricPerturbation.lean 1 declarations
PointedLiftDistances.lean 1 declarations
PointedLimitCompatibility.lean 1 declarations
PointedLimitPacking.lean 1 declarations
PointedLimitValueBound.lean 1 declarations
PointedMeasureValues.lean 2 declarations
PointedMetricFunctionCompactness.lean 2 declarations
PointedMetricInteriorLift.lean 1 declarations
PointedMetricLimitSegments.lean 1 declarations
PointedNearbyLifts.lean 1 declarations
PointedPhysicalScale.lean 1 declarations
PointedProbabilityCompactness.lean 3 declarations
PointedScaleChange.lean 1 declarations
PointedWeightedDifference.lean 1 declarations
PositiveCompactCoreApproximation.lean 1 declarations
PositiveCoreAELimit.lean 1 declarations
PositiveDistanceLocality.lean 2 declarations
PositiveSourceMeasure.lean 4 declarations
PositiveSquaredDistance.lean 8 declarations
PowerBallDimension.lean 2 declarations
PowerBallFullImage.lean 1 declarations
PowerGrowthGeometricBound.lean 1 declarations
PowerPacking.lean 1 declarations
ProbabilityClosedMass.lean 3 declarations
ProbabilityDensityPowerBound.lean 1 declarations
ProbabilityDominationL1.lean 3 declarations
ProductFactorDiameter.lean 7 declarations
ProductPackingGrid.lean 5 declarations
ProductVerticalDeviation.lean 1 declarations
QuantitativeDimensionalCross.lean 2 declarations
RadonDensityL2Bound.lean 2 declarations
RadonProductL2Bound.lean 1 declarations
RationalInteriorBalls.lean 1 declarations
RealSliceSelection.lean 1 declarations
RecenterApproximation.lean 3 declarations
RescaledBallVolume.lean 2 declarations
RescaledCompactRepresentative.lean 1 declarations
RescaledEvolution.lean 2 declarations
RescaledFiniteNets.lean 1 declarations
RescaledPackingBound.lean 1 declarations
RescaledRootBounds.lean 1 declarations
RescalingLimitApproximation.lean 5 declarations
RescalingLimitProper.lean 3 declarations
RescalingNetFamily.lean 8 declarations
RescalingSampleLimit.lean 1 declarations
RescalingVolumeDensity.lean 2 declarations
ScalarMetricBootstrap.lean 11 declarations
ScaledCentralMass.lean 1 declarations
ScaledCompactHamiltonJacobi.lean 1 declarations
ScaledCompactHoleCover.lean 1 declarations
ScaledCompactPotentialMeasurable.lean 3 declarations
ScaledEuclideanHoleBall.lean 1 declarations
ScaledHoleVolumeCover.lean 1 declarations
ScaledImageHoleVolume.lean 1 declarations
ScaledMassBackground.lean 2 declarations
ScalingFactorMassBound.lean 2 declarations
ScalingLogDensityLimit.lean 1 declarations
SeparatedPairRestriction.lean 2 declarations
ShiftedRadonBounds.lean 4 declarations
ShiftedRadonSum.lean 1 declarations
ShortAverageMass.lean 1 declarations
SignedRadonLocal.lean 3 declarations
SignedSourceDensity.lean 1 declarations
SignedSourceWeight.lean 4 declarations
SignedWeightedRadon.lean 3 declarations
SquaredDistanceFunctionalBound.lean 1 declarations
SquaredDistanceInequality.lean 1 declarations
SquaredDistanceLocality.lean 2 declarations
SubtypeDensitySupport.lean 1 declarations
SupportedAverageDifference.lean 1 declarations
SupportedL2Continuity.lean 1 declarations
SupportedRecoverySlope.lean 2 declarations
TimeAverageApproximation.lean 2 declarations
TranslatedDensityLaw.lean 1 declarations
UniformApproximationLimit.lean 1 declarations
UniformInteriorLimitMass.lean 1 declarations
UniformInteriorLocalMass.lean 1 declarations
UniformMassBackground.lean 2 declarations
UniformVolumeRatio.lean 3 declarations
VanishingBallRatio.lean 2 declarations
VolumeBudget.lean 10 declarations
VolumeComparison.lean 5 declarations
VolumeDensity.lean 2 declarations
VolumeDensityLimit.lean 1 declarations
VolumeDerivative.lean 2 declarations
VolumeRegime.lean 5 declarations
VolumeRigidityInput.lean 4 declarations
WeightedProbabilityRecovery.lean 2 declarations
WeightedRecoveryError.lean 1 declarations
WithDensityMarginals.lean 2 declarations