Theorem: ResidueTheoremInRectangle (PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
⊢ RectangleIntegral' (fun s => c / (s - p)) z w = c
Tactic:
simp only [rectangle_mem_nhds_iff, uIoo_of_le zRe_le_wRe, uIoo_of_le zIm_le_wIm, mem_reProdIm,
  mem_Ioo] at pInRectInterior
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
⊢ RectangleIntegral' (fun s => c / (s - p)) z w = c

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
⊢ RectangleIntegral' (fun s => c / (s - p)) z w = c
Tactic:
rw [RectangleIntegral.translate', RectangleIntegral']
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
⊢ (1 / (2 * ↑π * I)) • RectangleIntegral (HDiv.hDiv c) (z - p) (w - p) = c

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
⊢ (1 / (2 * ↑π * I)) • RectangleIntegral (HDiv.hDiv c) (z - p) (w - p) = c
Tactic:
have : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c := by field_simp [two_pi_I_ne_zero] ; ring
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ (1 / (2 * ↑π * I)) • RectangleIntegral (HDiv.hDiv c) (z - p) (w - p) = c

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ (1 / (2 * ↑π * I)) • RectangleIntegral (HDiv.hDiv c) (z - p) (w - p) = c
Tactic:
rwa [ResidueTheoremAtOrigin']
State after:
case h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ (z - p).re < 0

case h2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ (z - p).im < 0

case h3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ 0 < (w - p).re

case h4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ 0 < (w - p).im

State before:
case h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ (z - p).re < 0

case h2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ (z - p).im < 0

case h3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ 0 < (w - p).re

case h4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ 0 < (w - p).im
Tactic:
all_goals { simp [*] }
State after:
no goals

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
⊢ 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
Tactic:
field_simp [two_pi_I_ne_zero]
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
⊢ 2 * I * ↑π * c = c * (2 * ↑π * I)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
⊢ 2 * I * ↑π * c = c * (2 * ↑π * I)
Tactic:
ring
State after:
no goals

State before:
case h4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ 0 < (w - p).im
Tactic:
simp [*]
State after:
no goals