OAI/Combinatorics/KMedianRecovery/Geometry/
439 declarations, 0 contain sorry, 0 declared as axioms; 33 files
Files
- AllBadCostBound.lean 3 declarations
- ClusterCost.lean 11 declarations
- ExecutionClusterCostOne.lean 3 declarations
- FamilyMetric.lean 8 declarations
- IndexedCost.lean 9 declarations
- LeafDistances.lean 20 declarations
- LocalBest.lean 27 declarations
- LocalCandidates.lean 31 declarations
- LocalFuel.lean 17 declarations
- LocalIndex.lean 12 declarations
- LocalRefineMachine.lean 7 declarations
- LocalSets.lean 41 declarations
- LocalTransport.lean 5 declarations
- Metric.lean 8 declarations
- MetricAnchor.lean 13 declarations
- MetricArrays.lean 16 declarations
- MetricCost.lean 2 declarations
- MetricCost2.lean 23 declarations
- MetricParser.lean 37 declarations
- Nearest.lean 15 declarations
- NearestDistance.lean 27 declarations
- NearestHeight.lean 1 declarations
- NearestImage.lean 18 declarations
- NearestImages.lean 1 declarations
- NearestInsertEqual.lean 11 declarations
- NearestLeafMachine.lean 12 declarations
- NearestMap.lean 15 declarations
- OptimumClusterSeparation.lean 2 declarations
- OptimumMinCard.lean 1 declarations
- RealCost.lean 2 declarations
- RoundingArithmetic.lean 11 declarations
- RoundingMatrix.lean 21 declarations
- RoundingPrecision.lean 9 declarations