OAI/NumberTheory/Jacobsthal/Estimates/CorrectionStateSections.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosCorrectionLimit.even_inverse_product line 19
2. theorem OAI.Erdos970.ErdosCorrectionLimit.odd_inverse_product line 36
3. theorem OAI.Erdos970.ErdosCorrectionLimit.state_inverse_integral line 53
4. def OAI.Erdos970.ErdosCorrectionLimit.cutoffAmplitude line 88
5. theorem OAI.Erdos970.ErdosCorrectionLimit.cutoffAmplitude_measurable line 91
6. theorem OAI.Erdos970.ErdosCorrectionLimit.cutoffAmplitude_integral line 95
7. theorem OAI.Erdos970.ErdosCorrectionLimit.fullWeighted_cutoff line 128
8. theorem OAI.Erdos970.ErdosCorrectionLimit.fullWeighted_section line 136
9. theorem OAI.Erdos970.ErdosCorrectionLimit.even_cutoff_length line 145
10. theorem OAI.Erdos970.ErdosCorrectionLimit.odd_cutoff_length line 152
11. def OAI.Erdos970.ErdosCorrectionLimit.radialNumerator line 159
12. theorem OAI.Erdos970.ErdosCorrectionLimit.fullWeighted_section_radial line 163