Failure of the Riemann hypothesis forces psi-oscillation
OpenLandauCriterion.psi_oscillation_of_not_riemannHypothesisAssume the Riemann hypothesis is false. Then there are real numbers and such that, for every , the error exceeds for arbitrarily large and also falls below for arbitrarily large . This is the classical oscillation theorem: a zero off the critical line forces the prime distribution to oscillate on both sides of its main term at a power scale. This is the reverse analytic direction of the criterion.
import Mathlib
namespace LandauCriterion
theorem psi_oscillation_of_not_riemannHypothesis (h : ¬ RiemannHypothesis) :
∃ β c : ℝ, 1 / 2 < β ∧ 0 < c ∧ ∀ ε : ℝ, 0 < ε →
(Filter.Frequently (fun x : ℝ => c * x ^ (β - ε) ≤ Chebyshev.psi x - x) Filter.atTop) ∧
(Filter.Frequently (fun x : ℝ => Chebyshev.psi x - x ≤ -c * x ^ (β - ε)) Filter.atTop) := by sorry
end LandauCriterionRead-back
What the Lean code literally says, in plain math · Muse Spark
Assuming the negation of the proposition named , there exist real numbers and — existence only, not uniqueness — such that and , with no upper bound on stated, and such that for every real , with the same and serving for all such , both of the following hold: it is frequently the case, in the sense of arbitrarily large (that is, beyond any given threshold there is some satisfying the inequality, which is weaker than the inequality holding for all sufficiently large ), that , and it is likewise frequently the case, in the same arbitrarily-large- sense, that , where denotes the function named , ranges over the real numbers, and is the real power.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.