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

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) σ = 1 - 1 / ↑x
Tactic:
set f : ℂ → ℂ := (fun s ↦ x^s / (s * (s + 1)))
State after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ VerticalIntegral' f σ = 1 - 1 / ↑x

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ VerticalIntegral' f σ = 1 - 1 / ↑x
Tactic:
rw [residuePull1 x_gt_one σ_pos]
State after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ 1 + VerticalIntegral' (Perron.f x) (-1 / 2) = 1 - 1 / ↑x

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ 1 + VerticalIntegral' (Perron.f x) (-1 / 2) = 1 - 1 / ↑x
Tactic:
rw [residuePull2 x_gt_one]
State after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x
Tactic:
have contourPull₃ (σ' σ'' : ℝ) (hσ' : σ' ≤ -3/2) (hσ'' : σ'' ≤ -3/2) :
    VerticalIntegral' f σ' = VerticalIntegral' f σ'' :=
  contourPull3 x_gt_one hσ' hσ''
State after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x
Tactic:
have VertIntBound : ∃ C, ∀ σ' < -3/2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ' :=
  vertIntBoundLeft (by linarith : 0 < x)
State after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x
Tactic:
rw [limitOfConstantLeft (σ := -3/2) (Eq.le rfl) contourPull₃ ?_]
State after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ 1 + (-1 / ↑x + 0) = 1 - 1 / ↑x

x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ Tendsto (fun σ' => VerticalIntegral' f σ') atBot (𝓝 0)

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ 1 + (-1 / ↑x + 0) = 1 - 1 / ↑x

x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ Tendsto (fun σ' => VerticalIntegral' f σ') atBot (𝓝 0)
Tactic:
ring
State after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ Tendsto (fun σ' => VerticalIntegral' f σ') atBot (𝓝 0)

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ Tendsto (fun σ' => VerticalIntegral' f σ') atBot (𝓝 0)
Tactic:
exact tendsto_zero_iff_norm_tendsto_zero.mpr AbsVertIntTendsto
State after:
no goals

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
⊢ 0 < x
Tactic:
linarith
State after:
no goals

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
Tactic:
obtain ⟨C, hC⟩ := VertIntBound
State after:
case intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)

State before:
case intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
Tactic:
have := tendsto_rpow_atTop_nhds_zero_of_norm_gt_one x_gt_one C
State after:
case intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)

State before:
case intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds this
State after:
case intro.hgf
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in atBot, 0 ≤ (⇑Complex.abs ∘ VerticalIntegral' f) b

case intro.hfh
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in atBot, (⇑Complex.abs ∘ VerticalIntegral' f) b ≤ x ^ b * C

State before:
case intro.hgf
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in atBot, 0 ≤ (⇑Complex.abs ∘ VerticalIntegral' f) b
Tactic:
filter_upwards using fun _ ↦ Complex.abs.nonneg' _
State after:
no goals

State before:
case intro.hfh
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in atBot, (⇑Complex.abs ∘ VerticalIntegral' f) b ≤ x ^ b * C
Tactic:
filter_upwards [eventually_lt_atBot (-3/2)]
State after:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C

State before:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C
Tactic:
(conv at hC => intro σ hσ; rw [mul_comm])
State after:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ < -3 / 2, ‖VerticalIntegral' f σ‖ ≤ x ^ σ * C
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C

State before:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ < -3 / 2, ‖VerticalIntegral' f σ‖ ≤ x ^ σ * C
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C
Tactic:
exact fun _ ↦ hC _
State after:
no goals

State before:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C
Tactic:
conv at hC => intro σ hσ; rw [mul_comm]
State after:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ < -3 / 2, ‖VerticalIntegral' f σ‖ ≤ x ^ σ * C
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C