`OAI/Geometry/RCD/Transport/`

817 declarations, 0 contain sorry, 0 declared as axioms; 377 files

Files

ActualRadialTransportDefect.lean 2 declarations
AmbientOptimalDualSaturation.lean 1 declarations
AnnularTransportComparison.lean 2 declarations
AsymmetricMidpoint.lean 4 declarations
AsymmetricMidpointCapacity.lean 4 declarations
AsymmetricMidpointCompression.lean 3 declarations
AsymmetricMidpointReplacement.lean 1 declarations
BoltzmannDisjointAdditivity.lean 6 declarations
BoltzmannSupportBounds.lean 4 declarations
BoundedCouplingDual.lean 3 declarations
BoundedDensityPlanFamily.lean 1 declarations
BoundedEndpointNode.lean 2 declarations
BoundedEndpointPlan.lean 1 declarations
BoundedEntropyClosed.lean 1 declarations
BoundedEntropySemicontinuous.lean 1 declarations
BoundedGeodesicPlan.lean 2 declarations
BoundedOptimalRecovery.lean 1 declarations
BoundedPathDistortion.lean 1 declarations
BoundedPlanEntropyBounds.lean 1 declarations
BoundedPlanEntropyChord.lean 1 declarations
BranchEntropyDeficit.lean 4 declarations
BranchMeshObstruction.lean 1 declarations
BrokenGeodesicCost.lean 3 declarations
CalibratedRCDPlan.lean 1 declarations
CanonicalRenyiConstruction.lean 1 declarations
CanonicalRenyiTree.lean 4 declarations
ClosedMidpointConvex.lean 2 declarations
ColumnPlanGramEndpoint.lean 1 declarations
CompactContactCompletion.lean 1 declarations
CompactContactFirstVariation.lean 1 declarations
CompactCouplingAmbientCost.lean 2 declarations
CompactCouplingLift.lean 1 declarations
CompactCouplingSlack.lean 2 declarations
CompactDualCost.lean 2 declarations
CompactFactorMidpoint.lean 1 declarations
CompactHarmonicAffinePlan.lean 1 declarations
CompactHopfDirichlet.lean 1 declarations
CompactQuadraticContact.lean 1 declarations
ComponentScalarChord.lean 1 declarations
ComponentScalarMidpoint.lean 1 declarations
CompressedAllInverse.lean 2 declarations
CompressedEntropyConvexity.lean 1 declarations
CompressedEvaluationInverse.lean 2 declarations
CompressedFiniteUnique.lean 1 declarations
CompressedInitialInverse.lean 2 declarations
CompressedPlanChildren.lean 1 declarations
CompressedPlanMixture.lean 2 declarations
CompressedPlanUnique.lean 1 declarations
CompressedRadialPlan.lean 1 declarations
CompressedSegmentIntegral.lean 2 declarations
CompressedSegmentNullSet.lean 1 declarations
CompressedSubplanDensity.lean 1 declarations
CompressedSubplanNode.lean 2 declarations
ConcentratedMidpointLimit.lean 1 declarations
ContactCrossLength.lean 1 declarations
ContinuousDensityCoupling.lean 4 declarations
ContinuousDensityEntropy.lean 2 declarations
ContinuousLengthDistortion.lean 3 declarations
CurvatureCompressionBound.lean 3 declarations
CurvatureMidpointLimit.lean 2 declarations
DiagonalHopfRecoverySlope.lean 1 declarations
DimensionalCutoff.lean 1 declarations
DimensionalExpansion.lean 1 declarations
DimensionalExpansionZero.lean 1 declarations
DimensionalH1.lean 1 declarations
DimensionalPotential.lean 1 declarations
DimensionalSlope.lean 1 declarations
DimensionalSubgradient.lean 1 declarations
DiracTransportCost.lean 2 declarations
DistancePoissonOptimalMean.lean 1 declarations
DominatedEndpointTails.lean 2 declarations
DominatedOptimalPlan.lean 1 declarations
EndpointChordLimit.lean 2 declarations
EndpointDominatedOptimality.lean 1 declarations
EntropicDirectionalBound.lean 3 declarations
EntropyChordAlgebra.lean 3 declarations
EntropyGapUpper.lean 1 declarations
ExactAffineGeodesic.lean 1 declarations
ExponentialEntropyComparison.lean 3 declarations
ExponentialTiltLpVariation.lean 4 declarations
ExponentialTiltVariation.lean 2 declarations
FiniteComponentChord.lean 1 declarations
FiniteContinuousChord.lean 1 declarations
FirstOrderDistanceDistortion.lean 1 declarations
FirstOrderNearbyPlanErrors.lean 2 declarations
FirstOrderUniformDistortion.lean 1 declarations
FullReducedMidpoint.lean 1 declarations
GeodesicPackingSamples.lean 3 declarations
GeodesicPlanTightness.lean 2 declarations
GeodesicProductSamples.lean 1 declarations
GeodesicShortSteps.lean 1 declarations
GeodesicSquareLower.lean 2 declarations
GlobalLengthRootMaximality.lean 1 declarations
GlobalRenyiLeftComponent.lean 1 declarations
GlobalRenyiMidpoint.lean 2 declarations
GlobalRenyiRightComponent.lean 1 declarations
HalfRestrictedOptimalPlan.lean 1 declarations
HamiltonJacobiPlanBound.lean 1 declarations
HarmonicFamilyGeodesicAffine.lean 1 declarations
HarmonicGeodesicAffine.lean 2 declarations
HarmonicOptimalPlanMean.lean 1 declarations
HopfDirichletSequence.lean 1 declarations
HopfRecoveryTime.lean 6 declarations
HyperbolicChord.lean 6 declarations
HyperbolicChordLimit.lean 3 declarations
HyperbolicDistortion.lean 8 declarations
InitialEntropyObstruction.lean 1 declarations
LastPathAgreement.lean 7 declarations
LengthBinIntegral.lean 3 declarations
LengthComponentCompression.lean 1 declarations
LengthComponentDyadic.lean 1 declarations
LengthComponentIntegral.lean 2 declarations
LengthComponentNode.lean 1 declarations
LengthReplacementSeparation.lean 1 declarations
LengthRestrictionSubpath.lean 1 declarations
LengthRootMaximality.lean 1 declarations
LocalBochnerTransport.lean 5 declarations
LocalFeatureConvexImage.lean 4 declarations
LocalFeatureInner.lean 6 declarations
LocalFeatureSpace.lean 10 declarations
LocalHarmonicBoundedPlan.lean 1 declarations
LocalHarmonicGeodesic.lean 1 declarations
LocalHarmonicOptimalMean.lean 1 declarations
LocalHilbertEmbedding.lean 1 declarations
LocalLipschitzPlanMean.lean 1 declarations
LocalMidpointDensityComparison.lean 2 declarations
LocalMidpointDensityConstant.lean 1 declarations
LocalMidpointFeatures.lean 8 declarations
LocalPlanGradientMean.lean 1 declarations
LocalQuadraticMidpointGeometry.lean 7 declarations
LocalRenyiMaximality.lean 2 declarations
LocalSmoothEntropy.lean 1 declarations
LocalizedPlanEnergy.lean 1 declarations
MaximalCompressionChildren.lean 1 declarations
MaximalMidpointCompression.lean 1 declarations
MaximalScalarMidpoint.lean 1 declarations
MaximalTreeCompression.lean 2 declarations
MaximalTreeScalarChord.lean 1 declarations
MeasuredTransportData.lean 2 declarations
MeasuredTransportSupport.lean 1 declarations
MeasuredTransportValues.lean 1 declarations
MeetingPairCollapse.lean 1 declarations
MeetingSplice.lean 7 declarations
MeetingSpliceGeometry.lean 2 declarations
MeetingSpliceOptimality.lean 1 declarations
MetricLimitCompactMidpoint.lean 1 declarations
MetricLimitMidpointContraction.lean 2 declarations
MetricLimitMidpointExact.lean 1 declarations
MetricLimitSetMidpoint.lean 1 declarations
MetricLocalMidpointLaw.lean 2 declarations
MetricLocalMidpointVolume.lean 2 declarations
MetricPreimageMidpointVolume.lean 1 declarations
MetricSetMidpointLaw.lean 2 declarations
MetricSetMidpointVolume.lean 1 declarations
MidpointDimensionAlgebra.lean 5 declarations
MidpointLengthApproximation.lean 9 declarations
MidpointMinCoefficientLimit.lean 1 declarations
MidpointMinMass.lean 1 declarations
MidpointReducedComparison.lean 5 declarations
MidpointSupportVolume.lean 2 declarations
MidpointThickening.lean 3 declarations
NearbyAffineGeodesic.lean 1 declarations
NearbyBallPlan.lean 1 declarations
NearbyEndpointPlan.lean 1 declarations
NearbyPlanCompression.lean 1 declarations
NearbySegment.lean 2 declarations
NearbySegmentCompression.lean 3 declarations
NoResolvedBranchWindow.lean 1 declarations
ObservableSubplanDensity.lean 1 declarations
ObservableSubplans.lean 3 declarations
OptimalAveragePlan.lean 1 declarations
OptimalCommonContactSet.lean 2 declarations
OptimalComponentSeparation.lean 2 declarations
OptimalDualSaturation.lean 1 declarations
OptimalExactSplice.lean 3 declarations
OptimalGeodesicLengths.lean 3 declarations
OptimalInitialLength.lean 1 declarations
OptimalInitialSubmeasure.lean 2 declarations
OptimalLengthLaw.lean 4 declarations
OptimalLengthLocalization.lean 2 declarations
OptimalLengthObservable.lean 2 declarations
OptimalMidpointSplice.lean 2 declarations
OptimalRadialMidpoint.lean 1 declarations
OptimalRadialTime.lean 1 declarations
OptimalRightSplice.lean 2 declarations
OptimalSpeedTransfer.lean 1 declarations
OptimalSubmeasureLength.lean 1 declarations
OptimalSubplanSplice.lean 1 declarations
OptimalTripletCompletion.lean 1 declarations
OrthonormalHarmonicGeodesic.lean 2 declarations
PairedBranchLaws.lean 6 declarations
PairedEntropyChords.lean 1 declarations
PairedEntropyDeficit.lean 1 declarations
PairedInitialObstruction.lean 1 declarations
PairedInitialUniqueness.lean 1 declarations
PairedLipschitzCompactness.lean 1 declarations
PairedPathUniqueness.lean 1 declarations
PairedPrefixUniqueness.lean 1 declarations
PairedSuffixUniqueness.lean 1 declarations
PathAgreement.lean 6 declarations
PathMeetingSplice.lean 7 declarations
PathReversal.lean 5 declarations
PlanEndpointComparison.lean 2 declarations
PlanEntropyDerivative.lean 1 declarations
PlanGradientMean.lean 1 declarations
PlanLimitMarginals.lean 1 declarations
PlanLogDensity.lean 1 declarations
PlanMeanEnergy.lean 1 declarations
PointedGeodesicBall.lean 2 declarations
PointedGeodesicInterpolation.lean 1 declarations
PointedGeodesicWithin.lean 1 declarations
PointedHopfErrorLimit.lean 2 declarations
PointedHopfLaxLower.lean 1 declarations
PointedHopfLaxUpper.lean 1 declarations
PointedHopfMinimizer.lean 3 declarations
PointedHopfSlope.lean 1 declarations
PointedLocalGeodesic.lean 2 declarations
PointedLocalPlanSupport.lean 1 declarations
PointedMidpointBalls.lean 2 declarations
PointedMidpointSets.lean 3 declarations
PointedOptimalEndpointCompactness.lean 1 declarations
PointedOptimalLimit.lean 1 declarations
PointedPlanCompactness.lean 1 declarations
PointedPlanCost.lean 2 declarations
PointedPlanSupport.lean 2 declarations
PointedPotentialContact.lean 1 declarations
PointedTransportMarginals.lean 1 declarations
PointedVerticalGeodesic.lean 1 declarations
PointwisePlanComparison.lean 1 declarations
PointwiseReduced.lean 1 declarations
PositiveExponentialTilt.lean 2 declarations
PrescribedPlanCompression.lean 1 declarations
QuadraticGeodesicGeometry.lean 11 declarations
QuadraticGeodesicUniqueness.lean 2 declarations
QuadraticMidpointError.lean 5 declarations
QuadraticMidpointLimit.lean 2 declarations
QuadraticMidpointSelection.lean 1 declarations
QuadraticPlanIntegrability.lean 2 declarations
RadialDistortionContinuity.lean 1 declarations
RadialGeodesic.lean 4 declarations
RadialMidpoint.lean 1 declarations
RadialMidpointRigidity.lean 1 declarations
RadialPlanSlope.lean 2 declarations
RadialTimeCompression.lean 3 declarations
RadialTransport.lean 2 declarations
RadialTransportCutoff.lean 4 declarations
RadialTransportCutoffBounds.lean 1 declarations
RadialTransportError.lean 2 declarations
RadialTransportEstimate.lean 1 declarations
RadialTransportEulerIdentity.lean 1 declarations
RadialTransportForcing.lean 2 declarations
RadialTransportGeometry.lean 4 declarations
RadialTransportIdentity.lean 1 declarations
RadialTransportWeight.lean 6 declarations
RecoveryLimit.lean 1 declarations
RecoveryPlanCost.lean 2 declarations
ReducedChord.lean 6 declarations
ReducedChordMeshLimit.lean 1 declarations
ReducedChordScaling.lean 2 declarations
ReducedDistanceLimit.lean 3 declarations
ReducedDistortionNonpositive.lean 3 declarations
ReducedDistortionPositive.lean 2 declarations
ReducedDistortionRecurrence.lean 5 declarations
ReducedDyadicChord.lean 2 declarations
ReducedInterpolation.lean 2 declarations
ReducedMidpoint.lean 1 declarations
ReducedRecovery.lean 1 declarations
ReflectedMidpointDiameter.lean 1 declarations
ReflectedMidpointMass.lean 1 declarations
RelativeEntropyDerivative.lean 1 declarations
RelativeEntropyIntegral.lean 3 declarations
RelativeEntropyRemainder.lean 3 declarations
RelativePowerRemainder.lean 2 declarations
RenyiChord.lean 1 declarations
RenyiDisjointAdditivity.lean 2 declarations
RenyiDual.lean 8 declarations
RenyiDualIntegral.lean 4 declarations
RenyiDualScore.lean 6 declarations
RenyiDyadicChord.lean 1 declarations
RenyiDyadicConstruction.lean 1 declarations
RenyiDyadicData.lean 3 declarations
RenyiEnergyIntegrability.lean 3 declarations
RenyiFiniteAdditivity.lean 2 declarations
RenyiGlobalVariation.lean 1 declarations
RenyiHomogeneity.lean 1 declarations
RenyiIntegralAdditivity.lean 3 declarations
RenyiInverseDensity.lean 1 declarations
RenyiLeftComponent.lean 1 declarations
RenyiLocalVariation.lean 2 declarations
RenyiLocalization.lean 2 declarations
RenyiMeasureReplacement.lean 1 declarations
RenyiMidpointAbsoluteContinuity.lean 2 declarations
RenyiMidpointCompression.lean 2 declarations
RenyiMidpointInequality.lean 2 declarations
RenyiMidpointShort.lean 2 declarations
RenyiNodeChildren.lean 11 declarations
RenyiOptimalMidpoint.lean 2 declarations
RenyiPathPrimitive.lean 3 declarations
RenyiPathSemicontinuity.lean 7 declarations
RenyiPathTails.lean 5 declarations
RenyiPathVariation.lean 2 declarations
RenyiPerturbation.lean 6 declarations
RenyiPerturbationIntegral.lean 1 declarations
RenyiPlanVariation.lean 4 declarations
RenyiReweight.lean 3 declarations
RenyiRightComponent.lean 1 declarations
RenyiScalarMidpoint.lean 2 declarations
RenyiSemicontinuity.lean 5 declarations
RenyiSingularReplacement.lean 2 declarations
RenyiSmoothDual.lean 10 declarations
RenyiSobolev.lean 7 declarations
RenyiSobolevDensity.lean 1 declarations
RenyiSubmeasureBound.lean 1 declarations
RenyiSubplanMaximality.lean 1 declarations
RenyiTangent.lean 2 declarations
RenyiTransportNode.lean 4 declarations
RenyiTreeChord.lean 1 declarations
RenyiTreeClosed.lean 3 declarations
RenyiTreeCompactness.lean 2 declarations
RenyiTreeCompression.lean 2 declarations
RenyiTreeMaximality.lean 2 declarations
RescaledTransportPotentials.lean 1 declarations
ResolvePathBranch.lean 8 declarations
ResolvedBranchMeasure.lean 7 declarations
ResolvedBranchMixture.lean 15 declarations
ResolvedBranchSelection.lean 1 declarations
ResolvedBranchWindow.lean 1 declarations
ResolvedPairAgreement.lean 6 declarations
ResolvedSubplanCompression.lean 2 declarations
ResolvedSubplanEntropy.lean 1 declarations
ResolvedSubplanEntropyBounds.lean 1 declarations
ResolvedSubplanOptimality.lean 1 declarations
RestrictedMidpointContraction.lean 1 declarations
ScaledPlanHessianLimit.lean 1 declarations
ScaledRadialTransport.lean 2 declarations
ScaledRadialTransportEstimate.lean 1 declarations
ScaledRadialTransportForcing.lean 2 declarations
ScaledRadialTransportGeometry.lean 3 declarations
ScaledTransportConstants.lean 1 declarations
SegmentEntropyConvexity.lean 1 declarations
SelectedPlanLengthWindows.lean 1 declarations
ShiftedEntropyBounds.lean 3 declarations
ShortEndpointCompression.lean 2 declarations
ShortPlanFlux.lean 3 declarations
SmoothHopfRecoverySlope.lean 1 declarations
SobolevHamiltonJacobiPlan.lean 1 declarations
SobolevPlanDerivative.lean 1 declarations
SobolevPlanVariation.lean 2 declarations
StrongEntropy.lean 1 declarations
StrongEntropyMeasure.lean 1 declarations
StrongReduced.lean 1 declarations
SubpathMeanVariation.lean 2 declarations
SubpathMeasureSub.lean 1 declarations
SubplanAbsoluteIntegral.lean 2 declarations
SubplanReduced.lean 1 declarations
TestPlanIntervalFlux.lean 3 declarations
TestPlanLocalProperty.lean 1 declarations
TestPlanMeanSlope.lean 1 declarations
TestPlanTemporalDifference.lean 6 declarations
TiltPowerVariation.lean 2 declarations
TranslatedCouplingCost.lean 1 declarations
TransportCostEnergy.lean 3 declarations
TransportLevelBound.lean 2 declarations
TransportPoincare.lean 4 declarations
TransportPotentialCompactness.lean 1 declarations
TripletTransportCost.lean 1 declarations
UniformEndpointCompression.lean 1 declarations
UniformLengthPartition.lean 6 declarations
UnnormalizedReduced.lean 1 declarations
WeakGeodesicPlan.lean 2 declarations
WeakLengthCompression.lean 4 declarations
WeakMidpointMass.lean 1 declarations
WeakOptimalRecovery.lean 1 declarations
WeakPlanCost.lean 2 declarations
WeightedChordBins.lean 2 declarations
WeightedMatchedOptimality.lean 1 declarations
WeightedTransportEnergy.lean 1 declarations