OAI/NumberTheory/Jacobsthal/Harmonic/ZeroFrequencyBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosHyperbolaError.restrictionCount line 13
2. theorem OAI.Erdos970.ErdosHyperbolaError.restrictionCount_nonneg line 16
3. theorem OAI.Erdos970.ErdosHyperbolaError.restrictionCount_le_modulus line 19
4. theorem OAI.Erdos970.ErdosHyperbolaError.restrictionCount_ratio line 32
5. theorem OAI.Erdos970.ErdosHyperbolaError.restricted_zero_eq_real line 42
6. theorem OAI.Erdos970.ErdosHyperbolaError.product_approx_error line 48
7. theorem OAI.Erdos970.ErdosHyperbolaError.product_count_error line 58
8. theorem OAI.Erdos970.ErdosHyperbolaError.zero_frequency_rounding line 68