OAI/NumberTheory/Jacobsthal/Partitions/GridWeightComparison.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos970.NumberTheoryLean.ConditionalBinRate.relative_error_rateline 18 - theorem
OAI.Erdos970.NumberTheoryLean.ConditionalBinRate.actual_conditional_bin_rateline 36 - theorem
OAI.Erdos970.NumberTheoryLean.GridWeightComparison.weight_local_ratioline 82 - theorem
OAI.Erdos970.NumberTheoryLean.GridWeightComparison.actual_parent_bin_upperline 100