11.11. HardyZeta.Reality🔗

theorem mellin_conj_of_real_kernel (f : ℝ → ℂ) (hf : ∀ x, conj (f x) = f x) (s : ℂ) : mellin f (conj s) = conj (mellin f s) := byf:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂ⊢ mellin f ((starRingEnd ℂ) s) = (starRingEnd ℂ) (mellin f s) unfold mellinf:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂ⊢ ∫ (t : ℝ) in Ioi 0, ↑t ^ ((starRingEnd ℂ) s - 1) • f t = (starRingEnd ℂ) (∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t) rw [← integral_conjf:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂ⊢ ∫ (t : ℝ) in Ioi 0, ↑t ^ ((starRingEnd ℂ) s - 1) • f t = ∫ (x : ℝ) in Ioi 0, (starRingEnd ℂ) (↑x ^ (s - 1) • f x)]f:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂ⊢ ∫ (t : ℝ) in Ioi 0, ↑t ^ ((starRingEnd ℂ) s - 1) • f t = ∫ (x : ℝ) in Ioi 0, (starRingEnd ℂ) (↑x ^ (s - 1) • f x) apply setIntegral_congr_fun measurableSet_Ioif:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂ⊢ EqOn (fun x => ↑x ^ ((starRingEnd ℂ) s - 1) • f x) (fun x => (starRingEnd ℂ) (↑x ^ (s - 1) • f x)) (Ioi 0) intro x hxf:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂx:ℝhx:x ∈ Ioi 0⊢ (fun x => ↑x ^ ((starRingEnd ℂ) s - 1) • f x) x = (fun x => (starRingEnd ℂ) (↑x ^ (s - 1) • f x)) x have ha : (x : ℂ).arg ≠ Real.pi := byf:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂ⊢ mellin f ((starRingEnd ℂ) s) = (starRingEnd ℂ) (mellin f s) rw [arg_ofReal_of_nonneg (le_of_lt hx)f:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂx:ℝhx:x ∈ Ioi 0⊢ 0 ≠ Real.pi]f:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂx:ℝhx:x ∈ Ioi 0⊢ 0 ≠ Real.pi exact Real.pi_ne_zero.symmf:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂx:ℝhx:x ∈ Ioi 0ha:(↑x).arg ≠ Real.pi⊢ (fun x => ↑x ^ ((starRingEnd ℂ) s - 1) • f x) x = (fun x => (starRingEnd ℂ) (↑x ^ (s - 1) • f x)) x dsimp onlyf:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂx:ℝhx:x ∈ Ioi 0ha:(↑x).arg ≠ Real.pi⊢ ↑x ^ ((starRingEnd ℂ) s - 1) • f x = (starRingEnd ℂ) (↑x ^ (s - 1) • f x) rw [smul_eq_mul,f:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂx:ℝhx:x ∈ Ioi 0ha:(↑x).arg ≠ Real.pi⊢ ↑x ^ ((starRingEnd ℂ) s - 1) * f x = (starRingEnd ℂ) (↑x ^ (s - 1) • f x) smul_eq_mul,f:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂx:ℝhx:x ∈ Ioi 0ha:(↑x).arg ≠ Real.pi⊢ ↑x ^ ((starRingEnd ℂ) s - 1) * f x = (starRingEnd ℂ) (↑x ^ (s - 1) * f x) map_mul,f:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂx:ℝhx:x ∈ Ioi 0ha:(↑x).arg ≠ Real.pi⊢ ↑x ^ ((starRingEnd ℂ) s - 1) * f x = (starRingEnd ℂ) (↑x ^ (s - 1)) * (starRingEnd ℂ) (f x) hff:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂx:ℝhx:x ∈ Ioi 0ha:(↑x).arg ≠ Real.pi⊢ ↑x ^ ((starRingEnd ℂ) s - 1) * f x = (starRingEnd ℂ) (↑x ^ (s - 1)) * f x]f:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂx:ℝhx:x ∈ Ioi 0ha:(↑x).arg ≠ Real.pi⊢ ↑x ^ ((starRingEnd ℂ) s - 1) * f x = (starRingEnd ℂ) (↑x ^ (s - 1)) * f x congr 1e_af:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂx:ℝhx:x ∈ Ioi 0ha:(↑x).arg ≠ Real.pi⊢ ↑x ^ ((starRingEnd ℂ) s - 1) = (starRingEnd ℂ) (↑x ^ (s - 1)) have hc := cpow_conj (x : ℂ) (s - 1) hae_af:ℝ → ℂhf:∀ (x : ℝ), (starRingEnd ℂ) (f x) = f xs:ℂx:ℝhx:x ∈ Ioi 0ha:(↑x).arg ≠ Real.pihc:↑x ^ (starRingEnd ℂ) (s - 1) = (starRingEnd ℂ) ((starRingEnd ℂ) ↑x ^ (s - 1))⊢ ↑x ^ ((starRingEnd ℂ) s - 1) = (starRingEnd ℂ) (↑x ^ (s - 1)) simpa using hcAll goals completed! 🐙theorem modifiedTheta_conj (x : ℝ) : conj ((HurwitzZeta.hurwitzEvenFEPair 0).f_modif x) = (HurwitzZeta.hurwitzEvenFEPair 0).f_modif x := byx:ℝ⊢ (starRingEnd ℂ) ((HurwitzZeta.hurwitzEvenFEPair 0).f_modif x) = (HurwitzZeta.hurwitzEvenFEPair 0).f_modif x simp only [WeakFEPair.f_modif, Pi.add_apply]x:ℝ⊢ (starRingEnd ℂ) ((Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x) = (Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x by_cases h₁ : x ∈ Ioi (1 : ℝ)posx:ℝh₁:x ∈ Ioi 1⊢ (starRingEnd ℂ) ((Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x) = (Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) xnegx:ℝh₁:x ∉ Ioi 1⊢ (starRingEnd ℂ) ((Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x) = (Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x <;>posx:ℝh₁:x ∈ Ioi 1⊢ (starRingEnd ℂ) ((Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x) = (Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) xnegx:ℝh₁:x ∉ Ioi 1⊢ (starRingEnd ℂ) ((Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x) = (Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x by_cases h₂ : x ∈ Ioo (0 : ℝ) 1posx:ℝh₁:x ∉ Ioi 1h₂:x ∈ Ioo 0 1⊢ (starRingEnd ℂ) ((Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x) = (Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) xnegx:ℝh₁:x ∉ Ioi 1h₂:x ∉ Ioo 0 1⊢ (starRingEnd ℂ) ((Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x) = (Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x <;>posx:ℝh₁:x ∈ Ioi 1h₂:x ∈ Ioo 0 1⊢ (starRingEnd ℂ) ((Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x) = (Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) xnegx:ℝh₁:x ∈ Ioi 1h₂:x ∉ Ioo 0 1⊢ (starRingEnd ℂ) ((Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x) = (Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) xposx:ℝh₁:x ∉ Ioi 1h₂:x ∈ Ioo 0 1⊢ (starRingEnd ℂ) ((Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x) = (Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) xnegx:ℝh₁:x ∉ Ioi 1h₂:x ∉ Ioo 0 1⊢ (starRingEnd ℂ) ((Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x) = (Ioi 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - (HurwitzZeta.hurwitzEvenFEPair 0).f₀) x + (Ioo 0 1).indicator (fun x => (HurwitzZeta.hurwitzEvenFEPair 0).f x - ((HurwitzZeta.hurwitzEvenFEPair 0).ε * ↑(x ^ (-(HurwitzZeta.hurwitzEvenFEPair 0).k))) • (HurwitzZeta.hurwitzEvenFEPair 0).g₀) x simp [h₁, h₂, HurwitzZeta.hurwitzEvenFEPair, smul_eq_mul]All goals completed! 🐙theorem completedZeta₀_conj (s : ℂ) : completedRiemannZeta₀ (conj s) = conj (completedRiemannZeta₀ s) := bys:ℂ⊢ completedRiemannZeta₀ ((starRingEnd ℂ) s) = (starRingEnd ℂ) (completedRiemannZeta₀ s) unfold completedRiemannZeta₀ HurwitzZeta.completedHurwitzZetaEven₀ WeakFEPair.Λ₀s:ℂ⊢ mellin (HurwitzZeta.hurwitzEvenFEPair 0).f_modif ((starRingEnd ℂ) s / 2) / 2 = (starRingEnd ℂ) (mellin (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (s / 2) / 2) rw [show conj s / 2 = conj (s / 2) bys:ℂ⊢ completedRiemannZeta₀ ((starRingEnd ℂ) s) = (starRingEnd ℂ) (completedRiemannZeta₀ s) simp [map_ofNat]All goals completed! 🐙]s:ℂ⊢ mellin (HurwitzZeta.hurwitzEvenFEPair 0).f_modif ((starRingEnd ℂ) (s / 2)) / 2 = (starRingEnd ℂ) (mellin (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (s / 2) / 2) rw [mellin_conj_of_real_kernel _ modifiedTheta_conjs:ℂ⊢ (starRingEnd ℂ) (mellin (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (s / 2)) / 2 = (starRingEnd ℂ) (mellin (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (s / 2) / 2)]s:ℂ⊢ (starRingEnd ℂ) (mellin (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (s / 2)) / 2 = (starRingEnd ℂ) (mellin (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (s / 2) / 2) simp [map_ofNat]All goals completed! 🐙theorem completedZeta_conj (s : ℂ) : completedRiemannZeta (conj s) = conj (completedRiemannZeta s) := bys:ℂ⊢ completedRiemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (completedRiemannZeta s) simp [completedRiemannZeta_eq, completedZeta₀_conj]All goals completed! 🐙theorem xi_conj (s : ℂ) : xi (conj s) = conj (xi s) := bys:ℂ⊢ xi ((starRingEnd ℂ) s) = (starRingEnd ℂ) (xi s) simp [xi, completedZeta_conj, map_ofNat]All goals completed! 🐙theorem conj_criticalPoint (t : ℝ) : conj (criticalPoint t) = 1 - criticalPoint t := byt:ℝ⊢ (starRingEnd ℂ) (criticalPoint t) = 1 - criticalPoint t simp [criticalPoint, map_ofNat]t:ℝ⊢ 2⁻¹ + -(↑t * I) = 1 - (2⁻¹ + ↑t * I) ringAll goals completed! 🐙theorem criticalXi_conj (t : ℝ) : conj (criticalXi t) = criticalXi t := byt:ℝ⊢ (starRingEnd ℂ) (criticalXi t) = criticalXi t rw [criticalXi,t:ℝ⊢ (starRingEnd ℂ) (xi (criticalPoint t)) = xi (criticalPoint t) ← xi_conj,t:ℝ⊢ xi ((starRingEnd ℂ) (criticalPoint t)) = xi (criticalPoint t) conj_criticalPoint,t:ℝ⊢ xi (1 - criticalPoint t) = xi (criticalPoint t) xi_one_subt:ℝ⊢ xi (criticalPoint t) = xi (criticalPoint t)]All goals completed! 🐙 /-- The restriction of xi to the critical line is genuinely real. -/theorem criticalXi_im (t : ℝ) : (criticalXi t).im = 0 := byt:ℝ⊢ (criticalXi t).im = 0 have h := congrArg Complex.im (criticalXi_conj t)t:ℝh:((starRingEnd ℂ) (criticalXi t)).im = (criticalXi t).im⊢ (criticalXi t).im = 0 simp only [conj_im] at ht:ℝh:-(criticalXi t).im = (criticalXi t).im⊢ (criticalXi t).im = 0 linarithAll goals completed! 🐙 /-- Hardy's real xi function. -/def hardyXi (t : ℝ) : ℝ := (criticalXi t).retheorem ofReal_hardyXi (t : ℝ) : (hardyXi t : ℂ) = criticalXi t := byt:ℝ⊢ ↑(hardyXi t) = criticalXi t apply Complex.extat:ℝ⊢ (↑(hardyXi t)).re = (criticalXi t).reat:ℝ⊢ (↑(hardyXi t)).im = (criticalXi t).im <;>at:ℝ⊢ (↑(hardyXi t)).re = (criticalXi t).reat:ℝ⊢ (↑(hardyXi t)).im = (criticalXi t).im simp [hardyXi, criticalXi_im]All goals completed! 🐙theorem hardyXi_eq_zero_iff (t : ℝ) : hardyXi t = 0 ↔ riemannZeta (criticalPoint t) = 0 := byt:ℝ⊢ hardyXi t = 0 ↔ riemannZeta (criticalPoint t) = 0 rw [← criticalXi_eq_zero_iff,t:ℝ⊢ hardyXi t = 0 ↔ criticalXi t = 0 ← ofReal_hardyXit:ℝ⊢ hardyXi t = 0 ↔ ↑(hardyXi t) = 0]t:ℝ⊢ hardyXi t = 0 ↔ ↑(hardyXi t) = 0 exact Complex.ofReal_eq_zero.symmAll goals completed! 🐙theorem continuous_hardyXi : Continuous hardyXi := Complex.continuous_re.comp continuous_criticalXitheorem hardyXi_neg (t : ℝ) : hardyXi (-t) = hardyXi t := byt:ℝ⊢ hardyXi (-t) = hardyXi t simp [hardyXi, criticalXi_neg]All goals completed! 🐙 end HardyZeta