internlm/Lean-Github huggingface dataset:
Theorem: ResidueTheoremAtOrigin'
Proof 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * 2⁻¹ + -(c * ↑(w.re ^ 2 + z.im ^ 2).log * I * I * (-1 / 2)) +
                          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
                        (-(c * ↑(z.im ^ 2 + z.re ^ 2).log * I * I * 2⁻¹) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                      c * I * ↑(z.re * z.im⁻¹).arctan +
                    -(c * I * ↑(w.re ^ 2 + w.im ^ 2).log * I * 2⁻¹) +
                  -(c * I * ↑(z.re ^ 2 + w.im ^ 2).log * I * (-1 / 2)) +
                c * I * ↑(w.re * w.im⁻¹).arctan +
              (-(c * I * ↑(z.re * w.im⁻¹).arctan) + c * 1 * I * ↑(w.im * w.re⁻¹).arctan) +
            -(c * 1 * I * ↑(z.im * w.re⁻¹).arctan) +
          (-(c * 1 * I * ↑(w.im * z.re⁻¹).arctan) + c * 1 * I * ↑(z.im * z.re⁻¹).arctan) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * 2⁻¹ =
    c * I * ↑π * 2
Tactic:
rw [l1, l3, l4, l6, r1, r3, r4, r6]
Proof 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * 2⁻¹ + -(c * ↑(w.re ^ 2 + z.im ^ 2).log * I * I * (-1 / 2)) +
                          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
                        (-(c * ↑(z.im ^ 2 + z.re ^ 2).log * I * I * 2⁻¹) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                      c * I * ↑(z.re * z.im⁻¹).arctan +
                    -(c * I * ↑(w.re ^ 2 + w.im ^ 2).log * I * 2⁻¹) +
                  -(c * I * ↑(z.re ^ 2 + w.im ^ 2).log * I * (-1 / 2)) +
                c * I * ↑(w.re * w.im⁻¹).arctan +
              (-(c * I * ↑(z.re * w.im⁻¹).arctan) + c * 1 * I * ↑(π / 2 - (w.re * w.im⁻¹).arctan)) +
            -(c * 1 * I * ↑(-(π / 2) - (w.re * z.im⁻¹).arctan)) +
          (-(c * 1 * I * ↑(-(π / 2) - (z.re * w.im⁻¹).arctan)) + c * 1 * I * ↑(π / 2 - (z.re * z.im⁻¹).arctan)) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * 2⁻¹ =
    c * I * ↑π * 2
Theorem: ResidueTheoremAtOrigin'
Proof 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * 2⁻¹ + -(c * ↑(w.re ^ 2 + z.im ^ 2).log * I * I * (-1 / 2)) +
                          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
                        (-(c * ↑(z.im ^ 2 + z.re ^ 2).log * I * I * 2⁻¹) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                      c * I * ↑(z.re * z.im⁻¹).arctan +
                    -(c * I * ↑(w.re ^ 2 + w.im ^ 2).log * I * 2⁻¹) +
                  -(c * I * ↑(z.re ^ 2 + w.im ^ 2).log * I * (-1 / 2)) +
                c * I * ↑(w.re * w.im⁻¹).arctan +
              (-(c * I * ↑(z.re * w.im⁻¹).arctan) + c * 1 * I * ↑(π / 2 - (w.re * w.im⁻¹).arctan)) +
            -(c * 1 * I * ↑(-(π / 2) - (w.re * z.im⁻¹).arctan)) +
          (-(c * 1 * I * ↑(-(π / 2) - (z.re * w.im⁻¹).arctan)) + c * 1 * I * ↑(π / 2 - (z.re * z.im⁻¹).arctan)) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * 2⁻¹ =
    c * I * ↑π * 2
Tactic:
ring_nf
Proof 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * (1 / 2) +
                            (c * ↑(w.re ^ 2 + z.im ^ 2).log * I ^ 2 * (1 / 2) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                          c * I * ↑(z.re * z.im⁻¹).arctan +
                        (c * I * ↑(w.re * w.im⁻¹).arctan - c * I * ↑(z.re * w.im⁻¹).arctan) +
                      c * I * ↑(π * (1 / 2) - (w.re * w.im⁻¹).arctan) +
                    (-(c * I * ↑(π * (-1 / 2) - (w.re * z.im⁻¹).arctan)) -
                      c * I * ↑(π * (-1 / 2) - (z.re * w.im⁻¹).arctan)) +
                  c * I * ↑(π * (1 / 2) - (z.re * z.im⁻¹).arctan) +
                c * I ^ 2 * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
              c * I ^ 2 * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
            c * I ^ 2 * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) +
          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) =
    c * I * ↑π * 2
Theorem: ResidueTheoremAtOrigin'
Proof 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * (1 / 2) +
                            (c * ↑(w.re ^ 2 + z.im ^ 2).log * -1 * (1 / 2) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                          c * I * ↑(z.re * z.im⁻¹).arctan +
                        (c * I * ↑(w.re * w.im⁻¹).arctan - c * I * ↑(z.re * w.im⁻¹).arctan) +
                      c * I * (↑π * (1 / 2) - ↑(w.re * w.im⁻¹).arctan) +
                    (-(c * I * (↑π * (-1 / 2) - ↑(w.re * z.im⁻¹).arctan)) -
                      c * I * (↑π * (-1 / 2) - ↑(z.re * w.im⁻¹).arctan)) +
                  c * I * (↑π * (1 / 2) - ↑(z.re * z.im⁻¹).arctan) +
                c * -1 * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
              c * -1 * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
            c * -1 * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) +
          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) =
    c * I * ↑π * 2
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin'
Proof 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
⊢ z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
Tactic:
group
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin'
Proof 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
⊢ w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
Tactic:
group
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin'
Proof 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
⊢ z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
Tactic:
group
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin'
Proof 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
⊢ w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
Tactic:
group
Proof state after:
no goals
Theorem: ResidueTheoremInRectangle
Proof 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
Proof 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
Theorem: ResidueTheoremInRectangle
Proof 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']
Proof 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
Theorem: ResidueTheoremInRectangle
Proof 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
Proof 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
Theorem: ResidueTheoremInRectangle
Proof 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']
Proof 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
Theorem: ResidueTheoremInRectangle
Proof 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 [*] }
Proof state after:
no goals
Theorem: ResidueTheoremInRectangle
Proof 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]
Proof 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)
Theorem: ResidueTheoremInRectangle
Proof 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
Proof state after:
no goals
Theorem: ResidueTheoremInRectangle
Proof 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 [*]
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin
Proof 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₂ σ : ℝ
⊢ RectangleIntegral' (fun s => 1 / s) (-1 - I) (1 + I) = 1
Tactic:
rw [RectangleIntegral', ResidueTheoremAtOrigin']
Proof 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₂ σ : ℝ
⊢ (1 / (2 * ↑π * I)) • (2 * I * ↑π * 1) = 1

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₂ σ : ℝ
⊢ (-1 - I).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₂ σ : ℝ
⊢ (-1 - I).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₂ σ : ℝ
⊢ 0 < (1 + I).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₂ σ : ℝ
⊢ 0 < (1 + I).im
Theorem: ResidueTheoremAtOrigin
Proof 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₂ σ : ℝ
⊢ (1 / (2 * ↑π * I)) • (2 * I * ↑π * 1) = 1

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₂ σ : ℝ
⊢ (-1 - I).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₂ σ : ℝ
⊢ (-1 - I).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₂ σ : ℝ
⊢ 0 < (1 + I).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₂ σ : ℝ
⊢ 0 < (1 + I).im
Tactic:
all_goals { field_simp [pi_ne_zero] <;> ring }
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin
Proof 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₂ σ : ℝ
⊢ 0 < (1 + I).im
Tactic:
field_simp [pi_ne_zero] <;> ring
Proof state after:
no goals
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof 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₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
⊢ RectangleIntegral' f z w = A
Tactic:
have principalPart' : Set.EqOn f (g + (fun s ↦ A / (s - p))) (Rectangle z w \ {p}) :=
  fun s hs => by rw [Pi.add_apply, ← principalPart hs, Pi.sub_apply, sub_add_cancel]
Proof 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₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
⊢ RectangleIntegral' f z w = A
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof 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₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
⊢ RectangleIntegral' f z w = A
Tactic:
have : Set.EqOn f (g + (fun s ↦ A / (s - p))) (RectangleBorder z w) :=
  principalPart'.mono <| Set.subset_diff.mpr ⟨rectangleBorder_subset_rectangle z w,
    disjoint_singleton_right.mpr (not_mem_rectangleBorder_of_rectangle_mem_nhds pInRectInterior)⟩
Proof 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₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
⊢ RectangleIntegral' f z w = A
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof 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₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
⊢ RectangleIntegral' f z w = A
Tactic:
rw [RectangleIntegral'_congr this]
Proof 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₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
⊢ RectangleIntegral' (g + fun s => A / (s - p)) z w = A
Theorem: ResidueTheoremOnRectangleWithSimplePole
Proof 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₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
⊢ RectangleIntegral' (g + fun s => A / (s - p)) z w = A
Tactic:
have t1 : RectangleBorderIntegrable g z w := gHolo.rectangleBorderIntegrable
Proof 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₂ σ : ℝ
f g : ℂ → ℂ
z w p A : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
gHolo : HolomorphicOn g (Rectangle z w)
principalPart : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
⊢ RectangleIntegral' (g + fun s => A / (s - p)) z w = A