OAI/NumberTheory/Jacobsthal/Partitions/GeometricRangeInverse.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.NormalizedBoxException.weighted_witness_le_total line 17
2. theorem OAI.Erdos970.NumberTheoryLean.NormalizedBoxException.unnormalize_witness line 23
3. theorem OAI.Erdos970.NumberTheoryLean.NormalizedBoxException.selection_exception_bound line 34
4. theorem OAI.Erdos970.NumberTheoryLean.ActualInverseFullBoxMass.actual_inverse_full_box_mass line 53
5. theorem OAI.Erdos970.NumberTheoryLean.GeometricFullBoxInverse.geometric_full_box_inverse line 77
6. theorem OAI.Erdos970.NumberTheoryLean.GeometricRangeInverse.geometric_range_inverse line 176