OAI/NumberTheory/Jacobsthal/Analysis/CorrectionWeightedIntegral.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosCorrectionLimit.densityEnvelope line 18
2. theorem OAI.Erdos970.ErdosCorrectionLimit.densityEnvelope_nonneg line 21
3. theorem OAI.Erdos970.ErdosCorrectionLimit.densityEnvelope_measurable line 24
4. theorem OAI.Erdos970.ErdosCorrectionLimit.densityEnvelope_factor line 28
5. theorem OAI.Erdos970.ErdosCorrectionLimit.densityEnvelope_section_le line 43
6. theorem OAI.Erdos970.ErdosCorrectionLimit.densityEnvelope_integrable line 56
7. theorem OAI.Erdos970.ErdosCorrectionLimit.fullRaw_integrable line 70
8. theorem OAI.Erdos970.ErdosCorrectionLimit.invariant_ratio_ge_one line 110
9. theorem OAI.Erdos970.ErdosCorrectionLimit.limiting_gap_ge_two line 134
10. theorem OAI.Erdos970.ErdosCorrectionLimit.compact_raw_tendsto line 148
11. theorem OAI.Erdos970.ErdosCorrectionLimit.compact_raw_norm_le line 161
12. theorem OAI.Erdos970.ErdosCorrectionLimit.compact_limiting_integral_tendsto line 169
13. theorem OAI.Erdos970.ErdosCorrectionLimit.compact_invariant_tendsto line 178
14. def OAI.Erdos970.ErdosCorrectionLimit.fullWeighted line 201
15. theorem OAI.Erdos970.ErdosCorrectionLimit.fullWeighted_measurable line 203
16. theorem OAI.Erdos970.ErdosCorrectionLimit.fullWeighted_integrable line 206
17. theorem OAI.Erdos970.ErdosCorrectionLimit.densityEnvelope_section_integrable line 218
18. theorem OAI.Erdos970.ErdosCorrectionLimit.fullWeighted_section_integrable line 225
19. theorem OAI.Erdos970.ErdosCorrectionLimit.full_limiting_integral_fubini line 239