OAI/NumberTheory/Jacobsthal/Harmonic/WeightedAnomalyConvergence.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.BoundaryAnomaly.anomaly line 18
2. theorem OAI.Erdos970.NumberTheoryLean.BoundaryAnomaly.boundary_product_bounds line 22
3. theorem OAI.Erdos970.NumberTheoryLean.BoundaryAnomaly.anomaly_le_omission_and_benchmark line 29
4. theorem OAI.Erdos970.NumberTheoryLean.BoundaryAnomaly.actual_boundary_anomaly_decay line 43
5. theorem OAI.Erdos970.NumberTheoryLean.BoundaryAnomaly.actual_boundary_anomaly_exponential line 64
6. def OAI.Erdos970.ErdosContinuousAnomaly.continuousAnomaly line 91
7. theorem OAI.Erdos970.ErdosContinuousAnomaly.boundary_benchmark_bound line 94
8. theorem OAI.Erdos970.ErdosContinuousAnomaly.continuousAnomaly_continuousOn line 103
9. theorem OAI.Erdos970.ErdosContinuousAnomaly.anomaly_difference line 117
10. theorem OAI.Erdos970.ErdosContinuousAnomaly.uniform_anomaly_convergence line 124
11. theorem OAI.Erdos970.ErdosContinuousAnomaly.anomaly_tendsto line 159
12. theorem OAI.Erdos970.ErdosContinuousAnomaly.common_anomaly_decay line 168
13. theorem OAI.Erdos970.ErdosContinuousAnomaly.common_anomaly_exponential line 180
14. def OAI.Erdos970.ErdosBoundaryIntegral.shiftedAnomaly line 205
15. theorem OAI.Erdos970.ErdosBoundaryIntegral.shiftedAnomaly_continuousOn line 207
16. theorem OAI.Erdos970.ErdosBoundaryIntegral.shifted_anomaly_moment_integrable line 212
17. theorem OAI.Erdos970.ErdosContinuousAnomaly.weighted_anomaly_convergence line 245