Source indexedtheorem · leanprover/lean4:v4.32.0

CH2.Phi_star.meromorphic

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1686 to 1700

Mathematical statement

Exact Lean statement

@[blueprint
  "Phi-star-mero"
  (title := "$\\Phi^{\\pm,\\ast}_\\nu$ meromorphic")
  (statement := /--
  $$\Phi^{\pm,\ast}_\nu(z)$$ is meromorphic.
  -/)
  (proof := /-- This follows from the definition of $\Phi^{\pm,\ast}_\nu$ and the properties of the $B^\pm$ function. -/), fun_prop]
theorem Phi_star.meromorphic (ν ε : ℝ) : Meromorphic (Phi_star ν ε)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "Phi-star-mero"  (title := "$\\Phi^{\\pm,\\ast}_\\nu$ meromorphic")  (statement := /--  $$\Phi^{\pm,\ast}_\nu(z)$$ is meromorphic.  -/)  (proof := /-- This follows from the definition of $\Phi^{\pm,\ast}_\nu$ and the properties of the $B^\pm$ function. -/), fun_prop]theorem Phi_star.meromorphic (ν ε : ℝ) : Meromorphic (Phi_star ν ε) := by  intro z₀  have h_comp : MeromorphicAt (fun z => B ε (-2 * Real.pi * Complex.I * z + ν)) z₀ ∧      MeromorphicAt (fun _ => B ε ν) z₀ := by    constructor    · exact (meromorphicAt_B ε _).comp_analyticAt (by fun_prop)    · exact MeromorphicAt.const (B ε ν) z₀  exact (h_comp.1.sub h_comp.2).div (MeromorphicAt.const _ z₀)