Source indexedlemma · leanprover/lean4:v4.32.0

Perron.isHolomorphicOn

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:403 to 421

Mathematical statement

Exact Lean statement

@[blueprint
  "isHolomorphicOn"
  (title := "isHolomorphicOn")
  (statement := /--
  Let $x>0$. Then the function $f(s) = x^s/(s(s+1))$ is holomorphic on the half-plane
  $\{s\in\mathbb{C}:\Re(s)>0\}$.
  -/)
  (latexEnv := "lemma")]
lemma isHolomorphicOn (xpos : 0 < x) : HolomorphicOn (f x) {0, -1}ᶜ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "isHolomorphicOn"  (title := "isHolomorphicOn")  (statement := /--  Let $x>0$. Then the function $f(s) = x^s/(s(s+1))$ is holomorphic on the half-plane  $\{s\in\mathbb{C}:\Re(s)>0\}$.  -/)  (latexEnv := "lemma")]lemma isHolomorphicOn (xpos : 0 < x) : HolomorphicOn (f x) {0, -1}ᶜ := by  /-- Composition of differentiabilities. -/  unfold f  simp_rw [Complex.cpow_def_of_ne_zero <| ofReal_ne_zero.mpr <| ne_of_gt xpos]  apply DifferentiableOn.div    <| DifferentiableOn.cexp <| DifferentiableOn.const_mul differentiableOn_id _  · exact DifferentiableOn.mul differentiableOn_id      <| DifferentiableOn.add_const _ differentiableOn_id  · intro x hx    obtain ⟨h0, h1⟩ := not_or.mp hx    exact mul_ne_zero h0 <| add_ne_add_left 1 |>.mpr h1 |>.trans_eq (neg_add_cancel 1)