OAI/NumberTheory/Jacobsthal/Analysis/ContinuousCorrectionLimit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosBoundaryIntegral.even_ratio_integral line 17
2. theorem OAI.Erdos970.ErdosBoundaryIntegral.odd_ratio_integral line 19
3. theorem OAI.Erdos970.ErdosBoundaryIntegral.nested_ratio_coefficient_eq_twice_I line 42
4. theorem OAI.Erdos970.ErdosCorrectionLimit.anomaly_moment_integrable line 80
5. theorem OAI.Erdos970.ErdosCorrectionLimit.exp_cutoff_integral line 98
6. def OAI.Erdos970.ErdosCorrectionLimit.evenRadial line 125
7. def OAI.Erdos970.ErdosCorrectionLimit.oddRadial line 126
8. theorem OAI.Erdos970.ErdosCorrectionLimit.radial_parts_integrable line 128
9. theorem OAI.Erdos970.ErdosCorrectionLimit.full_limiting_integral_eq line 147
10. theorem OAI.Erdos970.ErdosCorrectionLimit.compact_invariant_coefficient_tendsto line 182
11. theorem OAI.Erdos970.ErdosCorrectionLimit.full_continuous_correction_limit line 187