OAI/Combinatorics/KMedianRecovery/Encoding/RationalConstants.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MetricKMedianRecovery.IntegralAssembly.countRatline 7 - def
OAI.MetricKMedianRecovery.IntegralAssembly.gapRatline 8 - def
OAI.MetricKMedianRecovery.IntegralAssembly.gammaRatline 9 - lemma
OAI.MetricKMedianRecovery.IntegralAssembly.countRat_castline 10 - lemma
OAI.MetricKMedianRecovery.IntegralAssembly.gapRat_castline 12 - lemma
OAI.MetricKMedianRecovery.IntegralAssembly.gammaRat_castline 14 - lemma
OAI.MetricKMedianRecovery.IntegralAssembly.gammaRat_posline 16 - lemma
OAI.MetricKMedianRecovery.IntegralAssembly.cap_ratline 17