Theorem: verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Proof state before:
case h
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ RectangleIntegral f (↑σ - I * ↑y) (↑σ' + I * ↑y) = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
apply RectanglePullToNhdOfPole'
Proof state after:
case h.h_orientation
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ (↑σ - I * ↑y).re ≤ (↑σ' + I * ↑y).re ∧
    (↑σ - I * ↑y).im ≤ (↑σ' + I * ↑y).im ∧
      (-↑c - ↑c * I + p).re ≤ (↑c + ↑c * I + p).re ∧ (-↑c - ↑c * I + p).im ≤ (↑c + ↑c * I + p).im

case h.hp
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ Rectangle (-↑c - ↑c * I + p) (↑c + ↑c * I + p) ∈ 𝓝 ?h.p

case h.hz
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ Rectangle (-↑c - ↑c * I + p) (↑c + ↑c * I + p) ⊆ Rectangle (↑σ - I * ↑y) (↑σ' + I * ↑y)

case h.fHolo
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ HolomorphicOn f (Rectangle (↑σ - I * ↑y) (↑σ' + I * ↑y) \ {?h.p})

case h.p
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ ℂ