OAI/NumberTheory/PiExponent/Analysis/FiniteSpacing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.FiniteSpacing.lower_bound_of_spacing line 9
2. theorem OAI.PiExponent.FiniteSpacing.sum_inv_succ_sq_le_two_sub line 29
3. theorem OAI.PiExponent.FiniteSpacing.sum_inv_succ_sq_le_two line 47
4. theorem OAI.PiExponent.FiniteSpacing.sum_inv_sq_le_two_div_sq_of_spacing line 53
5. theorem OAI.PiExponent.FiniteSpacing.sum_inv_sq_le_two_div_sq line 79
6. theorem OAI.PiExponent.FiniteSpacing.sum_inv_sq_le_two_div_sq_indexed line 101