Theorem: Perron.isHolomorphicOn (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ HolomorphicOn (f x) {0, -1}ᶜ
Tactic:
unfold f
State after:
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ HolomorphicOn (fun s => ↑x ^ s / (s * (s + 1))) {0, -1}ᶜ

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ HolomorphicOn (fun s => ↑x ^ s / (s * (s + 1))) {0, -1}ᶜ
Tactic:
simp_rw [Complex.cpow_def_of_ne_zero <| ofReal_ne_zero.mpr <| ne_of_gt xpos]
State after:
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ HolomorphicOn (fun s => cexp ((↑x).log * s) / (s * (s + 1))) {0, -1}ᶜ

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ HolomorphicOn (fun s => cexp ((↑x).log * s) / (s * (s + 1))) {0, -1}ᶜ
Tactic:
apply DifferentiableOn.div <| DifferentiableOn.cexp <| DifferentiableOn.const_mul differentiableOn_id _
State after:
case hd
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ DifferentiableOn ℂ (fun x => x * (x + 1)) {0, -1}ᶜ

case hx
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ ∀ x ∈ {0, -1}ᶜ, x * (x + 1) ≠ 0

State before:
case hd
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ DifferentiableOn ℂ (fun x => x * (x + 1)) {0, -1}ᶜ
Tactic:
exact DifferentiableOn.mul differentiableOn_id <| DifferentiableOn.add_const differentiableOn_id 1
State after:
no goals

State before:
case hx
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ ∀ x ∈ {0, -1}ᶜ, x * (x + 1) ≠ 0
Tactic:
intro x hx
State after:
case hx
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
x : ℂ
hx : x ∈ {0, -1}ᶜ
⊢ x * (x + 1) ≠ 0

State before:
case hx
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
x : ℂ
hx : x ∈ {0, -1}ᶜ
⊢ x * (x + 1) ≠ 0
Tactic:
obtain ⟨h0, h1⟩ := not_or.mp hx
State after:
case hx.intro
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
x : ℂ
hx : x ∈ {0, -1}ᶜ
h0 : ¬x = 0
h1 : x ∉ {-1}
⊢ x * (x + 1) ≠ 0

State before:
case hx.intro
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
x : ℂ
hx : x ∈ {0, -1}ᶜ
h0 : ¬x = 0
h1 : x ∉ {-1}
⊢ x * (x + 1) ≠ 0
Tactic:
exact mul_ne_zero h0 <| add_ne_add_left 1 |>.mpr h1 |>.trans_eq (add_left_neg 1)
State after:
no goals