OAI/Analysis/RCDHeat/
2048 declarations, 0 contain sorry, 0 declared as axioms; 78 files
Files
- BidirectionalPotential.lean 6 declarations
- CDSubplan.lean 18 declarations
- CompactCostTransform.lean 25 declarations
- CompactKantorovich.lean 17 declarations
- CompactSquareIntegrability.lean 17 declarations
- CompactTransportVariation.lean 14 declarations
- CompressionIntegral.lean 25 declarations
- CouplingRepair.lean 17 declarations
- CrossingOptimal.lean 18 declarations
- Density.lean 26 declarations
- DimensionalCompactWeightedGradient.lean 6 declarations
- DimensionalEntropy.lean 13 declarations
- DimensionalH1.lean 11 declarations
- DynamicalPlan.lean 20 declarations
- EVIConvexity.lean 8 declarations
- EndpointCut.lean 6 declarations
- EnergyChain.lean 37 declarations
- EnergyLp.lean 49 declarations
- EntropyPlanExtension.lean 27 declarations
- EntropySubsegment.lean 8 declarations
- EntropyWassersteinGeodesic.lean 21 declarations
- ExistingAnalytic.lean 590 declarations
- FiniteDimensionalBochnerTarget.lean 3 declarations
- FisherLimit.lean 26 declarations
- ForkPlans.lean 10 declarations
- Foundations.lean 47 declarations
- GeodesicCauchy.lean 12 declarations
- GeodesicMarginalCompact.lean 1 declarations
- GeometricSlopeOptimization.lean 10 declarations
- HeatEnergy.lean 35 declarations
- HeatEntropyPath.lean 31 declarations
- HeatFisher.lean 39 declarations
- HeatFisherSqrt.lean 19 declarations
- HeatH1.lean 30 declarations
- HeatHopfZero.lean 10 declarations
- HeatMetricSpeed.lean 29 declarations
- HeatMoments.lean 27 declarations
- HeatTest.lean 23 declarations
- HopfHeat.lean 33 declarations
- HopfTransport.lean 23 declarations
- InnerPath.lean 19 declarations
- KantorovichRadius.lean 26 declarations
- LastTimeBins.lean 6 declarations
- Main.lean 6 imports, no declarations
- MetricDescentSlope.lean 10 declarations
- MetricUpperGradient.lean 17 declarations
- MidpointEndpoint.lean 5 declarations
- Noncrossing.lean 13 declarations
- NormalizedCutoff.lean 5 declarations
- NormalizedSubplan.lean 6 declarations
- PoissonExp.lean 37 declarations
- ProbabilityCutoff.lean 9 declarations
- RelaxedChain.lean 27 declarations
- RelaxedSlope.lean 26 declarations
- ResolventFamily.lean 34 declarations
- RestrictedDensity.lean 16 declarations
- SignedEntropySupport.lean 26 declarations
- SlopeLevels.lean 14 declarations
- SlopeMeasurability.lean 26 declarations
- SobolevTestPlan.lean 14 declarations
- SqrtPairSlope.lean 33 declarations
- StrongLimit.lean 32 declarations
- TestPlanContinuous.lean 19 declarations
- UniformBoundedApply.lean 35 declarations
- UpperLipschitzEnvelope.lean 43 declarations
- VariableHeatODE.lean 10 declarations
- VariableHeatQuadratic.lean 16 declarations
- VariableRadialSecant.lean 7 declarations
- VolumeComparison.lean 15 declarations
- VolumeComparison2.lean 12 declarations
- WeightedCutoff.lean 20 declarations
- WeightedDimensionalH1Square.lean 5 declarations
- WeightedGradientConvex.lean 17 declarations
- WeightedHilbert.lean 20 declarations
- WeightedMidpointEndpoint.lean 5 declarations
- WeightedMoment.lean 11 declarations
- WeightedPlan.lean 13 declarations
- WeightedRenyi.lean 12 declarations