OAI/Analysis/Brenier/
1978 declarations, 0 contain sorry, 0 declared as axioms; 89 files
Files
- AffineCertificate.lean 34 declarations
- AffineOptimality.lean 14 declarations
- AffinePaths.lean 14 declarations
- AffineTies.lean 43 declarations
- Approximation.lean 13 declarations
- Argmax.lean 8 declarations
- Atomic.lean 28 declarations
- AtomicPaths.lean 5 declarations
- AtomicTransport.lean 17 declarations
- Basic.lean 12 declarations
- BoundaryStrip.lean 14 declarations
- CanonicalLaplacian.lean 15 declarations
- CanonicalPaths.lean 3 declarations
- CellContinuity.lean 22 declarations
- CellDerivative.lean 10 declarations
- CellEnergy.lean 8 declarations
- CellFaces.lean 11 declarations
- CellGeometry.lean 23 declarations
- CellMeasure.lean 40 declarations
- ClosedPaths.lean 2 declarations
- CompactMeasure.lean 14 declarations
- CompactTransport.lean 21 declarations
- Conjugacy.lean 23 declarations
- ConvexDensity.lean 8 declarations
- ConvexOptimality.lean 3 declarations
- ConvexQuantiles.lean 34 declarations
- Coordinates.lean 33 declarations
- Coupling.lean 10 declarations
- Cube.lean 49 declarations
- CutDerivative.lean 14 declarations
- CutVariation.lean 24 declarations
- DensityCDF.lean 45 declarations
- Difference.lean 17 declarations
- EndpointEnergy.lean 17 declarations
- Existence.lean 7 declarations
- FaceContinuity.lean 16 declarations
- FacetConnectivity.lean 23 declarations
- FiniteCoupling.lean 32 declarations
- FixedMass.lean 24 declarations
- Flux.lean 12 declarations
- HalfspaceKernel.lean 10 declarations
- InterceptContinuity.lean 11 declarations
- InterceptEnergy.lean 6 declarations
- Interfaces.lean 11 declarations
- Laplacian.lean 46 declarations
- LineDerivative.lean 30 declarations
- MapDistance.lean 42 declarations
- MapLimits.lean 9 declarations
- MapTransport.lean 4 declarations
- MassDerivative.lean 11 declarations
- MaxCalculus.lean 33 declarations
- MaxLimits.lean 13 declarations
- Midpoint.lean 40 declarations
- Minimizers.lean 16 declarations
- MomentAlgebra.lean 26 declarations
- MovingBoundary.lean 10 declarations
- MovingTrace.lean 18 declarations
- NormalizedPaths.lean 5 declarations
- NormalizedSections.lean 53 declarations
- Optimality.lean 18 declarations
- PlaneEnvelopes.lean 28 declarations
- Potential.lean 30 declarations
- PotentialLimits.lean 15 declarations
- PotentialTime.lean 16 declarations
- PrefixSampling.lean 44 declarations
- PrefixSections.lean 75 declarations
- PrescribedCells.lean 13 declarations
- Quantiles.lean 44 declarations
- Quantization.lean 15 declarations
- Sections.lean 45 declarations
- SharpMaps.lean 46 declarations
- SharpOptimality.lean 17 declarations
- SharpRectangle.lean 22 declarations
- SharpSlices.lean 58 declarations
- SharpTargets.lean 20 declarations
- Sharpness.lean 9 declarations
- SliceInterpolation.lean 7 declarations
- Stability.lean 2 declarations
- StationaryMoment.lean 19 declarations
- SupportingInterpolation.lean 15 declarations
- SurfaceCoordinates.lean 54 declarations
- SurfaceMeasure.lean 41 declarations
- Translation.lean 19 declarations
- TriangularDomination.lean 27 declarations
- TriangularRecursion.lean 38 declarations
- TriangularSampling.lean 22 declarations
- Uniform.lean 24 declarations
- UniformInterpolation.lean 14 declarations
- Wasserstein.lean 25 declarations