11.7. HardyZeta.Hardy🔗

theorem not_eventually_positive_hardyWeight_mul (c : ℝ) {T : ℝ} (hT : 0 < T) (hpos : ∀ t > T, 0 < c * hardyWeight t) : False := byc:ℝT:ℝhT:0 < Thpos:∀ t > T, 0 < c * hardyWeight t⊢ False apply not_positive_tail_of_vanishing_differences (continuous_hardyWeight.const_mul c) hT hposhic:ℝT:ℝhT:0 < Thpos:∀ t > T, 0 < c * hardyWeight t⊢ ∀ (k : ℕ), ∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => c * hardyWeight t * normalizedHardyKernel (k + 1) h t) (Ioi 0) volumehlc:ℝT:ℝhT:0 < Thpos:∀ t > T, 0 < c * hardyWeight t⊢ ∀ (k : ℕ), Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, c * hardyWeight t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0) ·hic:ℝT:ℝhT:0 < Thpos:∀ t > T, 0 < c * hardyWeight t⊢ ∀ (k : ℕ), ∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => c * hardyWeight t * normalizedHardyKernel (k + 1) h t) (Ioi 0) volume intro khic:ℝT:ℝhT:0 < Thpos:∀ t > T, 0 < c * hardyWeight tk:ℕ⊢ ∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => c * hardyWeight t * normalizedHardyKernel (k + 1) h t) (Ioi 0) volume filter_upwards [eventually_difference_center_inside (byc:ℝT:ℝhT:0 < Thpos:∀ t > T, 0 < c * hardyWeight tk:ℕ⊢ 0 < Real.pi / 4 positivityAll goals completed! 🐙 : (0 : ℝ) < Real.pi / 4) (k + 1)] with h hhc:ℝT:ℝhT:0 < Thpos:∀ t > T, 0 < c * hardyWeight tk:ℕh:ℝhh:|Real.pi / 4 - (↑(k + 1) + 1) * h| + ↑(k + 1) * |h| < Real.pi / 4⊢ IntegrableOn (fun t => c * hardyWeight t * normalizedHardyKernel (k + 1) h t) (Ioi 0) volume simpa only [IntegrableOn, mul_assoc] using (integrableOn_normalizedHardyKernel (k + 1) h hh).const_mul cAll goals completed! 🐙 ·hlc:ℝT:ℝhT:0 < Thpos:∀ t > T, 0 < c * hardyWeight t⊢ ∀ (k : ℕ), Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, c * hardyWeight t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0) intro khlc:ℝT:ℝhT:0 < Thpos:∀ t > T, 0 < c * hardyWeight tk:ℕ⊢ Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, c * hardyWeight t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0) have hl := (tendsto_normalizedHardyIntegral k).const_mul chlc:ℝT:ℝhT:0 < Thpos:∀ t > T, 0 < c * hardyWeight tk:ℕhl:Tendsto (fun x => c * ∫ (t : ℝ) in Ioi 0, hardyWeight t * normalizedHardyKernel (k + 1) x t) (𝓝[>] 0) (𝓝 (c * 0))⊢ Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, c * hardyWeight t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0) simpa only [mul_zero, ← integral_const_mul, mul_assoc] using hlAll goals completed! 🐙 /-- The actual zeta function has a critical-line zero above every real height. -/theorem zerosAboveEveryHeight : ZerosAboveEveryHeight := by⊢ ZerosAboveEveryHeight by_contra hh:¬ZerosAboveEveryHeight⊢ False obtain ⟨T, hT, hp | hn⟩ := eventual_sign_of_not_zerosAboveEveryHeight hinlh:¬ZerosAboveEveryHeightT:ℝhT:0 < Thp:∀ (t : ℝ), T < t → 0 < hardyXi t⊢ Falseinrh:¬ZerosAboveEveryHeightT:ℝhT:0 < Thn:∀ (t : ℝ), T < t → hardyXi t < 0⊢ False ·inlh:¬ZerosAboveEveryHeightT:ℝhT:0 < Thp:∀ (t : ℝ), T < t → 0 < hardyXi t⊢ False apply not_eventually_positive_hardyWeight_mul 1 hTinlh:¬ZerosAboveEveryHeightT:ℝhT:0 < Thp:∀ (t : ℝ), T < t → 0 < hardyXi t⊢ ∀ t > T, 0 < 1 * hardyWeight t intro t htinlh:¬ZerosAboveEveryHeightT:ℝhT:0 < Thp:∀ (t : ℝ), T < t → 0 < hardyXi tt:ℝht:t > T⊢ 0 < 1 * hardyWeight t simp only [one_mul, hardyWeight]inlh:¬ZerosAboveEveryHeightT:ℝhT:0 < Thp:∀ (t : ℝ), T < t → 0 < hardyXi tt:ℝht:t > T⊢ 0 < hardyXi t / (t ^ 2 + 1 / 4) exact div_pos (hp t ht) (byh:¬ZerosAboveEveryHeightT:ℝhT:0 < Thp:∀ (t : ℝ), T < t → 0 < hardyXi tt:ℝht:t > T⊢ 0 < t ^ 2 + 1 / 4 positivityAll goals completed! 🐙) ·inrh:¬ZerosAboveEveryHeightT:ℝhT:0 < Thn:∀ (t : ℝ), T < t → hardyXi t < 0⊢ False apply not_eventually_positive_hardyWeight_mul (-1) hTinrh:¬ZerosAboveEveryHeightT:ℝhT:0 < Thn:∀ (t : ℝ), T < t → hardyXi t < 0⊢ ∀ t > T, 0 < -1 * hardyWeight t intro t htinrh:¬ZerosAboveEveryHeightT:ℝhT:0 < Thn:∀ (t : ℝ), T < t → hardyXi t < 0t:ℝht:t > T⊢ 0 < -1 * hardyWeight t simp only [neg_one_mul, hardyWeight, neg_pos]inrh:¬ZerosAboveEveryHeightT:ℝhT:0 < Thn:∀ (t : ℝ), T < t → hardyXi t < 0t:ℝht:t > T⊢ hardyXi t / (t ^ 2 + 1 / 4) < 0 exact div_neg_of_neg_of_pos (hn t ht) (byh:¬ZerosAboveEveryHeightT:ℝhT:0 < Thn:∀ (t : ℝ), T < t → hardyXi t < 0t:ℝht:t > T⊢ 0 < t ^ 2 + 1 / 4 positivityAll goals completed! 🐙) /-- Infinitely many zeros of Riemann zeta lie on the critical line. -/theorem hardy : Set.Infinite {s : ℂ | s.re = 1 / 2 ∧ riemannZeta s = 0} := by⊢ {s | s.re = 1 / 2 ∧ riemannZeta s = 0}.Infinite exact infinite_criticalZeros_of_zerosAboveEveryHeight zerosAboveEveryHeightAll goals completed! 🐙