11.1. HardyZeta.CriticalLine🔗

def criticalPoint (t : ℝ) : ℂ := 1 / 2 + t * Complex.I@[simp] theorem criticalPoint_re (t : ℝ) : (criticalPoint t).re = 1 / 2 := byt:ℝ⊢ (criticalPoint t).re = 1 / 2 simp [criticalPoint]All goals completed! 🐙@[simp] theorem criticalPoint_im (t : ℝ) : (criticalPoint t).im = t := byt:ℝ⊢ (criticalPoint t).im = t simp [criticalPoint]All goals completed! 🐙theorem criticalPoint_injective : Function.Injective criticalPoint := by⊢ Function.Injective criticalPoint intro t u ht:ℝu:ℝh:criticalPoint t = criticalPoint u⊢ t = u simpa using congrArg Complex.im hAll goals completed! 🐙theorem criticalPoint_ne_zero (t : ℝ) : criticalPoint t ≠ 0 := byt:ℝ⊢ criticalPoint t ≠ 0 intro ht:ℝh:criticalPoint t = 0⊢ False have := congrArg Complex.re ht:ℝh:criticalPoint t = 0this:(criticalPoint t).re = Complex.re 0⊢ False simp at thisAll goals completed! 🐙theorem criticalPoint_ne_one (t : ℝ) : criticalPoint t ≠ 1 := byt:ℝ⊢ criticalPoint t ≠ 1 intro ht:ℝh:criticalPoint t = 1⊢ False have := congrArg Complex.re ht:ℝh:criticalPoint t = 1this:(criticalPoint t).re = Complex.re 1⊢ False simp at thisAll goals completed! 🐙theorem continuous_criticalPoint : Continuous criticalPoint := by⊢ Continuous criticalPoint unfold criticalPoint⊢ Continuous fun t => 1 / 2 + ↑t * Complex.I fun_propAll goals completed! 🐙 /-- Riemann's xi normalization, used only away from its removable singularities here. -/def xi (s : ℂ) : ℂ := (1 / 2) * s * (s - 1) * completedRiemannZeta s /-- The complex-valued restriction; reality is a separate theorem, not a coercion assumption. -/def criticalXi (t : ℝ) : ℂ := xi (criticalPoint t)theorem completedZeta_criticalPoint_eq_zero_iff (t : ℝ) : completedRiemannZeta (criticalPoint t) = 0 ↔ riemannZeta (criticalPoint t) = 0 := byt:ℝ⊢ completedRiemannZeta (criticalPoint t) = 0 ↔ riemannZeta (criticalPoint t) = 0 rw [riemannZeta_def_of_ne_zero (criticalPoint_ne_zero t)t:ℝ⊢ completedRiemannZeta (criticalPoint t) = 0 ↔ completedRiemannZeta (criticalPoint t) / (criticalPoint t).Gammaℝ = 0]t:ℝ⊢ completedRiemannZeta (criticalPoint t) = 0 ↔ completedRiemannZeta (criticalPoint t) / (criticalPoint t).Gammaℝ = 0 have hg : Complex.Gammaℝ (criticalPoint t) ≠ 0 := Complex.Gammaℝ_ne_zero_of_re_pos (byt:ℝ⊢ 0 < (criticalPoint t).re simpAll goals completed! 🐙)t:ℝhg:(criticalPoint t).Gammaℝ ≠ 0⊢ completedRiemannZeta (criticalPoint t) = 0 ↔ completedRiemannZeta (criticalPoint t) / (criticalPoint t).Gammaℝ = 0 simp [div_eq_zero_iff, hg]All goals completed! 🐙theorem criticalXi_eq_zero_iff (t : ℝ) : criticalXi t = 0 ↔ riemannZeta (criticalPoint t) = 0 := byt:ℝ⊢ criticalXi t = 0 ↔ riemannZeta (criticalPoint t) = 0 simp only [criticalXi, xi, mul_eq_zero]t:ℝ⊢ ((1 / 2 = 0 ∨ criticalPoint t = 0) ∨ criticalPoint t - 1 = 0) ∨ completedRiemannZeta (criticalPoint t) = 0 ↔ riemannZeta (criticalPoint t) = 0 simp [criticalPoint_ne_zero, criticalPoint_ne_one, sub_eq_zero, completedZeta_criticalPoint_eq_zero_iff]All goals completed! 🐙theorem xi_one_sub (s : ℂ) : xi (1 - s) = xi s := bys:ℂ⊢ xi (1 - s) = xi s unfold xis:ℂ⊢ 1 / 2 * (1 - s) * (1 - s - 1) * completedRiemannZeta (1 - s) = 1 / 2 * s * (s - 1) * completedRiemannZeta s rw [completedRiemannZeta_one_subs:ℂ⊢ 1 / 2 * (1 - s) * (1 - s - 1) * completedRiemannZeta s = 1 / 2 * s * (s - 1) * completedRiemannZeta s]s:ℂ⊢ 1 / 2 * (1 - s) * (1 - s - 1) * completedRiemannZeta s = 1 / 2 * s * (s - 1) * completedRiemannZeta s ringAll goals completed! 🐙theorem criticalPoint_neg (t : ℝ) : criticalPoint (-t) = 1 - criticalPoint t := byt:ℝ⊢ criticalPoint (-t) = 1 - criticalPoint t simp [criticalPoint]t:ℝ⊢ 2⁻¹ + -(↑t * Complex.I) = 1 - (2⁻¹ + ↑t * Complex.I) ringAll goals completed! 🐙theorem criticalXi_neg (t : ℝ) : criticalXi (-t) = criticalXi t := byt:ℝ⊢ criticalXi (-t) = criticalXi t simp only [criticalXi, criticalPoint_neg, xi_one_sub]All goals completed! 🐙theorem continuous_criticalXi : Continuous criticalXi := by⊢ Continuous criticalXi have hc : Continuous (fun t ↦ completedRiemannZeta (criticalPoint t)) := by apply continuous_iff_continuousAt.mpr⊢ ∀ (x : ℝ), ContinuousAt (fun t => completedRiemannZeta (criticalPoint t)) x intro tt:ℝ⊢ ContinuousAt (fun t => completedRiemannZeta (criticalPoint t)) t exact (differentiableAt_completedZeta (criticalPoint_ne_zero t) (criticalPoint_ne_one t)).continuousAt.comp continuous_criticalPoint.continuousAthc:Continuous fun t => completedRiemannZeta (criticalPoint t)⊢ Continuous criticalXi unfold criticalXi xihc:Continuous fun t => completedRiemannZeta (criticalPoint t)⊢ Continuous fun t => 1 / 2 * criticalPoint t * (criticalPoint t - 1) * completedRiemannZeta (criticalPoint t) exact ((continuous_const.mul continuous_criticalPoint).mul (continuous_criticalPoint.sub continuous_const)).mul hcAll goals completed! 🐙 /-- Exact target of the development; defining this proposition is not proving it. -/def InfinitelyManyCriticalZeros : Prop := Set.Infinite {s : ℂ | s.re = 1 / 2 ∧ riemannZeta s = 0} /-- The stronger positive-ordinate form of Hardy's theorem. -/def ZerosAboveEveryHeight : Prop := ∀ T : ℝ, ∃ t : ℝ, T < t ∧ riemannZeta (criticalPoint t) = 0theorem infinite_criticalZeros_of_zerosAboveEveryHeight (h : ZerosAboveEveryHeight) : InfinitelyManyCriticalZeros := byh:ZerosAboveEveryHeight⊢ InfinitelyManyCriticalZeros intro hfh:ZerosAboveEveryHeighthf:{s | s.re = 1 / 2 ∧ riemannZeta s = 0}.Finite⊢ False have hb := (hf.image Complex.im).bddAboveh:ZerosAboveEveryHeighthf:{s | s.re = 1 / 2 ∧ riemannZeta s = 0}.Finitehb:BddAbove (Complex.im '' {s | s.re = 1 / 2 ∧ riemannZeta s = 0})⊢ False obtain ⟨M, hM⟩ := hbh:ZerosAboveEveryHeighthf:{s | s.re = 1 / 2 ∧ riemannZeta s = 0}.FiniteM:ℝhM:M ∈ upperBounds (Complex.im '' {s | s.re = 1 / 2 ∧ riemannZeta s = 0})⊢ False obtain ⟨t, ht, hz⟩ := h Mh:ZerosAboveEveryHeighthf:{s | s.re = 1 / 2 ∧ riemannZeta s = 0}.FiniteM:ℝhM:M ∈ upperBounds (Complex.im '' {s | s.re = 1 / 2 ∧ riemannZeta s = 0})t:ℝht:M < thz:riemannZeta (criticalPoint t) = 0⊢ False have hmem : (criticalPoint t).im ∈ Complex.im '' {s : ℂ | s.re = 1 / 2 ∧ riemannZeta s = 0} := ⟨criticalPoint t, ⟨criticalPoint_re t, hz⟩, rfl⟩h:ZerosAboveEveryHeighthf:{s | s.re = 1 / 2 ∧ riemannZeta s = 0}.FiniteM:ℝhM:M ∈ upperBounds (Complex.im '' {s | s.re = 1 / 2 ∧ riemannZeta s = 0})t:ℝht:M < thz:riemannZeta (criticalPoint t) = 0hmem:(criticalPoint t).im ∈ Complex.im '' {s | s.re = 1 / 2 ∧ riemannZeta s = 0}⊢ False have := hM hmemh:ZerosAboveEveryHeighthf:{s | s.re = 1 / 2 ∧ riemannZeta s = 0}.FiniteM:ℝhM:M ∈ upperBounds (Complex.im '' {s | s.re = 1 / 2 ∧ riemannZeta s = 0})t:ℝht:M < thz:riemannZeta (criticalPoint t) = 0hmem:(criticalPoint t).im ∈ Complex.im '' {s | s.re = 1 / 2 ∧ riemannZeta s = 0}this:(criticalPoint t).im ≤ M⊢ False simp only [criticalPoint_im] at thish:ZerosAboveEveryHeighthf:{s | s.re = 1 / 2 ∧ riemannZeta s = 0}.FiniteM:ℝhM:M ∈ upperBounds (Complex.im '' {s | s.re = 1 / 2 ∧ riemannZeta s = 0})t:ℝht:M < thz:riemannZeta (criticalPoint t) = 0hmem:(criticalPoint t).im ∈ Complex.im '' {s | s.re = 1 / 2 ∧ riemannZeta s = 0}this:t ≤ M⊢ False exact (not_lt_of_ge this) htAll goals completed! 🐙 end HardyZeta