OAI/NumberTheory/OrdinaryCorrelations/Elliott/SubsetCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.RawDivisorBin.subsetCost line 34
2. lemma OAI.OrdinaryCorrelations.RawDivisorBin.subsetCost_nonneg line 37
3. lemma OAI.OrdinaryCorrelations.RawDivisorBin.cost_moment line 46
4. lemma OAI.OrdinaryCorrelations.RawDivisorBin.exists_small_cost line 54
5. lemma OAI.OrdinaryCorrelations.RawDivisorBin.subset_cost_bounds line 83
6. lemma OAI.OrdinaryCorrelations.RawDivisorBin.truncated_divisor_mass line 111