j_functional_equation

formal source

 152the zeros of Ξ should be confined to the real line. -/
 153
 154/-- J is symmetric under inversion: the RS "functional equation." -/
 155theorem j_functional_equation {x : ℝ} (hx : 0 < x) :
 156    Cost.Jcost x = Cost.Jcost x⁻¹ :=
 157  Cost.Jcost_symm hx
 158
 159/-- The fixed point of x ↔ 1/x is x = 1. This is the RS "critical point." -/
 160theorem inversion_fixed_point (x : ℝ) (hx : 0 < x) :
 161    x = x⁻¹ ↔ x = 1 := by
 162  constructor
 163  · intro h
 164    have hne : x ≠ 0 := ne_of_gt hx
 165    have : x * x = 1 := by
 166      calc x * x = x * x⁻¹ := by rw [← h]
 167        _ = 1 := mul_inv_cancel₀ hne
 168    have hx_sq : x ^ 2 = 1 := by rwa [sq]
 169    nlinarith [sq_nonneg (x - 1)]
 170  · intro h; rw [h]; simp
 171
 172/-- J has its unique zero at the fixed point x = 1. -/
 173theorem j_zero_at_fixed_point : Cost.Jcost 1 = 0 := Cost.Jcost_unit0
 174
 175/-- J is strictly positive away from the fixed point. -/
 176theorem j_positive_off_fixed_point (x : ℝ) (hx : 0 < x) (hne : x ≠ 1) :
 177    0 < Cost.Jcost x :=
 178  Cost.Jcost_pos_of_ne_one x hx hne
 179
 180/-! ## The RS Prediction of the Riemann Hypothesis
 181
 182**HYPOTHESIS (not theorem)**
 183
 184The Riemann Hypothesis states that all non-trivial zeros of the
 185Riemann zeta function have real part 1/2.