OAI/Analysis/CoulombTransport/
667 declarations, 0 contain sorry, 0 declared as axioms; 97 files
Files
- ActualGeometryConclusion.lean 3 declarations
- All.lean 94 imports, no declarations
- AnalyticCoulomb.lean 5 declarations
- AtomlessMap.lean 2 declarations
- AtomlessTransport.lean 5 declarations
- AxisHessian.lean 21 declarations
- BorelTransport.lean 3 declarations
- BranchCoupling.lean 15 declarations
- BranchDensity.lean 6 declarations
- BranchInterfaces.lean 2 declarations
- BranchOptimizer.lean 4 declarations
- BranchSeparation.lean 8 declarations
- Calibration.lean 15 declarations
- CellOscillation.lean 1 declarations
- CellTable.lean 16 declarations
- CellwiseLift.lean 2 declarations
- CenterAxis.lean 7 declarations
- CenterCertificate.lean 14 declarations
- CertificateAttainment.lean 9 declarations
- CertificateDuality.lean 13 declarations
- CertificateNeighborhoods.lean 4 declarations
- CommonBranches.lean 14 declarations
- CompactLiftApproximation.lean 2 declarations
- CompactPartition.lean 3 declarations
- CompactSeparation.lean 1 declarations
- ComponentCertificate.lean 5 declarations
- ComponentPotential.lean 7 declarations
- ComponentRegions.lean 1 declarations
- Conclusion.lean 1 declarations
- ContactCommonBranches.lean 1 declarations
- ContactObstruction.lean 3 declarations
- ContactSelection.lean 3 declarations
- ContactSelectionAE.lean 7 declarations
- ContinuousCDF.lean 2 declarations
- CostTopology.lean 7 declarations
- CoulombBranches.lean 1 declarations
- CoulombCalculus.lean 24 declarations
- CoulombCharts.lean 5 declarations
- CoulombCoercivity.lean 9 declarations
- CoulombEstimates.lean 16 declarations
- CoulombLocalCertificate.lean 4 declarations
- CoulombSupportExistence.lean 6 declarations
- CoulombSupportSeparated.lean 3 declarations
- CounterexampleAssembly.lean 6 declarations
- CouplingSupport.lean 4 declarations
- Density.lean 3 declarations
- DensityMeasure.lean 4 declarations
- DensityMixture.lean 5 declarations
- DisjointSquares.lean 4 declarations
- DualCertificate.lean 7 declarations
- Endgame.lean 2 declarations
- EqualInfima.lean 5 declarations
- ExistenceFromLocalGeometry.lean 1 declarations
- ExtendedPushforward.lean 3 declarations
- FiniteMassSplit.lean 6 declarations
- FirstCoordinateLift.lean 4 declarations
- FiveComponentCanonical.lean 2 declarations
- FiveComponentGeometry.lean 15 declarations
- FiveComponentGlobal.lean 6 declarations
- FiveComponentSelection.lean 1 declarations
- GeometryJets.lean 7 declarations
- GluedCertificate.lean 2 declarations
- GluedCertificateForward.lean 1 declarations
- GoodTypePermutation.lean 5 declarations
- GraphBridge.lean 12 declarations
- HessianCLM.lean 26 declarations
- HessianCoercivity.lean 6 declarations
- HessianMatrix.lean 13 declarations
- IsometryTransport.lean 17 declarations
- JacobianSquareRoot.lean 11 declarations
- LocalBranchMeasure.lean 10 declarations
- LocalCertificate.lean 3 declarations
- LocalImplicit.lean 12 declarations
- LocalPotentialBounds.lean 1 declarations
- LocalSplitting.lean 2 declarations
- Main.lean 2 imports, no declarations
- Model.lean 19 declarations
- NeighborhoodCertificate.lean 4 declarations
- OptimalLocalization.lean 9 declarations
- PairEnergyFinite.lean 12 declarations
- PartitionLabel.lean 7 declarations
- PartitionTransport.lean 7 declarations
- ProductPlan.lean 9 declarations
- RealCounterexampleAssembly.lean 3 declarations
- SeparatedLiftApproximation.lean 2 declarations
- SmoothBranchMarginal.lean 19 declarations
- SmoothPushforward.lean 10 declarations
- SplitMeasure.lean 8 declarations
- Splitting.lean 3 declarations
- SplittingConstruction.lean 1 declarations
- StateDual.lean 7 declarations
- StationaryConvexity.lean 5 declarations
- StationaryEquation.lean 12 declarations
- StationaryMap.lean 11 declarations
- StrictMinimum.lean 6 declarations
- Symmetrization.lean 17 declarations
- TriplePermutation.lean 10 declarations