Theorem: Perron.residueAtNegOne
Proof state before:
case h.intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) \ {-1})
f1Holo : HolomorphicOn (f x - fun s => -↑x⁻¹ / (s + 1)) (Square (-1) c \ {-1})
RectMemNhds : Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) ∈ 𝓝 (-1)
g : ℂ → ℂ
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1))
g_eq_fDiff : EqOn (f x - fun s => -↑x⁻¹ / (s + 1)) g (Square (-1) c \ {-1})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I - 1) (↑c + ↑c * I - 1) = -↑x⁻¹
Tactic:
refine ResidueTheoremOnRectangleWithSimplePole ?_ ?_ RectMemNhds gHolo ?_
Proof state after:
case h.intro.intro.intro.refine_1
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) \ {-1})
f1Holo : HolomorphicOn (f x - fun s => -↑x⁻¹ / (s + 1)) (Square (-1) c \ {-1})
RectMemNhds : Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) ∈ 𝓝 (-1)
g : ℂ → ℂ
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1))
g_eq_fDiff : EqOn (f x - fun s => -↑x⁻¹ / (s + 1)) g (Square (-1) c \ {-1})
⊢ (-↑c - ↑c * I - 1).re ≤ (↑c + ↑c * I - 1).re

case h.intro.intro.intro.refine_2
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) \ {-1})
f1Holo : HolomorphicOn (f x - fun s => -↑x⁻¹ / (s + 1)) (Square (-1) c \ {-1})
RectMemNhds : Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) ∈ 𝓝 (-1)
g : ℂ → ℂ
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1))
g_eq_fDiff : EqOn (f x - fun s => -↑x⁻¹ / (s + 1)) g (Square (-1) c \ {-1})
⊢ (-↑c - ↑c * I - 1).im ≤ (↑c + ↑c * I - 1).im

case h.intro.intro.intro.refine_3
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) \ {-1})
f1Holo : HolomorphicOn (f x - fun s => -↑x⁻¹ / (s + 1)) (Square (-1) c \ {-1})
RectMemNhds : Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) ∈ 𝓝 (-1)
g : ℂ → ℂ
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1))
g_eq_fDiff : EqOn (f x - fun s => -↑x⁻¹ / (s + 1)) g (Square (-1) c \ {-1})
⊢ EqOn (f x - fun s => -↑x⁻¹ / (s - -1)) g (Rectangle (-↑c - ↑c * I - 1) (↑c + ↑c * I - 1) \ {-1})