OAI/NumberTheory/PiExponent/Approximation/SuccessiveApproximations.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.exists_successive_approximations line 8
2. theorem OAI.PiExponent.logarithmic_weight_bounds line 57
3. theorem OAI.PiExponent.approximation_error_at_logarithmic_weight line 62
4. def OAI.PiExponent.normalizedLogWeights line 74
5. theorem OAI.PiExponent.normalizedLogWeights_zero line 78
6. theorem OAI.PiExponent.normalizedLogWeights_succ line 81
7. theorem OAI.PiExponent.reverse_logWeights_prod line 84
8. theorem OAI.PiExponent.exists_normalized_selection_of_selector line 97
9. theorem OAI.PiExponent.exists_normalized_successive_approximations line 134