132theorem j_submult {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : 133 Cost.Jcost (x * y) ≤ 134 2 * Cost.Jcost x + 2 * Cost.Jcost y + 2 * Cost.Jcost x * Cost.Jcost y :=
proof body
Term-mode proof.
135 Cost.Jcost_submult hx hy 136 137/-! ## The Reciprocal Symmetry and the Critical Line 138 139The RS cost function satisfies J(x) = J(1/x): reciprocal symmetry. 140The ζ functional equation has the analogous reflection s ↔ 1-s. 141 142The critical line Re(s) = 1/2 is the fixed point of s ↔ 1-s, 143just as x = 1 is the fixed point of x ↔ 1/x. 144 145The completed zeta function ξ(s) = ξ(1-s) has this same symmetry. 146Defining Ξ(t) := ξ(1/2 + it), RH is equivalent to: 147"all zeros of Ξ are real." 148 149The RS structural prediction: 150Since d'Alembert solutions have zeros on lines, 151and the ledger's cost structure is governed by d'Alembert, 152the zeros of Ξ should be confined to the real line. -/ 153 154/-- J is symmetric under inversion: the RS "functional equation." -/
depends on (24)
Lean names referenced from this declaration's body.