HardyZeta.ThetaTransform

            
              11.21. HardyZeta.ThetaTransform🔗
            def modifiedThetaLogKernel (u : ℝ) : ℂ :=
  Real.exp (-u / 4) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u))theorem modifiedTheta_mellinConvergent (s : ℂ) :
    MellinConvergent (HurwitzZeta.hurwitzEvenFEPair 0).f_modif s :=
  ((HurwitzZeta.hurwitzEvenFEPair 0).isStrongFEPair_toStrongFEPair.hasMellin s).1

/-- An unconditional Fourier representation of the pole-removed completed zeta. -/theorem completedZeta₀_eq_fourier (t : ℝ) :
    completedRiemannZeta₀ (criticalPoint t) =
      𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 := byt:ℝ⊢ completedRiemannZeta₀ (criticalPoint t) = 𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2
  unfold completedRiemannZeta₀ HurwitzZeta.completedHurwitzZetaEven₀ WeakFEPair.Λ₀t:ℝ⊢ mellin (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (criticalPoint t / 2) / 2 =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2
  rw [mellin_eq_fouriert:ℝ⊢ 𝓕 (fun u => Real.exp (-(criticalPoint t / 2).re * u) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u)))
      ((criticalPoint t / 2).im / (2 * Real.pi)) /
    2 =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2]t:ℝ⊢ 𝓕 (fun u => Real.exp (-(criticalPoint t / 2).re * u) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u)))
      ((criticalPoint t / 2).im / (2 * Real.pi)) /
    2 =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2
  have hr : (criticalPoint t / 2).re = 1 / 4 := byt:ℝ⊢ completedRiemannZeta₀ (criticalPoint t) = 𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 simp [criticalPoint]t:ℝ⊢ 2⁻¹ / 2 = 4⁻¹; ringt:ℝhr:(criticalPoint t / 2).re = 1 / 4⊢ 𝓕 (fun u => Real.exp (-(criticalPoint t / 2).re * u) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u)))
      ((criticalPoint t / 2).im / (2 * Real.pi)) /
    2 =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2
  have hi : (criticalPoint t / 2).im / (2 * Real.pi) = t / (4 * Real.pi) := byt:ℝ⊢ completedRiemannZeta₀ (criticalPoint t) = 𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2
    simp [criticalPoint]t:ℝhr:(criticalPoint t / 2).re = 1 / 4⊢ t / 2 / (2 * Real.pi) = t / (4 * Real.pi)
    ringt:ℝhr:(criticalPoint t / 2).re = 1 / 4hi:(criticalPoint t / 2).im / (2 * Real.pi) = t / (4 * Real.pi)⊢ 𝓕 (fun u => Real.exp (-(criticalPoint t / 2).re * u) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u)))
      ((criticalPoint t / 2).im / (2 * Real.pi)) /
    2 =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2
  rw [hr,t:ℝhr:(criticalPoint t / 2).re = 1 / 4hi:(criticalPoint t / 2).im / (2 * Real.pi) = t / (4 * Real.pi)⊢ 𝓕 (fun u => Real.exp (-(1 / 4) * u) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u)))
      ((criticalPoint t / 2).im / (2 * Real.pi)) /
    2 =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 hit:ℝhr:(criticalPoint t / 2).re = 1 / 4hi:(criticalPoint t / 2).im / (2 * Real.pi) = t / (4 * Real.pi)⊢ 𝓕 (fun u => Real.exp (-(1 / 4) * u) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u))) (t / (4 * Real.pi)) /
    2 =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2]t:ℝhr:(criticalPoint t / 2).re = 1 / 4hi:(criticalPoint t / 2).im / (2 * Real.pi) = t / (4 * Real.pi)⊢ 𝓕 (fun u => Real.exp (-(1 / 4) * u) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u))) (t / (4 * Real.pi)) /
    2 =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2
  simp_rw [t:ℝhr:(criticalPoint t / 2).re = 1 / 4hi:(criticalPoint t / 2).im / (2 * Real.pi) = t / (4 * Real.pi)⊢ 𝓕 (fun u => Real.exp (-(1 / 4) * u) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u))) (t / (4 * Real.pi)) /
    2 =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2show ∀ u : ℝ, -(1 / 4) * u = -u / 4 from fun u ↦ byt:ℝhr:(criticalPoint t / 2).re = 1 / 4hi:(criticalPoint t / 2).im / (2 * Real.pi) = t / (4 * Real.pi)u:ℝ⊢ -(1 / 4) * u = -u / 4 ringAll goals completed! 🐙]
  rflAll goals completed! 🐙

/-- The pole correction in the same representation is explicit. -/theorem completedZeta_eq_fourier (t : ℝ) :
    completedRiemannZeta (criticalPoint t) =
      𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 -
        1 / criticalPoint t - 1 / (1 - criticalPoint t) := byt:ℝ⊢ completedRiemannZeta (criticalPoint t) =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / criticalPoint t - 1 / (1 - criticalPoint t)
  rw [completedRiemannZeta_eq,t:ℝ⊢ completedRiemannZeta₀ (criticalPoint t) - 1 / criticalPoint t - 1 / (1 - criticalPoint t) =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / criticalPoint t - 1 / (1 - criticalPoint t) completedZeta₀_eq_fouriert:ℝ⊢ 𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / criticalPoint t - 1 / (1 - criticalPoint t) =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / criticalPoint t - 1 / (1 - criticalPoint t)]All goals completed! 🐙

/-- Logarithmic change of variables transfers Mellin convergence to L¹. -/theorem integrable_mellinLogKernel {f : ℝ → ℂ} {σ : ℝ}
    (hf : MellinConvergent f (σ : ℂ)) :
    Integrable (fun u : ℝ ↦ Real.exp (-σ * u) • f (Real.exp (-u))) := byf:ℝ → ℂσ:ℝhf:MellinConvergent f ↑σ⊢ Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) volume
  have himage : (fun u : ℝ ↦ Real.exp (-u)) '' univ = Ioi 0 := by
    change (Real.exp ∘ Neg.neg) '' univ = Ioi 0f:ℝ → ℂσ:ℝhf:MellinConvergent f ↑σ⊢ Real.exp ∘ Neg.neg '' univ = Ioi 0
    rw [Set.image_comp,f:ℝ → ℂσ:ℝhf:MellinConvergent f ↑σ⊢ Real.exp '' Neg.neg '' univ = Ioi 0 Set.image_univ_of_surjective neg_surjective,f:ℝ → ℂσ:ℝhf:MellinConvergent f ↑σ⊢ Real.exp '' univ = Ioi 0
      Set.image_univ,f:ℝ → ℂσ:ℝhf:MellinConvergent f ↑σ⊢ range Real.exp = Ioi 0 Real.range_expf:ℝ → ℂσ:ℝhf:MellinConvergent f ↑σ⊢ Ioi 0 = Ioi 0]f:ℝ → ℂσ:ℝhf:MellinConvergent f ↑σhimage:(fun u => Real.exp (-u)) '' univ = Ioi 0⊢ Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) volume
  have hder : ∀ u ∈ (univ : Set ℝ), HasDerivWithinAt
      (fun u : ℝ ↦ Real.exp (-u)) (-Real.exp (-u)) univ u := by
    intro u _f:ℝ → ℂσ:ℝhf:MellinConvergent f ↑σhimage:(fun u => Real.exp (-u)) '' univ = Ioi 0u:ℝa✝:u ∈ univ⊢ HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ u
    simpa using ((hasDerivAt_neg u).exp)f:ℝ → ℂσ:ℝhf:MellinConvergent f ↑σhimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ u⊢ Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) volume
  have hinj : InjOn (fun u : ℝ ↦ Real.exp (-u)) univ :=
    Real.exp_injective.injOn.comp neg_injective.injOn (univ.mapsTo_univ _)f:ℝ → ℂσ:ℝhf:MellinConvergent f ↑σhimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univ⊢ Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) volume
  unfold MellinConvergent at hff:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) (Ioi 0) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univ⊢ Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) volume
  rw [← himagef:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univ⊢ Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) volume] at hff:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univ⊢ Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) volume
  have h := (integrableOn_image_iff_integrableOn_abs_deriv_smul MeasurableSet.univ
    hder hinj (fun t : ℝ ↦ (t : ℂ) ^ ((σ : ℂ) - 1) • f t)).mp hff:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:IntegrableOn (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) univ volume⊢ Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) volume
  rw [integrableOn_univf:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volume⊢ Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) volume] at hf:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volume⊢ Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) volume
  have he (u : ℝ) : |(-Real.exp (-u))| •
      ((Real.exp (-u) : ℂ) ^ ((σ : ℂ) - 1) • f (Real.exp (-u))) =
        Real.exp (-σ * u) • f (Real.exp (-u)) := by
    rw [abs_neg,f:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝ⊢ |Real.exp (-u)| • ↑(Real.exp (-u)) ^ (↑σ - 1) • f (Real.exp (-u)) = Real.exp (-σ * u) • f (Real.exp (-u)) abs_of_pos (Real.exp_pos _),f:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝ⊢ Real.exp (-u) • ↑(Real.exp (-u)) ^ (↑σ - 1) • f (Real.exp (-u)) = Real.exp (-σ * u) • f (Real.exp (-u)) real_smulf:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝ⊢ ↑(Real.exp (-u)) * ↑(Real.exp (-u)) ^ (↑σ - 1) • f (Real.exp (-u)) = Real.exp (-σ * u) • f (Real.exp (-u))]f:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝ⊢ ↑(Real.exp (-u)) * ↑(Real.exp (-u)) ^ (↑σ - 1) • f (Real.exp (-u)) = Real.exp (-σ * u) • f (Real.exp (-u))
    have hp : (Real.exp (-u) : ℂ) * (Real.exp (-u) : ℂ) ^ ((σ : ℂ) - 1) =
        (Real.exp (-σ * u) : ℂ) := byf:ℝ → ℂσ:ℝhf:MellinConvergent f ↑σ⊢ Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) volume
      rw [cpow_def_of_ne_zero (ofReal_ne_zero.mpr (Real.exp_ne_zero _)),f:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝ⊢ ↑(Real.exp (-u)) * cexp (log ↑(Real.exp (-u)) * (↑σ - 1)) = ↑(Real.exp (-σ * u))
        ← ofReal_log (Real.exp_pos _).le,f:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝ⊢ ↑(Real.exp (-u)) * cexp (↑(Real.log (Real.exp (-u))) * (↑σ - 1)) = ↑(Real.exp (-σ * u)) Real.log_expf:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝ⊢ ↑(Real.exp (-u)) * cexp (↑(-u) * (↑σ - 1)) = ↑(Real.exp (-σ * u))]f:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝ⊢ ↑(Real.exp (-u)) * cexp (↑(-u) * (↑σ - 1)) = ↑(Real.exp (-σ * u))
      push_castf:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝ⊢ cexp (-↑u) * cexp (-↑u * (↑σ - 1)) = cexp (-↑σ * ↑u)
      rw [← exp_addf:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝ⊢ cexp (-↑u + -↑u * (↑σ - 1)) = cexp (-↑σ * ↑u)]f:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝ⊢ cexp (-↑u + -↑u * (↑σ - 1)) = cexp (-↑σ * ↑u)
      congr 1f:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝ⊢ -↑u + -↑u * (↑σ - 1) = -↑σ * ↑u
      ringf:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝhp:↑(Real.exp (-u)) * ↑(Real.exp (-u)) ^ (↑σ - 1) = ↑(Real.exp (-σ * u))⊢ ↑(Real.exp (-u)) * ↑(Real.exp (-u)) ^ (↑σ - 1) • f (Real.exp (-u)) = Real.exp (-σ * u) • f (Real.exp (-u))
    rw [smul_eq_mul,f:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝhp:↑(Real.exp (-u)) * ↑(Real.exp (-u)) ^ (↑σ - 1) = ↑(Real.exp (-σ * u))⊢ ↑(Real.exp (-u)) * (↑(Real.exp (-u)) ^ (↑σ - 1) * f (Real.exp (-u))) = Real.exp (-σ * u) • f (Real.exp (-u)) ← mul_assoc,f:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝhp:↑(Real.exp (-u)) * ↑(Real.exp (-u)) ^ (↑σ - 1) = ↑(Real.exp (-σ * u))⊢ ↑(Real.exp (-u)) * ↑(Real.exp (-u)) ^ (↑σ - 1) * f (Real.exp (-u)) = Real.exp (-σ * u) • f (Real.exp (-u)) hp,f:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝhp:↑(Real.exp (-u)) * ↑(Real.exp (-u)) ^ (↑σ - 1) = ↑(Real.exp (-σ * u))⊢ ↑(Real.exp (-σ * u)) * f (Real.exp (-u)) = Real.exp (-σ * u) • f (Real.exp (-u)) real_smulf:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumeu:ℝhp:↑(Real.exp (-u)) * ↑(Real.exp (-u)) ^ (↑σ - 1) = ↑(Real.exp (-σ * u))⊢ ↑(Real.exp (-σ * u)) * f (Real.exp (-u)) = ↑(Real.exp (-σ * u)) * f (Real.exp (-u))]f:ℝ → ℂσ:ℝhf:IntegrableOn (fun t => ↑t ^ (↑σ - 1) • f t) ((fun u => Real.exp (-u)) '' univ) volumehimage:(fun u => Real.exp (-u)) '' univ = Ioi 0hder:∀ u ∈ univ, HasDerivWithinAt (fun u => Real.exp (-u)) (-Real.exp (-u)) univ uhinj:InjOn (fun u => Real.exp (-u)) univh:Integrable (fun x => |(-Real.exp (-x))| • ↑(Real.exp (-x)) ^ (↑σ - 1) • f (Real.exp (-x))) volumehe:∀ (u : ℝ), |(-Real.exp (-u))| • ↑(Real.exp (-u)) ^ (↑σ - 1) • f (Real.exp (-u)) = Real.exp (-σ * u) • f (Real.exp (-u))⊢ Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) volume
  simpa only [he] using hAll goals completed! 🐙theorem integrable_modifiedThetaLogKernel : Integrable modifiedThetaLogKernel := by⊢ Integrable modifiedThetaLogKernel volume
  have h := integrable_mellinLogKernel (σ := 1 / 4)
    (modifiedTheta_mellinConvergent ((1 / 4 : ℝ) : ℂ))h:Integrable (fun u => Real.exp (-(1 / 4) * u) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u))) volume⊢ Integrable modifiedThetaLogKernel volume
  unfold modifiedThetaLogKernelh:Integrable (fun u => Real.exp (-(1 / 4) * u) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u))) volume⊢ Integrable (fun u => Real.exp (-u / 4) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u))) volume
  simpa only [show ∀ u : ℝ, -(1 / 4) * u = -u / 4 from fun u ↦ byh:Integrable (fun u => Real.exp (-(1 / 4) * u) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u))) volumeu:ℝ⊢ -(1 / 4) * u = -u / 4 ringAll goals completed! 🐙] using h

/-- The elementary correction to the logarithmic kernel. -/def poleLogKernel (u : ℝ) : ℂ := (Real.exp (-|u| / 4) : ℂ)theorem integrable_poleLogKernel : Integrable poleLogKernel := by⊢ Integrable poleLogKernel volume
  unfold poleLogKernel⊢ Integrable (fun u => ↑(Real.exp (-|u| / 4))) volume
  simpa only [show ∀ u : ℝ, -(1 / 4) * |u| = -|u| / 4 from fun u ↦ byu:ℝ⊢ -(1 / 4) * |u| = -|u| / 4 ringAll goals completed! 🐙] using
    integrable_exp_neg_abs (by⊢ 0 < 1 / 4 norm_numAll goals completed! 🐙 : (0 : ℝ) < 1 / 4)theorem fourier_poleLogKernel (t : ℝ) :
    𝓕 poleLogKernel (t / (4 * Real.pi)) / 2 =
      1 / criticalPoint t + 1 / (1 - criticalPoint t) := byt:ℝ⊢ 𝓕 poleLogKernel (t / (4 * Real.pi)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)
  have h := fourier_exp_neg_abs (byt:ℝ⊢ 0 < 1 / 4 norm_numAll goals completed! 🐙 : (0 : ℝ) < 1 / 4) (t / (4 * Real.pi))t:ℝh:𝓕 (fun u => ↑(Real.exp (-(1 / 4) * |u|))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)⊢ 𝓕 poleLogKernel (t / (4 * Real.pi)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)
  simp only [show ∀ u : ℝ, -(1 / 4) * |u| = -|u| / 4 from fun u ↦ by ring] at ht:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)⊢ 𝓕 poleLogKernel (t / (4 * Real.pi)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)
  change 𝓕 (fun u : ℝ ↦ (Real.exp (-|u| / 4) : ℂ)) _ / 2 = _t:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)⊢ 𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)
  rw [ht:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)⊢ (1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)) /
    2 =
  1 / criticalPoint t + 1 / (1 - criticalPoint t)]t:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)⊢ (1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)) /
    2 =
  1 / criticalPoint t + 1 / (1 - criticalPoint t)
  have he : (2 : ℂ) * Real.pi * ((t / (4 * Real.pi) : ℝ) : ℂ) = (t : ℂ) / 2 := byt:ℝ⊢ 𝓕 poleLogKernel (t / (4 * Real.pi)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)
    push_castt:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)⊢ 2 * ↑Real.pi * (↑t / (4 * ↑Real.pi)) = ↑t / 2
    field_simpt:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)⊢ 2 ^ 2 * ↑t = ↑t * 4
    ringt:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2⊢ (1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)) /
    2 =
  1 / criticalPoint t + 1 / (1 - criticalPoint t)
  rw [het:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2⊢ (1 / (↑(1 / 4) - ↑t / 2 * I) + 1 / (↑(1 / 4) + ↑t / 2 * I)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)]t:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2⊢ (1 / (↑(1 / 4) - ↑t / 2 * I) + 1 / (↑(1 / 4) + ↑t / 2 * I)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)
  have hl : ((1 / 4 : ℝ) : ℂ) - (t : ℂ) / 2 * I = (1 - criticalPoint t) / 2 := byt:ℝ⊢ 𝓕 poleLogKernel (t / (4 * Real.pi)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)
    unfold criticalPointt:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2⊢ ↑(1 / 4) - ↑t / 2 * I = (1 - (1 / 2 + ↑t * I)) / 2
    push_castt:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2⊢ 1 / 4 - ↑t / 2 * I = (1 - (1 / 2 + ↑t * I)) / 2
    ringt:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2hl:↑(1 / 4) - ↑t / 2 * I = (1 - criticalPoint t) / 2⊢ (1 / (↑(1 / 4) - ↑t / 2 * I) + 1 / (↑(1 / 4) + ↑t / 2 * I)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)
  have hr : ((1 / 4 : ℝ) : ℂ) + (t : ℂ) / 2 * I = criticalPoint t / 2 := byt:ℝ⊢ 𝓕 poleLogKernel (t / (4 * Real.pi)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)
    unfold criticalPointt:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2hl:↑(1 / 4) - ↑t / 2 * I = (1 - criticalPoint t) / 2⊢ ↑(1 / 4) + ↑t / 2 * I = (1 / 2 + ↑t * I) / 2
    push_castt:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2hl:↑(1 / 4) - ↑t / 2 * I = (1 - criticalPoint t) / 2⊢ 1 / 4 + ↑t / 2 * I = (1 / 2 + ↑t * I) / 2
    ringt:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2hl:↑(1 / 4) - ↑t / 2 * I = (1 - criticalPoint t) / 2hr:↑(1 / 4) + ↑t / 2 * I = criticalPoint t / 2⊢ (1 / (↑(1 / 4) - ↑t / 2 * I) + 1 / (↑(1 / 4) + ↑t / 2 * I)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)
  rw [hl,t:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2hl:↑(1 / 4) - ↑t / 2 * I = (1 - criticalPoint t) / 2hr:↑(1 / 4) + ↑t / 2 * I = criticalPoint t / 2⊢ (1 / ((1 - criticalPoint t) / 2) + 1 / (↑(1 / 4) + ↑t / 2 * I)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t) hr,t:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2hl:↑(1 / 4) - ↑t / 2 * I = (1 - criticalPoint t) / 2hr:↑(1 / 4) + ↑t / 2 * I = criticalPoint t / 2⊢ (1 / ((1 - criticalPoint t) / 2) + 1 / (criticalPoint t / 2)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t) one_div_div,t:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2hl:↑(1 / 4) - ↑t / 2 * I = (1 - criticalPoint t) / 2hr:↑(1 / 4) + ↑t / 2 * I = criticalPoint t / 2⊢ (2 / (1 - criticalPoint t) + 1 / (criticalPoint t / 2)) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t) one_div_div,t:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2hl:↑(1 / 4) - ↑t / 2 * I = (1 - criticalPoint t) / 2hr:↑(1 / 4) + ↑t / 2 * I = criticalPoint t / 2⊢ (2 / (1 - criticalPoint t) + 2 / criticalPoint t) / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t) add_divt:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2hl:↑(1 / 4) - ↑t / 2 * I = (1 - criticalPoint t) / 2hr:↑(1 / 4) + ↑t / 2 * I = criticalPoint t / 2⊢ 2 / (1 - criticalPoint t) / 2 + 2 / criticalPoint t / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)]t:ℝh:𝓕 (fun u => ↑(Real.exp (-|u| / 4))) (t / (4 * Real.pi)) =
  1 / (↑(1 / 4) - 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I) + 1 / (↑(1 / 4) + 2 * ↑Real.pi * ↑(t / (4 * Real.pi)) * I)he:2 * ↑Real.pi * ↑(t / (4 * Real.pi)) = ↑t / 2hl:↑(1 / 4) - ↑t / 2 * I = (1 - criticalPoint t) / 2hr:↑(1 / 4) + ↑t / 2 * I = criticalPoint t / 2⊢ 2 / (1 - criticalPoint t) / 2 + 2 / criticalPoint t / 2 = 1 / criticalPoint t + 1 / (1 - criticalPoint t)
  ringAll goals completed! 🐙

/-- The integrable theta kernel after removing both poles. -/def correctedThetaLogKernel (u : ℝ) : ℂ := modifiedThetaLogKernel u - poleLogKernel utheorem integrable_correctedThetaLogKernel : Integrable correctedThetaLogKernel :=
  integrable_modifiedThetaLogKernel.sub integrable_poleLogKerneltheorem fourier_sub_of_integrable {f g : ℝ → ℂ} (hf : Integrable f) (hg : Integrable g)
    (w : ℝ) : 𝓕 (fun u ↦ f u - g u) w = 𝓕 f w - 𝓕 g w := byf:ℝ → ℂg:ℝ → ℂhf:Integrable f volumehg:Integrable g volumew:ℝ⊢ 𝓕 (fun u => f u - g u) w = 𝓕 f w - 𝓕 g w
  simp only [Real.fourier_eq, smul_sub]f:ℝ → ℂg:ℝ → ℂhf:Integrable f volumehg:Integrable g volumew:ℝ⊢ ∫ (v : ℝ), 𝐞 (-inner ℝ v w) • f v - 𝐞 (-inner ℝ v w) • g v =
  (∫ (v : ℝ), 𝐞 (-inner ℝ v w) • f v) - ∫ (v : ℝ), 𝐞 (-inner ℝ v w) • g v
  apply integral_subhff:ℝ → ℂg:ℝ → ℂhf:Integrable f volumehg:Integrable g volumew:ℝ⊢ Integrable (fun a => 𝐞 (-inner ℝ a w) • f a) volumehgf:ℝ → ℂg:ℝ → ℂhf:Integrable f volumehg:Integrable g volumew:ℝ⊢ Integrable (fun a => 𝐞 (-inner ℝ a w) • g a) volume
  ·hff:ℝ → ℂg:ℝ → ℂhf:Integrable f volumehg:Integrable g volumew:ℝ⊢ Integrable (fun a => 𝐞 (-inner ℝ a w) • f a) volume exact (Real.fourierIntegral_convergent_iff w).mpr hfAll goals completed! 🐙
  ·hgf:ℝ → ℂg:ℝ → ℂhf:Integrable f volumehg:Integrable g volumew:ℝ⊢ Integrable (fun a => 𝐞 (-inner ℝ a w) • g a) volume exact (Real.fourierIntegral_convergent_iff w).mpr hgAll goals completed! 🐙

/-- The actual completed zeta is the Fourier transform of one integrable kernel. -/theorem completedZeta_eq_fourier_corrected (t : ℝ) :
    completedRiemannZeta (criticalPoint t) =
      𝓕 correctedThetaLogKernel (t / (4 * Real.pi)) / 2 := byt:ℝ⊢ completedRiemannZeta (criticalPoint t) = 𝓕 correctedThetaLogKernel (t / (4 * Real.pi)) / 2
  rw [completedZeta_eq_fouriert:ℝ⊢ 𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / criticalPoint t - 1 / (1 - criticalPoint t) =
  𝓕 correctedThetaLogKernel (t / (4 * Real.pi)) / 2]t:ℝ⊢ 𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / criticalPoint t - 1 / (1 - criticalPoint t) =
  𝓕 correctedThetaLogKernel (t / (4 * Real.pi)) / 2
  unfold correctedThetaLogKernelt:ℝ⊢ 𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / criticalPoint t - 1 / (1 - criticalPoint t) =
  𝓕 (fun u => modifiedThetaLogKernel u - poleLogKernel u) (t / (4 * Real.pi)) / 2
  rw [fourier_sub_of_integrable integrable_modifiedThetaLogKernel integrable_poleLogKernel,t:ℝ⊢ 𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / criticalPoint t - 1 / (1 - criticalPoint t) =
  (𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) - 𝓕 poleLogKernel (t / (4 * Real.pi))) / 2
    sub_div,t:ℝ⊢ 𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / criticalPoint t - 1 / (1 - criticalPoint t) =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 𝓕 poleLogKernel (t / (4 * Real.pi)) / 2 fourier_poleLogKernelt:ℝ⊢ 𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / criticalPoint t - 1 / (1 - criticalPoint t) =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - (1 / criticalPoint t + 1 / (1 - criticalPoint t))]t:ℝ⊢ 𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / criticalPoint t - 1 / (1 - criticalPoint t) =
  𝓕 modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - (1 / criticalPoint t + 1 / (1 - criticalPoint t))
  ringAll goals completed! 🐙

/-- The smooth kernel whose restriction agrees almost everywhere with the corrected kernel. -/def thetaLogKernel (z : ℂ) : ℂ :=
  2 * exp (-z / 4) * psi (exp (-z)) - exp (z / 4)theorem correctedThetaLogKernel_eq {u : ℝ} (hu : u ≠ 0) :
    correctedThetaLogKernel u = thetaLogKernel (u : ℂ) := byu:ℝhu:u ≠ 0⊢ correctedThetaLogKernel u = thetaLogKernel ↑u
  have hx : 0 < Real.exp (-u) := Real.exp_pos _u:ℝhu:u ≠ 0hx:0 < Real.exp (-u)⊢ correctedThetaLogKernel u = thetaLogKernel ↑u
  have he : exp (-(u : ℂ)) = (Real.exp (-u) : ℂ) := by simpu:ℝhu:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))⊢ correctedThetaLogKernel u = thetaLogKernel ↑u
  unfold thetaLogKernelu:ℝhu:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * psi (cexp (-↑u)) - cexp (↑u / 4)
  rw [he,u:ℝhu:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * psi ↑(Real.exp (-u)) - cexp (↑u / 4) psi_ofReal_eq_evenKernelu:ℝhu:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)]u:ℝhu:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)
  rcases lt_or_gt_of_ne hu with hu | huinlu:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:u < 0⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)inru:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < u⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)
  ·inlu:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:u < 0⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4) have hx1 : 1 < Real.exp (-u) := byu:ℝhu:u ≠ 0⊢ correctedThetaLogKernel u = thetaLogKernel ↑u simpa using Real.one_lt_exp_iff.mpr (neg_pos.mpr hu)inlu:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:u < 0hx1:1 < Real.exp (-u)⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)
    have hn : ¬ Real.exp (-u) < 1 := not_lt_of_ge hx1.leinlu:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:u < 0hx1:1 < Real.exp (-u)hn:¬Real.exp (-u) < 1⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)
    simp [correctedThetaLogKernel, modifiedThetaLogKernel, poleLogKernel,
      WeakFEPair.f_modif, HurwitzZeta.hurwitzEvenFEPair, hx1, hn,
      abs_of_neg hu, real_smul, smul_eq_mul, ofReal_exp]inlu:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:u < 0hx1:1 < Real.exp (-u)hn:¬Real.exp (-u) < 1⊢ cexp (-↑u / 4) * (↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) =
  2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2)
    ringAll goals completed! 🐙
  ·inru:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < u⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4) have hx1 : Real.exp (-u) < 1 := byu:ℝhu:u ≠ 0⊢ correctedThetaLogKernel u = thetaLogKernel ↑u simpa using Real.exp_lt_one_iff.mpr (neg_neg_of_pos hu)inru:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)
    have hn : ¬ 1 < Real.exp (-u) := not_lt_of_ge hx1.leinru:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)
    have hp : (Real.exp (-u)) ^ (-(1 / 2 : ℝ)) = Real.exp (u / 2) := byu:ℝhu:u ≠ 0⊢ correctedThetaLogKernel u = thetaLogKernel ↑u
      rw [Real.rpow_def_of_pos hx,u:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)⊢ Real.exp (Real.log (Real.exp (-u)) * -(1 / 2)) = Real.exp (u / 2) Real.log_expu:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)⊢ Real.exp (-u * -(1 / 2)) = Real.exp (u / 2)]u:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)⊢ Real.exp (-u * -(1 / 2)) = Real.exp (u / 2)
      congr 1u:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)⊢ -u * -(1 / 2) = u / 2
      ringinru:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)hp:Real.exp (-u) ^ (-(1 / 2)) = Real.exp (u / 2)⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)
    simp only [one_div] at hpinru:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)hp:Real.exp (-u) ^ (-2⁻¹) = Real.exp (u / 2)⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)
    have hmul : (Real.exp (-u / 4) : ℂ) * (Real.exp (u / 2) : ℂ) =
        (Real.exp (u / 4) : ℂ) := byu:ℝhu:u ≠ 0⊢ correctedThetaLogKernel u = thetaLogKernel ↑u
      rw [← ofReal_mul,u:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)hp:Real.exp (-u) ^ (-2⁻¹) = Real.exp (u / 2)⊢ ↑(Real.exp (-u / 4) * Real.exp (u / 2)) = ↑(Real.exp (u / 4)) ← Real.exp_addu:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)hp:Real.exp (-u) ^ (-2⁻¹) = Real.exp (u / 2)⊢ ↑(Real.exp (-u / 4 + u / 2)) = ↑(Real.exp (u / 4))]u:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)hp:Real.exp (-u) ^ (-2⁻¹) = Real.exp (u / 2)⊢ ↑(Real.exp (-u / 4 + u / 2)) = ↑(Real.exp (u / 4))
      congr 2u:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)hp:Real.exp (-u) ^ (-2⁻¹) = Real.exp (u / 2)⊢ -u / 4 + u / 2 = u / 4
      ringinru:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)hp:Real.exp (-u) ^ (-2⁻¹) = Real.exp (u / 2)hmul:↑(Real.exp (-u / 4)) * ↑(Real.exp (u / 2)) = ↑(Real.exp (u / 4))⊢ correctedThetaLogKernel u = 2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)
    simp [correctedThetaLogKernel, modifiedThetaLogKernel, poleLogKernel,
      WeakFEPair.f_modif, HurwitzZeta.hurwitzEvenFEPair, hx1, hn, hx, hp,
      abs_of_pos hu, real_smul, smul_eq_mul]inru:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)hp:Real.exp (-u) ^ (-2⁻¹) = Real.exp (u / 2)hmul:↑(Real.exp (-u / 4)) * ↑(Real.exp (u / 2)) = ↑(Real.exp (u / 4))⊢ cexp (-↑u / 4) * (↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - cexp (↑u / 2)) - cexp (-↑u / 4) =
  2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)
    push_cast at hmul ⊢inru:ℝhu✝:u ≠ 0hx:0 < Real.exp (-u)he:cexp (-↑u) = ↑(Real.exp (-u))hu:0 < uhx1:Real.exp (-u) < 1hn:¬1 < Real.exp (-u)hp:Real.exp (-u) ^ (-2⁻¹) = Real.exp (u / 2)hmul:cexp (-↑u / 4) * cexp (↑u / 2) = cexp (↑u / 4)⊢ cexp (-↑u / 4) * (↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - cexp (↑u / 2)) - cexp (-↑u / 4) =
  2 * cexp (-↑u / 4) * ((↑(HurwitzZeta.evenKernel 0 (Real.exp (-u))) - 1) / 2) - cexp (↑u / 4)
    linear_combination -hmulAll goals completed! 🐙theorem correctedThetaLogKernel_ae_eq :
    correctedThetaLogKernel =ᵐ[volume] fun u : ℝ ↦ thetaLogKernel (u : ℂ) := by⊢ correctedThetaLogKernel =ᵐ[volume] fun u => thetaLogKernel ↑u
  filter_upwards [volume.ae_ne (0 : ℝ)] with u huu:ℝhu:u ≠ 0⊢ correctedThetaLogKernel u = thetaLogKernel ↑u using correctedThetaLogKernel_eq hutheorem integrable_thetaLogKernel : Integrable (fun u : ℝ ↦ thetaLogKernel (u : ℂ)) :=
  integrable_correctedThetaLogKernel.congr correctedThetaLogKernel_ae_eqtheorem completedZeta_eq_fourier_theta (t : ℝ) :
    completedRiemannZeta (criticalPoint t) =
      𝓕 (fun u : ℝ ↦ thetaLogKernel (u : ℂ)) (t / (4 * Real.pi)) / 2 := byt:ℝ⊢ completedRiemannZeta (criticalPoint t) = 𝓕 (fun u => thetaLogKernel ↑u) (t / (4 * Real.pi)) / 2
  rw [completedZeta_eq_fourier_corrected,t:ℝ⊢ 𝓕 correctedThetaLogKernel (t / (4 * Real.pi)) / 2 = 𝓕 (fun u => thetaLogKernel ↑u) (t / (4 * Real.pi)) / 2
    Real.fourier_congr_ae correctedThetaLogKernel_ae_eqt:ℝ⊢ 𝓕 (fun u => thetaLogKernel ↑u) (t / (4 * Real.pi)) / 2 = 𝓕 (fun u => thetaLogKernel ↑u) (t / (4 * Real.pi)) / 2]All goals completed! 🐙theorem differentiableAt_thetaLogKernel {z : ℂ} (hz : |z.im| < Real.pi / 2) :
    DifferentiableAt ℂ thetaLogKernel z := byz:ℂhz:|z.im| < Real.pi / 2⊢ DifferentiableAt ℂ thetaLogKernel z
  have hc : 0 < (exp (-z)).re := by
    rw [exp_rez:ℂhz:|z.im| < Real.pi / 2⊢ 0 < Real.exp (-z).re * Real.cos (-z).im]z:ℂhz:|z.im| < Real.pi / 2⊢ 0 < Real.exp (-z).re * Real.cos (-z).im
    apply mul_pos (Real.exp_pos _)z:ℂhz:|z.im| < Real.pi / 2⊢ 0 < Real.cos (-z).im
    apply Real.cos_pos_of_mem_Iooz:ℂhz:|z.im| < Real.pi / 2⊢ (-z).im ∈ Ioo (-(Real.pi / 2)) (Real.pi / 2)
    rw [neg_imz:ℂhz:|z.im| < Real.pi / 2⊢ -z.im ∈ Ioo (-(Real.pi / 2)) (Real.pi / 2)]z:ℂhz:|z.im| < Real.pi / 2⊢ -z.im ∈ Ioo (-(Real.pi / 2)) (Real.pi / 2)
    exact ⟨byz:ℂhz:|z.im| < Real.pi / 2⊢ -(Real.pi / 2) < -z.im linarith [(abs_lt.mp hz).2]All goals completed! 🐙, byz:ℂhz:|z.im| < Real.pi / 2⊢ -z.im < Real.pi / 2 linarith [(abs_lt.mp hz).1]All goals completed! 🐙⟩z:ℂhz:|z.im| < Real.pi / 2hc:0 < (cexp (-z)).re⊢ DifferentiableAt ℂ thetaLogKernel z
  have hp := (differentiableAt_psi hc).comp z (differentiableAt_id.neg.cexp)z:ℂhz:|z.im| < Real.pi / 2hc:0 < (cexp (-z)).rehp:DifferentiableAt ℂ (psi ∘ fun x => cexp ((-id) x)) z⊢ DifferentiableAt ℂ thetaLogKernel z
  unfold thetaLogKernelz:ℂhz:|z.im| < Real.pi / 2hc:0 < (cexp (-z)).rehp:DifferentiableAt ℂ (psi ∘ fun x => cexp ((-id) x)) z⊢ DifferentiableAt ℂ (fun z => 2 * cexp (-z / 4) * psi (cexp (-z)) - cexp (z / 4)) z
  fun_propAll goals completed! 🐙theorem thetaLogKernel_neg {z : ℂ} (hz : |z.im| < Real.pi / 2) :
    thetaLogKernel (-z) = thetaLogKernel z := byz:ℂhz:|z.im| < Real.pi / 2⊢ thetaLogKernel (-z) = thetaLogKernel z
  have hp : exp (-z) ^ (1 / 2 : ℂ) = exp (-z / 2) := by
    rw [cpow_def_of_ne_zero (exp_ne_zero _),z:ℂhz:|z.im| < Real.pi / 2⊢ cexp (log (cexp (-z)) * (1 / 2)) = cexp (-z / 2) log_expz:ℂhz:|z.im| < Real.pi / 2⊢ cexp (-z * (1 / 2)) = cexp (-z / 2)hx₁z:ℂhz:|z.im| < Real.pi / 2⊢ -Real.pi < (-z).imhx₂z:ℂhz:|z.im| < Real.pi / 2⊢ (-z).im ≤ Real.pi]z:ℂhz:|z.im| < Real.pi / 2⊢ cexp (-z * (1 / 2)) = cexp (-z / 2)hx₁z:ℂhz:|z.im| < Real.pi / 2⊢ -Real.pi < (-z).imhx₂z:ℂhz:|z.im| < Real.pi / 2⊢ (-z).im ≤ Real.pi
    ·z:ℂhz:|z.im| < Real.pi / 2⊢ cexp (-z * (1 / 2)) = cexp (-z / 2) congr 1z:ℂhz:|z.im| < Real.pi / 2⊢ -z * (1 / 2) = -z / 2
      ringAll goals completed! 🐙
    ·hx₁z:ℂhz:|z.im| < Real.pi / 2⊢ -Real.pi < (-z).im simp only [neg_im]hx₁z:ℂhz:|z.im| < Real.pi / 2⊢ -Real.pi < -z.im
      linarith [(abs_lt.mp hz).2, Real.pi_pos]All goals completed! 🐙
    ·hx₂z:ℂhz:|z.im| < Real.pi / 2⊢ (-z).im ≤ Real.pi simp only [neg_im]hx₂z:ℂhz:|z.im| < Real.pi / 2⊢ -z.im ≤ Real.pi
      linarith [(abs_lt.mp hz).1, Real.pi_pos]z:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)⊢ thetaLogKernel (-z) = thetaLogKernel z
  have hi : (1 : ℂ) / exp (-z) = exp z := by rw [one_div,z:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)⊢ (cexp (-z))⁻¹ = cexp z ← exp_neg,z:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)⊢ cexp (- -z) = cexp z neg_negz:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)⊢ cexp z = cexp z]z:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp z⊢ thetaLogKernel (-z) = thetaLogKernel z
  have he := psi_inversion (exp (-z))z:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = 1 / cexp (-z) ^ (1 / 2) * (1 + 2 * psi (1 / cexp (-z)))⊢ thetaLogKernel (-z) = thetaLogKernel z
  rw [hp,z:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = 1 / cexp (-z / 2) * (1 + 2 * psi (1 / cexp (-z)))⊢ thetaLogKernel (-z) = thetaLogKernel z hi,z:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = 1 / cexp (-z / 2) * (1 + 2 * psi (cexp z))⊢ thetaLogKernel (-z) = thetaLogKernel z one_div,z:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = (cexp (-z / 2))⁻¹ * (1 + 2 * psi (cexp z))⊢ thetaLogKernel (-z) = thetaLogKernel z ← exp_negz:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = cexp (-(-z / 2)) * (1 + 2 * psi (cexp z))⊢ thetaLogKernel (-z) = thetaLogKernel z] at hez:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = cexp (-(-z / 2)) * (1 + 2 * psi (cexp z))⊢ thetaLogKernel (-z) = thetaLogKernel z
  have hm : exp (-z / 4) * exp (-(-z / 2)) = exp (z / 4) := by
    rw [← exp_addz:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = cexp (-(-z / 2)) * (1 + 2 * psi (cexp z))⊢ cexp (-z / 4 + -(-z / 2)) = cexp (z / 4)]z:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = cexp (-(-z / 2)) * (1 + 2 * psi (cexp z))⊢ cexp (-z / 4 + -(-z / 2)) = cexp (z / 4)
    congr 1z:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = cexp (-(-z / 2)) * (1 + 2 * psi (cexp z))⊢ -z / 4 + -(-z / 2) = z / 4
    ringz:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = cexp (-(-z / 2)) * (1 + 2 * psi (cexp z))hm:cexp (-z / 4) * cexp (-(-z / 2)) = cexp (z / 4)⊢ thetaLogKernel (-z) = thetaLogKernel z
  have hh := congrArg (fun w : ℂ ↦ exp (-z / 4) * w) hez:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = cexp (-(-z / 2)) * (1 + 2 * psi (cexp z))hm:cexp (-z / 4) * cexp (-(-z / 2)) = cexp (z / 4)hh:cexp (-z / 4) * (1 + 2 * psi (cexp (-z))) = cexp (-z / 4) * (cexp (-(-z / 2)) * (1 + 2 * psi (cexp z)))⊢ thetaLogKernel (-z) = thetaLogKernel z
  unfold thetaLogKernelz:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = cexp (-(-z / 2)) * (1 + 2 * psi (cexp z))hm:cexp (-z / 4) * cexp (-(-z / 2)) = cexp (z / 4)hh:cexp (-z / 4) * (1 + 2 * psi (cexp (-z))) = cexp (-z / 4) * (cexp (-(-z / 2)) * (1 + 2 * psi (cexp z)))⊢ 2 * cexp (- -z / 4) * psi (cexp (- -z)) - cexp (-z / 4) = 2 * cexp (-z / 4) * psi (cexp (-z)) - cexp (z / 4)
  simp only [neg_neg, neg_div]z:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = cexp (-(-z / 2)) * (1 + 2 * psi (cexp z))hm:cexp (-z / 4) * cexp (-(-z / 2)) = cexp (z / 4)hh:cexp (-z / 4) * (1 + 2 * psi (cexp (-z))) = cexp (-z / 4) * (cexp (-(-z / 2)) * (1 + 2 * psi (cexp z)))⊢ 2 * cexp (z / 4) * psi (cexp z) - cexp (-(z / 4)) = 2 * cexp (-(z / 4)) * psi (cexp (-z)) - cexp (z / 4)
  simp only [neg_div] at hm hhz:ℂhz:|z.im| < Real.pi / 2hp:cexp (-z) ^ (1 / 2) = cexp (-z / 2)hi:1 / cexp (-z) = cexp zhe:1 + 2 * psi (cexp (-z)) = cexp (-(-z / 2)) * (1 + 2 * psi (cexp z))hm:cexp (-(z / 4)) * cexp (- -(z / 2)) = cexp (z / 4)hh:cexp (-(z / 4)) * (1 + 2 * psi (cexp (-z))) = cexp (-(z / 4)) * (cexp (- -(z / 2)) * (1 + 2 * psi (cexp z)))⊢ 2 * cexp (z / 4) * psi (cexp z) - cexp (-(z / 4)) = 2 * cexp (-(z / 4)) * psi (cexp (-z)) - cexp (z / 4)
  linear_combination -hh - (1 + 2 * psi (exp z)) * hmAll goals completed! 🐙