Hardy zeta

11.18. HardyZeta.ThetaInversion🔗

theorem fourier_theta_horizontal_eq_integral (b w : ℝ) : 𝓕 (fun u : ℝ ↦ thetaLogKernel ((u : ℂ) + b * I)) w = ∫ u : ℝ, exp (-I * (2 * Real.pi * w : ℝ) * (u : ℂ)) * thetaLogKernel ((u : ℂ) + b * I) := b:ℝw:ℝ⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ∫ (u : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel (↑u + ↑b * I) b:ℝw:ℝ⊢ ∫ (v : ℝ), cexp (↑(-2 * Real.pi * inner ℝ v w) * I) • thetaLogKernel (↑v + ↑b * I) = ∫ (u : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel (↑u + ↑b * I) b:ℝw:ℝ⊢ (fun a => cexp (↑(-2 * Real.pi * inner ℝ a w) * I) • thetaLogKernel (↑a + ↑b * I)) =ᵐ[volume] fun a => cexp (-I * ↑(2 * Real.pi * w) * ↑a) * thetaLogKernel (↑a + ↑b * I) b:ℝw:ℝu:ℝ⊢ cexp (↑(-2 * Real.pi * inner ℝ u w) * I) • thetaLogKernel (↑u + ↑b * I) = cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel (↑u + ↑b * I) b:ℝw:ℝu:ℝ⊢ cexp (↑(-2 * Real.pi * (w * u)) * I) * thetaLogKernel (↑u + ↑b * I) = cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel (↑u + ↑b * I) b:ℝw:ℝu:ℝ⊢ ↑(-2 * Real.pi * (w * u)) * I = -I * ↑(2 * Real.pi * w) * ↑u b:ℝw:ℝu:ℝ⊢ -2 * ↑Real.pi * (↑w * ↑u) * I = -I * (2 * ↑Real.pi * ↑w) * ↑u All goals completed! 🐙theorem thetaFourierIntegrand_horizontal (t u b : ℝ) : thetaFourierIntegrand t ((u : ℂ) + b * I) = (Real.exp (t * b) : ℂ) * (exp (-I * (t : ℂ) * (u : ℂ)) * thetaLogKernel ((u : ℂ) + b * I)) := t:ℝu:ℝb:ℝ⊢ thetaFourierIntegrand t (↑u + ↑b * I) = ↑(Real.exp (t * b)) * (cexp (-I * ↑t * ↑u) * thetaLogKernel (↑u + ↑b * I)) t:ℝu:ℝb:ℝ⊢ cexp (-I * ↑t * (↑u + ↑b * I)) * thetaLogKernel (↑u + ↑b * I) = ↑(Real.exp (t * b)) * (cexp (-I * ↑t * ↑u) * thetaLogKernel (↑u + ↑b * I)) t:ℝu:ℝb:ℝ⊢ cexp (-I * ↑t * (↑u + ↑b * I)) * thetaLogKernel (↑u + ↑b * I) = cexp ↑(t * b) * (cexp (-I * ↑t * ↑u) * thetaLogKernel (↑u + ↑b * I)) conv_rhs => t:ℝu:ℝb:ℝ| cexp (↑(t * b) + -I * ↑t * ↑u) * thetaLogKernel (↑u + ↑b * I) t:ℝu:ℝb:ℝ⊢ -I * ↑t * (↑u + ↑b * I) = ↑(t * b) + -I * ↑t * ↑u t:ℝu:ℝb:ℝ⊢ -I * ↑t * (↑u + ↑b * I) = ↑t * ↑b + -I * ↑t * ↑u t:ℝu:ℝb:ℝ⊢ -(I * ↑t * ↑u) - I ^ 2 * ↑t * ↑b = -(I * ↑t * ↑u) + ↑t * ↑b All goals completed! 🐙theorem fourier_theta_horizontal (w : ℝ) {b : ℝ} (hb : |b| < Real.pi / 2) : 𝓕 (fun u : ℝ ↦ thetaLogKernel ((u : ℂ) + b * I)) w = (Real.exp (-2 * Real.pi * w * b) : ℂ) * 𝓕 (fun u : ℝ ↦ thetaLogKernel (u : ℂ)) w := w:ℝb:ℝhb:|b| < Real.pi / 2⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ↑(Real.exp (-2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel ↑u) w w:ℝb:ℝhb:|b| < Real.pi / 2h:∫ (u : ℝ), thetaFourierIntegrand (2 * Real.pi * w) ↑u = ∫ (u : ℝ), thetaFourierIntegrand (2 * Real.pi * w) (↑u + ↑b * I)⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ↑(Real.exp (-2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel ↑u) w simp_rw w:ℝb:ℝhb:|b| < Real.pi / 2h:∫ (u : ℝ), thetaFourierIntegrand (2 * Real.pi * w) ↑u = ∫ (u : ℝ), thetaFourierIntegrand (2 * Real.pi * w) (↑u + ↑b * I)⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ↑(Real.exp (-2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel ↑u) ww:ℝb:ℝhb:|b| < Real.pi / 2h:∫ (u : ℝ), thetaFourierIntegrand (2 * Real.pi * w) ↑u = ∫ (u : ℝ), ↑(Real.exp (2 * Real.pi * w * b)) * (cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel (↑u + ↑b * I))⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ↑(Real.exp (-2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel ↑u) w w:ℝb:ℝhb:|b| < Real.pi / 2h:∫ (u : ℝ), thetaFourierIntegrand (2 * Real.pi * w) ↑u = ↑(Real.exp (2 * Real.pi * w * b)) * ∫ (a : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑a) * thetaLogKernel (↑a + ↑b * I)⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ↑(Real.exp (-2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel ↑u) w] at h w:ℝb:ℝhb:|b| < Real.pi / 2h:∫ (u : ℝ), thetaFourierIntegrand (2 * Real.pi * w) ↑u = ↑(Real.exp (2 * Real.pi * w * b)) * ∫ (a : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑a) * thetaLogKernel (↑a + ↑b * I)h0:𝓕 (fun u => thetaLogKernel (↑u + ↑0 * I)) w = ∫ (u : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel (↑u + ↑0 * I)⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ↑(Real.exp (-2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel ↑u) w w:ℝb:ℝhb:|b| < Real.pi / 2h:∫ (u : ℝ), thetaFourierIntegrand (2 * Real.pi * w) ↑u = ↑(Real.exp (2 * Real.pi * w * b)) * ∫ (a : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑a) * thetaLogKernel (↑a + ↑b * I)h0:𝓕 (fun u => thetaLogKernel ↑u) w = ∫ (u : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel ↑u⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ↑(Real.exp (-2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel ↑u) w w:ℝb:ℝhb:|b| < Real.pi / 2h:∫ (u : ℝ), thetaFourierIntegrand (2 * Real.pi * w) ↑u = ↑(Real.exp (2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) wh0:𝓕 (fun u => thetaLogKernel ↑u) w = ∫ (u : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel ↑u⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ↑(Real.exp (-2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel ↑u) w w:ℝb:ℝhb:|b| < Real.pi / 2h0:𝓕 (fun u => thetaLogKernel ↑u) w = ∫ (u : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel ↑uh:∫ (u : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel ↑u = ↑(Real.exp (2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ↑(Real.exp (-2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel ↑u) w w:ℝb:ℝhb:|b| < Real.pi / 2h0:𝓕 (fun u => thetaLogKernel ↑u) w = ∫ (u : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel ↑uh:𝓕 (fun u => thetaLogKernel ↑u) w = ↑(Real.exp (2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ↑(Real.exp (-2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel ↑u) w w:ℝb:ℝhb:|b| < Real.pi / 2h0:𝓕 (fun u => thetaLogKernel ↑u) w = ∫ (u : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel ↑uh:𝓕 (fun u => thetaLogKernel ↑u) w = ↑(Real.exp (2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ↑(Real.exp (-2 * Real.pi * w * b + 2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w w:ℝb:ℝhb:|b| < Real.pi / 2h0:𝓕 (fun u => thetaLogKernel ↑u) w = ∫ (u : ℝ), cexp (-I * ↑(2 * Real.pi * w) * ↑u) * thetaLogKernel ↑uh:𝓕 (fun u => thetaLogKernel ↑u) w = ↑(Real.exp (2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) whe:-2 * Real.pi * w * b + 2 * Real.pi * w * b = 0⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = ↑(Real.exp (-2 * Real.pi * w * b + 2 * Real.pi * w * b)) * 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w All goals completed! 🐙theorem fourier_theta_eq_hardyWeight (w : ℝ) : 𝓕 (fun u : ℝ ↦ thetaLogKernel (u : ℂ)) w = -4 * (hardyWeight (4 * Real.pi * w) : ℂ) := w:ℝ⊢ 𝓕 (fun u => thetaLogKernel ↑u) w = -4 * ↑(hardyWeight (4 * Real.pi * w)) w:ℝh:completedRiemannZeta (criticalPoint (4 * Real.pi * w)) = 𝓕 (fun u => thetaLogKernel ↑u) (4 * Real.pi * w / (4 * Real.pi)) / 2⊢ 𝓕 (fun u => thetaLogKernel ↑u) w = -4 * ↑(hardyWeight (4 * Real.pi * w)) w:ℝh:completedRiemannZeta (criticalPoint (4 * Real.pi * w)) = 𝓕 (fun u => thetaLogKernel ↑u) (4 * Real.pi * w / (4 * Real.pi)) / 2he:4 * Real.pi * w / (4 * Real.pi) = w⊢ 𝓕 (fun u => thetaLogKernel ↑u) w = -4 * ↑(hardyWeight (4 * Real.pi * w)) w:ℝh:completedRiemannZeta (criticalPoint (4 * Real.pi * w)) = 𝓕 (fun u => thetaLogKernel ↑u) w / 2he:4 * Real.pi * w / (4 * Real.pi) = w⊢ 𝓕 (fun u => thetaLogKernel ↑u) w = -4 * ↑(hardyWeight (4 * Real.pi * w)) w:ℝh:completedRiemannZeta (criticalPoint (4 * Real.pi * w)) = 𝓕 (fun u => thetaLogKernel ↑u) w / 2he:4 * Real.pi * w / (4 * Real.pi) = w⊢ 𝓕 (fun u => thetaLogKernel ↑u) w = -4 * (-(𝓕 (fun u => thetaLogKernel ↑u) w / 2) / 2) All goals completed! 🐙theorem fourier_theta_horizontal_eq_weight (w : ℝ) {b : ℝ} (hb : |b| < Real.pi / 2) : 𝓕 (fun u : ℝ ↦ thetaLogKernel ((u : ℂ) + b * I)) w = -4 * ((hardyWeight (4 * Real.pi * w) * Real.exp ((-b / 2) * (4 * Real.pi * w)) : ℝ) : ℂ) := w:ℝb:ℝhb:|b| < Real.pi / 2⊢ 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = -4 * ↑(hardyWeight (4 * Real.pi * w) * Real.exp (-b / 2 * (4 * Real.pi * w))) w:ℝb:ℝhb:|b| < Real.pi / 2⊢ ↑(Real.exp (-2 * Real.pi * w * b)) * (-4 * ↑(hardyWeight (4 * Real.pi * w))) = -4 * ↑(hardyWeight (4 * Real.pi * w) * Real.exp (-b / 2 * (4 * Real.pi * w))) w:ℝb:ℝhb:|b| < Real.pi / 2he:-2 * Real.pi * w * b = -b / 2 * (4 * Real.pi * w)⊢ ↑(Real.exp (-2 * Real.pi * w * b)) * (-4 * ↑(hardyWeight (4 * Real.pi * w))) = -4 * ↑(hardyWeight (4 * Real.pi * w) * Real.exp (-b / 2 * (4 * Real.pi * w))) w:ℝb:ℝhb:|b| < Real.pi / 2he:-2 * Real.pi * w * b = -b / 2 * (4 * Real.pi * w)⊢ ↑(Real.exp (-b / 2 * (4 * Real.pi * w))) * (-4 * ↑(hardyWeight (4 * Real.pi * w))) = -4 * ↑(hardyWeight (4 * Real.pi * w) * Real.exp (-b / 2 * (4 * Real.pi * w))) w:ℝb:ℝhb:|b| < Real.pi / 2he:-2 * Real.pi * w * b = -b / 2 * (4 * Real.pi * w)⊢ cexp (-↑b / 2 * (4 * ↑Real.pi * ↑w)) * (-4 * ↑(hardyWeight (4 * Real.pi * w))) = -4 * (↑(hardyWeight (4 * Real.pi * w)) * cexp (-↑b / 2 * (4 * ↑Real.pi * ↑w))) All goals completed! 🐙theorem integrable_fourier_theta_horizontal {b : ℝ} (hb : |b| < Real.pi / 2) : Integrable (𝓕 (fun u : ℝ ↦ thetaLogKernel ((u : ℂ) + b * I))) := b:ℝhb:|b| < Real.pi / 2⊢ Integrable (𝓕 fun u => thetaLogKernel (↑u + ↑b * I)) volume b:ℝhb:|b| < Real.pi / 2ha:|-b / 2| < Real.pi / 4⊢ Integrable (𝓕 fun u => thetaLogKernel (↑u + ↑b * I)) volume b:ℝhb:|b| < Real.pi / 2ha:|-b / 2| < Real.pi / 4h:Integrable (fun x => ↑(hardyWeight (x * (4 * Real.pi)) * Real.exp (-b / 2 * (x * (4 * Real.pi))))) volume⊢ Integrable (𝓕 fun u => thetaLogKernel (↑u + ↑b * I)) volume b:ℝhb:|b| < Real.pi / 2ha:|-b / 2| < Real.pi / 4h:Integrable (fun x => ↑(hardyWeight (x * (4 * Real.pi)) * Real.exp (-b / 2 * (x * (4 * Real.pi))))) volumeh':Integrable (fun x => -4 * ↑(hardyWeight (x * (4 * Real.pi)) * Real.exp (-b / 2 * (x * (4 * Real.pi))))) volume⊢ Integrable (𝓕 fun u => thetaLogKernel (↑u + ↑b * I)) volume b:ℝhb:|b| < Real.pi / 2ha:|-b / 2| < Real.pi / 4h:Integrable (fun x => ↑(hardyWeight (x * (4 * Real.pi)) * Real.exp (-b / 2 * (x * (4 * Real.pi))))) volumeh':Integrable (fun x => -4 * ↑(hardyWeight (x * (4 * Real.pi)) * Real.exp (-b / 2 * (x * (4 * Real.pi))))) volume⊢ (fun x => -4 * ↑(hardyWeight (x * (4 * Real.pi)) * Real.exp (-b / 2 * (x * (4 * Real.pi))))) =ᵐ[volume] 𝓕 fun u => thetaLogKernel (↑u + ↑b * I) b:ℝhb:|b| < Real.pi / 2ha:|-b / 2| < Real.pi / 4h:Integrable (fun x => ↑(hardyWeight (x * (4 * Real.pi)) * Real.exp (-b / 2 * (x * (4 * Real.pi))))) volumeh':Integrable (fun x => -4 * ↑(hardyWeight (x * (4 * Real.pi)) * Real.exp (-b / 2 * (x * (4 * Real.pi))))) volumew:ℝ⊢ -4 * ↑(hardyWeight (w * (4 * Real.pi)) * Real.exp (-b / 2 * (w * (4 * Real.pi)))) = 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w b:ℝhb:|b| < Real.pi / 2ha:|-b / 2| < Real.pi / 4h:Integrable (fun x => ↑(hardyWeight (x * (4 * Real.pi)) * Real.exp (-b / 2 * (x * (4 * Real.pi))))) volumeh':Integrable (fun x => -4 * ↑(hardyWeight (x * (4 * Real.pi)) * Real.exp (-b / 2 * (x * (4 * Real.pi))))) volumew:ℝ⊢ -4 * ↑(hardyWeight (w * (4 * Real.pi)) * Real.exp (-b / 2 * (w * (4 * Real.pi)))) = -4 * ↑(hardyWeight (4 * Real.pi * w) * Real.exp (-b / 2 * (4 * Real.pi * w))) b:ℝhb:|b| < Real.pi / 2ha:|-b / 2| < Real.pi / 4h:Integrable (fun x => ↑(hardyWeight (x * (4 * Real.pi)) * Real.exp (-b / 2 * (x * (4 * Real.pi))))) volumeh':Integrable (fun x => -4 * ↑(hardyWeight (x * (4 * Real.pi)) * Real.exp (-b / 2 * (x * (4 * Real.pi))))) volumew:ℝ⊢ -4 * ↑(hardyWeight (4 * Real.pi * w) * Real.exp (-b / 2 * (4 * Real.pi * w))) = -4 * ↑(hardyWeight (4 * Real.pi * w) * Real.exp (-b / 2 * (4 * Real.pi * w))) All goals completed! 🐙 /-- Inversion at the origin on any interior horizontal line. -/theorem integral_fourier_theta_horizontal {b : ℝ} (hb : |b| < Real.pi / 2) : (∫ w : ℝ, 𝓕 (fun u : ℝ ↦ thetaLogKernel ((u : ℂ) + b * I)) w) = thetaLogKernel (b * I) := b:ℝhb:|b| < Real.pi / 2⊢ ∫ (w : ℝ), 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = thetaLogKernel (↑b * I) b:ℝhb:|b| < Real.pi / 2hc:ContinuousAt (fun u => thetaLogKernel (↑u + ↑b * I)) 0⊢ ∫ (w : ℝ), 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = thetaLogKernel (↑b * I) b:ℝhb:|b| < Real.pi / 2hc:ContinuousAt (fun u => thetaLogKernel (↑u + ↑b * I)) 0h:𝓕⁻ (𝓕 fun u => thetaLogKernel (↑u + ↑b * I)) 0 = thetaLogKernel (↑0 + ↑b * I)⊢ ∫ (w : ℝ), 𝓕 (fun u => thetaLogKernel (↑u + ↑b * I)) w = thetaLogKernel (↑b * I) All goals completed! 🐙 /-- Evaluation of the actual exponentially weighted Hardy integral. -/theorem integral_hardyWeight_exp {α : ℝ} (hα : |α| < Real.pi / 4) : (∫ t : ℝ, ((hardyWeight t * Real.exp (α * t) : ℝ) : ℂ)) = -(Real.pi : ℂ) * thetaLogKernel ((-2 * α : ℝ) * I) := α:ℝhα:|α| < Real.pi / 4⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2h:∫ (w : ℝ), 𝓕 (fun u => thetaLogKernel (↑u + ↑(-2 * α) * I)) w = thetaLogKernel (↑(-2 * α) * I)⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) simp_rw α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2h:∫ (w : ℝ), 𝓕 (fun u => thetaLogKernel (↑u + ↑(-2 * α) * I)) w = thetaLogKernel (↑(-2 * α) * I)⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2h:∫ (w : ℝ), -4 * ↑(hardyWeight (4 * Real.pi * w) * Real.exp (-(-2 * α) / 2 * (4 * Real.pi * w))) = thetaLogKernel (↑(-2 * α) * I)⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)] at h α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2h:-4 * ∫ (a : ℝ), ↑(hardyWeight (4 * Real.pi * a) * Real.exp (-(-2 * α) / 2 * (4 * Real.pi * a))) = thetaLogKernel (↑(-2 * α) * I)⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2h:-4 * ∫ (a : ℝ), ↑(hardyWeight (4 * Real.pi * a) * Real.exp (-(-2 * α) / 2 * (4 * Real.pi * a))) = thetaLogKernel (↑(-2 * α) * I)he:-(-2 * α) / 2 = α⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) simp_rw α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2h:-4 * ∫ (a : ℝ), ↑(hardyWeight (4 * Real.pi * a) * Real.exp (-(-2 * α) / 2 * (4 * Real.pi * a))) = thetaLogKernel (↑(-2 * α) * I)he:-(-2 * α) / 2 = α⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2he:-(-2 * α) / 2 = αh:-4 * ∫ (a : ℝ), ↑(hardyWeight (4 * Real.pi * a) * Real.exp (α * (4 * Real.pi * a))) = thetaLogKernel (↑(-2 * α) * I)⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)] at h α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2he:-(-2 * α) / 2 = αh:-4 * |(4 * Real.pi)⁻¹| • ∫ (y : ℝ), ↑(hardyWeight y * Real.exp (α * y)) = thetaLogKernel (↑(-2 * α) * I)⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2he:-(-2 * α) / 2 = αh:-4 * (↑(4 * Real.pi)⁻¹ * ∫ (y : ℝ), ↑(hardyWeight y * Real.exp (α * y))) = thetaLogKernel (↑(-2 * α) * I)⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2he:-(-2 * α) / 2 = αh:-4 * (↑(4 * Real.pi)⁻¹ * ∫ (y : ℝ), ↑(hardyWeight y * Real.exp (α * y))) = thetaLogKernel (↑(-2 * α) * I)hpi:↑Real.pi ≠ 0⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2he:-(-2 * α) / 2 = αhpi:↑Real.pi ≠ 0h:-4 * ((4 * ↑Real.pi)⁻¹ * ∫ (y : ℝ), ↑(hardyWeight y) * cexp (↑α * ↑y)) = thetaLogKernel (-2 * ↑α * I)⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2he:-(-2 * α) / 2 = αhpi:↑Real.pi ≠ 0h:-4 * ((4 * ↑Real.pi)⁻¹ * ∫ (y : ℝ), ↑(hardyWeight y) * cexp (↑α * ↑y)) = thetaLogKernel (-2 * ↑α * I)h':-↑Real.pi * (-4 * ((4 * ↑Real.pi)⁻¹ * ∫ (y : ℝ), ↑(hardyWeight y) * cexp (↑α * ↑y))) = -↑Real.pi * thetaLogKernel (-2 * ↑α * I)⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2he:-(-2 * α) / 2 = αhpi:↑Real.pi ≠ 0h:-4 * ((4 * ↑Real.pi)⁻¹ * ∫ (y : ℝ), ↑(hardyWeight y) * cexp (↑α * ↑y)) = thetaLogKernel (-2 * ↑α * I)h':∫ (y : ℝ), ↑(hardyWeight y) * cexp (↑α * ↑y) = -(↑Real.pi * thetaLogKernel (-(↑α * 2 * I)))⊢ ∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2he:-(-2 * α) / 2 = αhpi:↑Real.pi ≠ 0h:-4 * ((4 * ↑Real.pi)⁻¹ * ∫ (y : ℝ), ↑(hardyWeight y) * cexp (↑α * ↑y)) = thetaLogKernel (-2 * ↑α * I)h':∫ (y : ℝ), ↑(hardyWeight y) * cexp (↑α * ↑y) = -(↑Real.pi * thetaLogKernel (-(↑α * 2 * I)))⊢ ∫ (t : ℝ), ↑(hardyWeight t) * cexp (↑α * ↑t) = -↑Real.pi * thetaLogKernel (-2 * ↑α * I) α:ℝhα:|α| < Real.pi / 4hb:|-2 * α| < Real.pi / 2he:-(-2 * α) / 2 = αhpi:↑Real.pi ≠ 0h:-4 * ((4 * ↑Real.pi)⁻¹ * ∫ (y : ℝ), ↑(hardyWeight y) * cexp (↑α * ↑y)) = thetaLogKernel (-2 * ↑α * I)h':∫ (y : ℝ), ↑(hardyWeight y) * cexp (↑α * ↑y) = -(↑Real.pi * thetaLogKernel (-(↑α * 2 * I)))⊢ ∫ (t : ℝ), ↑(hardyWeight t) * cexp (↑α * ↑t) = -↑Real.pi * thetaLogKernel (-(↑α * 2 * I)) All goals completed! 🐙theorem integral_hardyWeight_exp_eq_cosh {α : ℝ} (hα : |α| < Real.pi / 4) : (∫ t : ℝ, hardyWeight t * Real.exp (α * t)) = 2 * ∫ t : ℝ in Ioi 0, hardyWeight t * Real.cosh (α * t) := α:ℝhα:|α| < Real.pi / 4⊢ ∫ (t : ℝ), hardyWeight t * Real.exp (α * t) = 2 * ∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t) α:ℝhα:|α| < Real.pi / 4hp:Integrable (fun t => hardyWeight t * Real.exp (α * t)) volume⊢ ∫ (t : ℝ), hardyWeight t * Real.exp (α * t) = 2 * ∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t) α:ℝhα:|α| < Real.pi / 4hp:Integrable (fun t => hardyWeight t * Real.exp (α * t)) volumehm:Integrable (fun t => hardyWeight t * Real.exp (-α * t)) volume⊢ ∫ (t : ℝ), hardyWeight t * Real.exp (α * t) = 2 * ∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t) α:ℝhα:|α| < Real.pi / 4hp:Integrable (fun t => hardyWeight t * Real.exp (α * t)) volumehm:Integrable (fun t => hardyWeight t * Real.exp (-α * t)) volumehn:∫ (t : ℝ) in Iic 0, hardyWeight t * Real.exp (α * t) = ∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.exp (-α * t)⊢ ∫ (t : ℝ), hardyWeight t * Real.exp (α * t) = 2 * ∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t) α:ℝhα:|α| < Real.pi / 4hp:Integrable (fun t => hardyWeight t * Real.exp (α * t)) volumehm:Integrable (fun t => hardyWeight t * Real.exp (-α * t)) volumehn:∫ (t : ℝ) in Iic 0, hardyWeight t * Real.exp (α * t) = ∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.exp (-α * t)⊢ ∫ (a : ℝ) in Ioi 0, hardyWeight a * Real.exp (-α * a) + hardyWeight a * Real.exp (α * a) = ∫ (a : ℝ) in Ioi 0, 2 * (hardyWeight a * Real.cosh (α * a)) α:ℝhα:|α| < Real.pi / 4hp:Integrable (fun t => hardyWeight t * Real.exp (α * t)) volumehm:Integrable (fun t => hardyWeight t * Real.exp (-α * t)) volumehn:∫ (t : ℝ) in Iic 0, hardyWeight t * Real.exp (α * t) = ∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.exp (-α * t)⊢ EqOn (fun x => hardyWeight x * Real.exp (-α * x) + hardyWeight x * Real.exp (α * x)) (fun x => 2 * (hardyWeight x * Real.cosh (α * x))) (Ioi 0) α:ℝhα:|α| < Real.pi / 4hp:Integrable (fun t => hardyWeight t * Real.exp (α * t)) volumehm:Integrable (fun t => hardyWeight t * Real.exp (-α * t)) volumehn:∫ (t : ℝ) in Iic 0, hardyWeight t * Real.exp (α * t) = ∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.exp (-α * t)t:ℝa✝:t ∈ Ioi 0⊢ (fun x => hardyWeight x * Real.exp (-α * x) + hardyWeight x * Real.exp (α * x)) t = (fun x => 2 * (hardyWeight x * Real.cosh (α * x))) t α:ℝhα:|α| < Real.pi / 4hp:Integrable (fun t => hardyWeight t * Real.exp (α * t)) volumehm:Integrable (fun t => hardyWeight t * Real.exp (-α * t)) volumehn:∫ (t : ℝ) in Iic 0, hardyWeight t * Real.exp (α * t) = ∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.exp (-α * t)t:ℝa✝:t ∈ Ioi 0⊢ hardyWeight t * Real.exp (-α * t) + hardyWeight t * Real.exp (α * t) = 2 * (hardyWeight t * Real.cosh (α * t)) α:ℝhα:|α| < Real.pi / 4hp:Integrable (fun t => hardyWeight t * Real.exp (α * t)) volumehm:Integrable (fun t => hardyWeight t * Real.exp (-α * t)) volumehn:∫ (t : ℝ) in Iic 0, hardyWeight t * Real.exp (α * t) = ∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.exp (-α * t)t:ℝa✝:t ∈ Ioi 0⊢ hardyWeight t * Real.exp (-α * t) + hardyWeight t * Real.exp (α * t) = 2 * (hardyWeight t * ((Real.exp (α * t) + Real.exp (-(α * t))) / 2)) α:ℝhα:|α| < Real.pi / 4hp:Integrable (fun t => hardyWeight t * Real.exp (α * t)) volumehm:Integrable (fun t => hardyWeight t * Real.exp (-α * t)) volumehn:∫ (t : ℝ) in Iic 0, hardyWeight t * Real.exp (α * t) = ∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.exp (-α * t)t:ℝa✝:t ∈ Ioi 0⊢ hardyWeight t * Real.exp (-(α * t)) + hardyWeight t * Real.exp (α * t) = 2 * (hardyWeight t * ((Real.exp (α * t) + Real.exp (-(α * t))) / 2)) All goals completed! 🐙 /-- Hardy's open-strip cosh-transform identity for the actual zeta weight. -/theorem integral_hardyWeight_cosh {α : ℝ} (hα : |α| < Real.pi / 4) : ((∫ t : ℝ in Ioi 0, hardyWeight t * Real.cosh (α * t) : ℝ) : ℂ) = (Real.pi : ℂ) * Real.cos (α / 2) - Real.pi * thetaBoundaryRemainder α := α:ℝhα:|α| < Real.pi / 4⊢ ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = ↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * thetaBoundaryRemainder α α:ℝhα:|α| < Real.pi / 4h:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)⊢ ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = ↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * thetaBoundaryRemainder α α:ℝhα:|α| < Real.pi / 4h:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)hof:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = ↑(∫ (t : ℝ), hardyWeight t * Real.exp (α * t))⊢ ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = ↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * thetaBoundaryRemainder α α:ℝhα:|α| < Real.pi / 4h:↑2 * ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)hof:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = ↑(∫ (t : ℝ), hardyWeight t * Real.exp (α * t))⊢ ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = ↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * thetaBoundaryRemainder α α:ℝhα:|α| < Real.pi / 4h:2 * ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)hof:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = ↑(∫ (t : ℝ), hardyWeight t * Real.exp (α * t))⊢ ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = ↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * thetaBoundaryRemainder α α:ℝhα:|α| < Real.pi / 4h:2 * ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)hof:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = ↑(∫ (t : ℝ), hardyWeight t * Real.exp (α * t))he:↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) / 2⊢ ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = ↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * thetaBoundaryRemainder α α:ℝhα:|α| < Real.pi / 4h:2 * ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)hof:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = ↑(∫ (t : ℝ), hardyWeight t * Real.exp (α * t))he:↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) / 2⊢ -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) / 2 = ↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * thetaBoundaryRemainder α α:ℝhα:|α| < Real.pi / 4h:2 * ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)hof:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = ↑(∫ (t : ℝ), hardyWeight t * Real.exp (α * t))he:↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) / 2⊢ -↑Real.pi * (2 * cexp (-(↑(-2 * α) * I) / 4) * psi (cexp (-(↑(-2 * α) * I))) - cexp (↑(-2 * α) * I / 4)) / 2 = ↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * (cexp (I * ↑α / 2) * (1 / 2 + psi (cexp (2 * I * ↑α)))) α:ℝhα:|α| < Real.pi / 4h:2 * ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)hof:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = ↑(∫ (t : ℝ), hardyWeight t * Real.exp (α * t))he:↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) / 2ha:-(↑(-2 * α) * I) / 4 = I * ↑α / 2⊢ -↑Real.pi * (2 * cexp (-(↑(-2 * α) * I) / 4) * psi (cexp (-(↑(-2 * α) * I))) - cexp (↑(-2 * α) * I / 4)) / 2 = ↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * (cexp (I * ↑α / 2) * (1 / 2 + psi (cexp (2 * I * ↑α)))) α:ℝhα:|α| < Real.pi / 4h:2 * ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)hof:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = ↑(∫ (t : ℝ), hardyWeight t * Real.exp (α * t))he:↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) / 2ha:-(↑(-2 * α) * I) / 4 = I * ↑α / 2hb:-(↑(-2 * α) * I) = 2 * I * ↑α⊢ -↑Real.pi * (2 * cexp (-(↑(-2 * α) * I) / 4) * psi (cexp (-(↑(-2 * α) * I))) - cexp (↑(-2 * α) * I / 4)) / 2 = ↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * (cexp (I * ↑α / 2) * (1 / 2 + psi (cexp (2 * I * ↑α)))) α:ℝhα:|α| < Real.pi / 4h:2 * ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)hof:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = ↑(∫ (t : ℝ), hardyWeight t * Real.exp (α * t))he:↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) / 2ha:-(↑(-2 * α) * I) / 4 = I * ↑α / 2hb:-(↑(-2 * α) * I) = 2 * I * ↑αhc:↑(-2 * α) * I / 4 = -(I * ↑α / 2)⊢ -↑Real.pi * (2 * cexp (-(↑(-2 * α) * I) / 4) * psi (cexp (-(↑(-2 * α) * I))) - cexp (↑(-2 * α) * I / 4)) / 2 = ↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * (cexp (I * ↑α / 2) * (1 / 2 + psi (cexp (2 * I * ↑α)))) α:ℝhα:|α| < Real.pi / 4h:2 * ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)hof:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = ↑(∫ (t : ℝ), hardyWeight t * Real.exp (α * t))he:↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) / 2ha:-(↑(-2 * α) * I) / 4 = I * ↑α / 2hb:-(↑(-2 * α) * I) = 2 * I * ↑αhc:↑(-2 * α) * I / 4 = -(I * ↑α / 2)⊢ -↑Real.pi * (2 * cexp (I * ↑α / 2) * psi (cexp (2 * I * ↑α)) - cexp (-(I * ↑α / 2))) / 2 = ↑Real.pi * cos ↑(α / 2) - ↑Real.pi * (cexp (I * ↑α / 2) * (1 / 2 + psi (cexp (2 * I * ↑α)))) α:ℝhα:|α| < Real.pi / 4h:2 * ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)hof:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = ↑(∫ (t : ℝ), hardyWeight t * Real.exp (α * t))he:↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) / 2ha:-(↑(-2 * α) * I) / 4 = I * ↑α / 2hb:-(↑(-2 * α) * I) = 2 * I * ↑αhc:↑(-2 * α) * I / 4 = -(I * ↑α / 2)⊢ -↑Real.pi * (2 * cexp (I * ↑α / 2) * psi (cexp (2 * I * ↑α)) - cexp (-(I * ↑α / 2))) / 2 = ↑Real.pi * ((cexp (↑(α / 2) * I) + cexp (-↑(α / 2) * I)) / 2) - ↑Real.pi * (cexp (I * ↑α / 2) * (1 / 2 + psi (cexp (2 * I * ↑α)))) α:ℝhα:|α| < Real.pi / 4h:2 * ↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I)hof:∫ (t : ℝ), ↑(hardyWeight t * Real.exp (α * t)) = ↑(∫ (t : ℝ), hardyWeight t * Real.exp (α * t))he:↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (α * t)) = -↑Real.pi * thetaLogKernel (↑(-2 * α) * I) / 2ha:-(↑(-2 * α) * I) / 4 = I * ↑α / 2hb:-(↑(-2 * α) * I) = 2 * I * ↑αhc:↑(-2 * α) * I / 4 = -(I * ↑α / 2)⊢ -↑Real.pi * (2 * cexp (I * ↑α / 2) * psi (cexp (2 * I * ↑α)) - cexp (-(I * ↑α / 2))) / 2 = ↑Real.pi * ((cexp (↑α / 2 * I) + cexp (-(↑α / 2) * I)) / 2) - ↑Real.pi * (cexp (I * ↑α / 2) * (1 / 2 + psi (cexp (2 * I * ↑α)))) All goals completed! 🐙