OAI/Geometry/WeakHessian/Transport/
377 declarations, 0 contain sorry, 0 declared as axioms; 78 files
Files
- ActionDistPrimitiveValues.lean 2 declarations
- ActionIntervalIntegrable.lean 4 declarations
- AeActionData.lean 3 declarations
- AeEvalAe.lean 12 declarations
- AeProdMetricSpeed.lean 2 declarations
- BoundedHopfLpDual.lean 2 declarations
- BoundedHopfLpPairing.lean 2 declarations
- BoundedHopfMap.lean 11 declarations
- BoundedHopfMapLipschitz.lean 9 declarations
- BoundedHopfMapNorm.lean 3 declarations
- BoundedMarginalSum.lean 10 declarations
- BridgeError.lean 6 declarations
- CDPlanLeg.lean 2 declarations
- CcConst.lean 12 declarations
- CdEntropyPlanBounded.lean 1 declarations
- CompactBounded.lean 10 declarations
- CompactContraction.lean 1 declarations
- CouplingConcentration.lean 3 declarations
- CouplingCostBound.lean 8 declarations
- CouplingCostHopfBound.lean 1 declarations
- DensityCouplingBound.lean 1 declarations
- DensityMeasure.lean 11 declarations
- DerivEventuallyUpperRight.lean 2 declarations
- DriftLipschitzContraction.lean 1 declarations
- DualTransportPairing.lean 1 declarations
- DynamicActionBound.lean 4 declarations
- DynamicActionBoundProper.lean 5 declarations
- EVIContraction.lean 1 declarations
- EntropyAction.lean 2 declarations
- EntropyCoupling.lean 3 declarations
- FiniteLocalization.lean 2 declarations
- FormAction.lean 8 declarations
- HopfLaxScaleTime.lean 1 declarations
- HopfLpPairingIncrement.lean 1 declarations
- HopfLpTransportPairing.lean 1 declarations
- HopfMap.lean 14 declarations
- HopfObjective.lean 31 declarations
- IntegrableEvalBounded.lean 7 declarations
- IntegratedAction.lean 2 declarations
- JoinControl.lean 11 declarations
- JoinPlanPolish.lean 2 declarations
- KineticAction.lean 10 declarations
- LiftBoundedCoupling.lean 2 declarations
- LimitPlanEntropyBound.lean 1 declarations
- LipschitzTransport.lean 1 declarations
- LocalSlopeCompContraction.lean 2 declarations
- LocalizedActionBound.lean 6 declarations
- LocalizedPlanDual.lean 1 declarations
- LocalizedPlanLaw.lean 1 declarations
- MapCompProdComap.lean 3 declarations
- MapEvalReal.lean 6 declarations
- MeasurableVariableIntervalAction.lean 2 declarations
- OptimalPlansShort.lean 17 declarations
- PerturbedAction.lean 3 declarations
- PerturbedPlanDual.lean 5 declarations
- PlanAction.lean 3 declarations
- PlanComparisonLaw.lean 2 declarations
- PlanEnergy.lean 18 declarations
- PlanEntropyCoupling.lean 1 declarations
- PlanHamiltonJacobi.lean 1 declarations
- PlanHamiltonJacobiAction.lean 2 declarations
- PlanIncrement.lean 9 declarations
- ProbabilityTightMarginals.lean 3 declarations
- QuadraticCost.lean 5 declarations
- QuadraticCostIncrement.lean 6 declarations
- RerouteFiniteSubplanShort.lean 7 declarations
- RestrictCurve.lean 8 declarations
- ScaledPlanYoung.lean 1 declarations
- SmoothedPlanSupport.lean 5 declarations
- TestAction.lean 2 declarations
- TestPlanCostReference.lean 2 declarations
- TruncatedQuadraticCost.lean 6 declarations
- TwoCouplingCost.lean 1 declarations
- UpperEnvelope.lean 13 declarations
- VariationQuotient.lean 2 declarations
- WeightedEntropyCoupling.lean 3 declarations
- WeightedPlanComparison.lean 1 declarations
- WeightedPlanHamiltonJacobi.lean 1 declarations