internlm/Lean-Github huggingface dataset:
Theorem: integral_const_div_self_add_im
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₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * I) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)
Tactic:
have e3 : IntervalIntegrable (fun x ↦ A * I * y / (x ^ 2 + y ^ 2)) volume x₁ x₂ := by
  apply Continuous.intervalIntegrable
  refine continuous_const.div (by continuity) (λ x => ?_)
  norm_cast ; exact sq_add_sq_ne_zero hy
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₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * I) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)
Theorem: integral_const_div_self_add_im
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₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * I) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)
Tactic:
simp_rw [integral_congr (λ _ _ => e1), integral_sub e2 e3, mul_div_assoc]
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₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ (∫ (x : ℝ) in x₁..x₂, A * (↑x / (↑x ^ 2 + ↑y ^ 2))) - ∫ (x : ℝ) in x₁..x₂, A * I * (↑y / (↑x ^ 2 + ↑y ^ 2)) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)
Theorem: integral_const_div_self_add_im
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₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ (∫ (x : ℝ) in x₁..x₂, A * (↑x / (↑x ^ 2 + ↑y ^ 2))) - ∫ (x : ℝ) in x₁..x₂, A * I * (↑y / (↑x ^ 2 + ↑y ^ 2)) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)
Tactic:
norm_cast
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₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ (∫ (x : ℝ) in x₁..x₂, A * ↑(x / (x ^ 2 + y ^ 2))) - ∫ (x : ℝ) in x₁..x₂, A * I * ↑(y / (x ^ 2 + y ^ 2)) =
    A * ↑((x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2) - A * I * ↑((x₂ / y).arctan - (x₁ / y).arctan)
Theorem: integral_const_div_self_add_im
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₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ (∫ (x : ℝ) in x₁..x₂, A * ↑(x / (x ^ 2 + y ^ 2))) - ∫ (x : ℝ) in x₁..x₂, A * I * ↑(y / (x ^ 2 + y ^ 2)) =
    A * ↑((x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2) - A * I * ↑((x₂ / y).arctan - (x₁ / y).arctan)
Tactic:
simp_rw [integral_const_mul, intervalIntegral.integral_ofReal, integral_self_div_sq_add_sq hy,
  integral_const_div_sq_add_sq hy]
Proof state after:
no goals
Theorem: integral_const_div_self_add_im
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₂ σ : ℝ
hy : y ≠ 0
x : ℝ
⊢ A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 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₂ σ : ℝ
hy : y ≠ 0
x : ℝ
⊢ A * (↑x + ↑y * I)⁻¹ = A * ↑x * (↑x ^ 2 + ↑y ^ 2)⁻¹ - A * ↑y * I * (↑x ^ 2 + ↑y ^ 2)⁻¹
Theorem: integral_const_div_self_add_im
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₂ σ : ℝ
hy : y ≠ 0
x : ℝ
⊢ A * (↑x + ↑y * I)⁻¹ = A * ↑x * (↑x ^ 2 + ↑y ^ 2)⁻¹ - A * ↑y * I * (↑x ^ 2 + ↑y ^ 2)⁻¹
Tactic:
simp_rw [inv_re_add_im]
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₂ σ : ℝ
hy : y ≠ 0
x : ℝ
⊢ A * ((↑x - I * ↑y) / (↑x ^ 2 + ↑y ^ 2)) = A * ↑x * (↑x ^ 2 + ↑y ^ 2)⁻¹ - A * ↑y * I * (↑x ^ 2 + ↑y ^ 2)⁻¹
Theorem: integral_const_div_self_add_im
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₂ σ : ℝ
hy : y ≠ 0
x : ℝ
⊢ A * ((↑x - I * ↑y) / (↑x ^ 2 + ↑y ^ 2)) = A * ↑x * (↑x ^ 2 + ↑y ^ 2)⁻¹ - A * ↑y * I * (↑x ^ 2 + ↑y ^ 2)⁻¹
Tactic:
ring
Proof state after:
no goals
Theorem: integral_const_div_self_add_im
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₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
Tactic:
apply Continuous.intervalIntegrable
Proof state after:
case hu
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ Continuous fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)
Theorem: integral_const_div_self_add_im
Proof state before:
case hu
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ Continuous fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)
Tactic:
simp_rw [mul_div_assoc]
Proof state after:
case hu
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ Continuous fun x => A * (↑x / (↑x ^ 2 + ↑y ^ 2))
Theorem: integral_const_div_self_add_im
Proof state before:
case hu
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ Continuous fun x => A * (↑x / (↑x ^ 2 + ↑y ^ 2))
Tactic:
norm_cast
Proof state after:
case hu
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ Continuous fun x => A * ↑(x / (x ^ 2 + y ^ 2))
Theorem: integral_const_div_self_add_im
Proof state before:
case hu
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ Continuous fun x => A * ↑(x / (x ^ 2 + y ^ 2))
Tactic:
exact continuous_const.mul <| continuous_ofReal.comp <| continuous_self_div_sq_add_sq hy
Proof state after:
no goals
Theorem: integral_const_div_self_add_im
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₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
Tactic:
apply Continuous.intervalIntegrable
Proof state after:
case hu
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ Continuous fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
Theorem: integral_const_div_self_add_im
Proof state before:
case hu
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ Continuous fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
Tactic:
refine continuous_const.div (by continuity) (λ x => ?_)
Proof state after:
case hu
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x✝ x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
x : ℝ
⊢ ↑x ^ 2 + ↑y ^ 2 ≠ 0
Theorem: integral_const_div_self_add_im
Proof state before:
case hu
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x✝ x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
x : ℝ
⊢ ↑x ^ 2 + ↑y ^ 2 ≠ 0
Tactic:
norm_cast
Proof state after:
case hu
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x✝ x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
x : ℝ
⊢ ¬x ^ 2 + y ^ 2 = 0
Theorem: integral_const_div_self_add_im
Proof state before:
case hu
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x✝ x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
x : ℝ
⊢ ¬x ^ 2 + y ^ 2 = 0
Tactic:
exact sq_add_sq_ne_zero hy
Proof state after:
no goals
Theorem: integral_const_div_self_add_im
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₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ Continuous fun x => ↑x ^ 2 + ↑y ^ 2
Tactic:
continuity
Proof state after:
no goals
Theorem: integral_const_div_re_add_self
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₂ σ : ℝ
hx : x ≠ 0
⊢ ∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * I) =
    A / I * (↑(y₂ ^ 2 + (-x) ^ 2).log / 2 - ↑(y₁ ^ 2 + (-x) ^ 2).log / 2) -
      A / I * I * (↑(y₂ / -x).arctan - ↑(y₁ / -x).arctan)
Tactic:
have l1 {y : ℝ} : A / (x + y * I) = A / I / (y + ↑(-x) * I) := by
  have e1 : x + y * I ≠ 0 := by contrapose! hx ; simpa using congr_arg re hx
  have e2 : y + -(x * I) ≠ 0 := by contrapose! hx ; simpa using congr_arg im hx
  field_simp ; ring_nf ; simp
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₂ σ : ℝ
hx : x ≠ 0
l1 : ∀ {y : ℝ}, A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
⊢ ∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * I) =
    A / I * (↑(y₂ ^ 2 + (-x) ^ 2).log / 2 - ↑(y₁ ^ 2 + (-x) ^ 2).log / 2) -
      A / I * I * (↑(y₂ / -x).arctan - ↑(y₁ / -x).arctan)
Theorem: integral_const_div_re_add_self
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₂ σ : ℝ
hx : x ≠ 0
l1 : ∀ {y : ℝ}, A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
⊢ ∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * I) =
    A / I * (↑(y₂ ^ 2 + (-x) ^ 2).log / 2 - ↑(y₁ ^ 2 + (-x) ^ 2).log / 2) -
      A / I * I * (↑(y₂ / -x).arctan - ↑(y₁ / -x).arctan)
Tactic:
have l2 : -x ≠ 0 := by rwa [neg_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₂ σ : ℝ
hx : x ≠ 0
l1 : ∀ {y : ℝ}, A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
l2 : -x ≠ 0
⊢ ∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * I) =
    A / I * (↑(y₂ ^ 2 + (-x) ^ 2).log / 2 - ↑(y₁ ^ 2 + (-x) ^ 2).log / 2) -
      A / I * I * (↑(y₂ / -x).arctan - ↑(y₁ / -x).arctan)
Theorem: integral_const_div_re_add_self
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₂ σ : ℝ
hx : x ≠ 0
l1 : ∀ {y : ℝ}, A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
l2 : -x ≠ 0
⊢ ∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * I) =
    A / I * (↑(y₂ ^ 2 + (-x) ^ 2).log / 2 - ↑(y₁ ^ 2 + (-x) ^ 2).log / 2) -
      A / I * I * (↑(y₂ / -x).arctan - ↑(y₁ / -x).arctan)
Tactic:
simp_rw [l1, integral_const_div_self_add_im l2]
Proof state after:
no goals
Theorem: integral_const_div_re_add_self
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
⊢ A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
Tactic:
have e1 : x + y * I ≠ 0 := by contrapose! hx ; simpa using congr_arg re hx
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
⊢ A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
Theorem: integral_const_div_re_add_self
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
⊢ A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
Tactic:
have e2 : y + -(x * I) ≠ 0 := by contrapose! hx ; simpa using congr_arg im hx
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
e2 : ↑y + -(↑x * I) ≠ 0
⊢ A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
Theorem: integral_const_div_re_add_self
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
e2 : ↑y + -(↑x * I) ≠ 0
⊢ A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
Tactic:
field_simp
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
e2 : ↑y + -(↑x * I) ≠ 0
⊢ A * (↑y + -(↑x * I)) = -(A * I * (↑x + ↑y * I))
Theorem: integral_const_div_re_add_self
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
e2 : ↑y + -(↑x * I) ≠ 0
⊢ A * (↑y + -(↑x * I)) = -(A * I * (↑x + ↑y * I))
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
e2 : ↑y + -(↑x * I) ≠ 0
⊢ A * ↑y - A * ↑x * I = -(A * ↑y * I ^ 2) - A * ↑x * I
Theorem: integral_const_div_re_add_self
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
e2 : ↑y + -(↑x * I) ≠ 0
⊢ A * ↑y - A * ↑x * I = -(A * ↑y * I ^ 2) - A * ↑x * I
Tactic:
simp
Proof state after:
no goals
Theorem: integral_const_div_re_add_self
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
⊢ ↑x + ↑y * I ≠ 0
Tactic:
contrapose! hx
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₂ σ y : ℝ
hx : ↑x + ↑y * I = 0
⊢ x = 0
Theorem: integral_const_div_re_add_self
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₂ σ y : ℝ
hx : ↑x + ↑y * I = 0
⊢ x = 0
Tactic:
simpa using congr_arg re hx
Proof state after:
no goals
Theorem: integral_const_div_re_add_self
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
⊢ ↑y + -(↑x * I) ≠ 0
Tactic:
contrapose! hx
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₂ σ y : ℝ
e1 : ↑x + ↑y * I ≠ 0
hx : ↑y + -(↑x * I) = 0
⊢ x = 0
Theorem: integral_const_div_re_add_self
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₂ σ y : ℝ
e1 : ↑x + ↑y * I ≠ 0
hx : ↑y + -(↑x * I) = 0
⊢ x = 0
Tactic:
simpa using congr_arg im hx
Proof state after:
no goals
Theorem: integral_const_div_re_add_self
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₂ σ : ℝ
hx : x ≠ 0
l1 : ∀ {y : ℝ}, A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
⊢ -x ≠ 0
Tactic:
rwa [neg_ne_zero]
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
⊢ RectangleIntegral (fun s => c / s) z w = 2 * I * ↑π * c
Tactic:
simp only [RectangleIntegral, HIntegral, VIntegral, smul_eq_mul]
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
⊢ (((∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑w.im * I)) +
        I * ∫ (y : ℝ) in z.im..w.im, c / (↑w.re + ↑y * I)) -
      I * ∫ (y : ℝ) in z.im..w.im, c / (↑z.re + ↑y * I) =
    2 * I * ↑π * c
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
⊢ (((∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑w.im * I)) +
        I * ∫ (y : ℝ) in z.im..w.im, c / (↑w.re + ↑y * I)) -
      I * ∫ (y : ℝ) in z.im..w.im, c / (↑z.re + ↑y * I) =
    2 * I * ↑π * c
Tactic:
rw [integral_const_div_re_add_self h1.ne, integral_const_div_re_add_self h3.ne.symm]
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
⊢ ((∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑w.im * I)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
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
⊢ ((∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑w.im * I)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
Tactic:
rw [integral_const_div_self_add_im h2.ne, integral_const_div_self_add_im h4.ne.symm]
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
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
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
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
Tactic:
have l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹ := by group
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⁻¹)⁻¹
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c