module module

`IndisputableMonolith.NumberTheory.RiemannHypothesis.PrimeTailBounds`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.NumberTheory.Port module_import
IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget module_import

declarations in this module (16)

theorem prime_rpow_summable L53
theorem prime_rpow_tsum_exists L59
theorem rpow_neg_nonneg' L73
theorem summable_nat_rpow_neg_subtype L78
theorem antitoneOn_rpow_neg L86
theorem integral_rpow_neg L96
theorem integral_rpow_neg_improper L113
theorem integer_tail_tsum_le L138
theorem prime_tail_le_integer_tail L213
theorem prime_tail_tsum_bound L228
theorem primeTailBound_christmas L252
theorem primeTailBound_of_explicit L261
structure ArithmeticApproximant L274
structure PassiveCertificate L284
def ArithmeticDeformationIdentification L301
theorem attachmentWithMargin_of_bossLemma L307