internlm/Lean-Github huggingface dataset:
Theorem: RectanglePullToNhdOfPole
Proof state before:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f g : ℂ → E
z✝ w✝ p✝ c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
inst✝ : CompleteSpace E
z w p : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
cpos : 0 < c
right✝ : c < 1
hc : Square p c ⊆ Rectangle z w
⊢ RectangleIntegral f z w = RectangleIntegral f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)
Tactic:
simp_rw [mul_comm I]
Proof state after:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f g : ℂ → E
z✝ w✝ p✝ c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
inst✝ : CompleteSpace E
z w p : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
cpos : 0 < c
right✝ : c < 1
hc : Square p c ⊆ Rectangle z w
⊢ RectangleIntegral f z w = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Theorem: RectanglePullToNhdOfPole
Proof state before:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f g : ℂ → E
z✝ w✝ p✝ c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
inst✝ : CompleteSpace E
z w p : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
cpos : 0 < c
right✝ : c < 1
hc : Square p c ⊆ Rectangle z w
⊢ RectangleIntegral f z w = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
exact RectanglePullToNhdOfPole' (by simp_all [cpos.le])
  (square_mem_nhds p (ne_of_gt cpos)) hc fHolo
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole
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₂ σ : ℝ
inst✝ : CompleteSpace E
z w p : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
cpos : 0 < c
right✝ : c < 1
hc : Square p c ⊆ Rectangle z w
⊢ z.re ≤ w.re ∧
    z.im ≤ w.im ∧ (-↑c - ↑c * I + p).re ≤ (↑c + ↑c * I + p).re ∧ (-↑c - ↑c * I + p).im ≤ (↑c + ↑c * I + p).im
Tactic:
simp_all [cpos.le]
Proof state after:
no goals
Theorem: RectanglePullToNhdOfPole''
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₂ σ : ℝ
inst✝ : CompleteSpace E
z w p : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, RectangleIntegral' f z w = RectangleIntegral' f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)
Tactic:
filter_upwards [RectanglePullToNhdOfPole zRe_le_wRe zIm_le_wIm pInRectInterior fHolo] with c h
Proof state after:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f g : ℂ → E
z✝ w✝ p✝ c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
inst✝ : CompleteSpace E
z w p : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
h : RectangleIntegral f z w = RectangleIntegral f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)
⊢ RectangleIntegral' f z w = RectangleIntegral' f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)
Theorem: RectanglePullToNhdOfPole''
Proof state before:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f g : ℂ → E
z✝ w✝ p✝ c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
inst✝ : CompleteSpace E
z w p : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
h : RectangleIntegral f z w = RectangleIntegral f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)
⊢ RectangleIntegral' f z w = RectangleIntegral' f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)
Tactic:
simp_rw [RectangleIntegral', h]
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin_aux1c
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₂ σ a b : ℝ
⊢ ContinuousOn (fun y => ↑y + I) [[a, b]]
Tactic:
fun_prop
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin_aux1c
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₂ σ a b : ℝ
⊢ ∀ x ∈ [[a, b]], ↑x + I ≠ 0
Tactic:
simp [Complex.ext_iff]
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin_aux1c'
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₂ σ a b : ℝ
⊢ ContinuousOn (fun y => ↑y - I) [[a, b]]
Tactic:
fun_prop
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin_aux1c'
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₂ σ a b : ℝ
⊢ ∀ x ∈ [[a, b]], ↑x - I ≠ 0
Tactic:
simp [Complex.ext_iff]
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin_aux2c
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₂ σ a b : ℝ
⊢ ContinuousOn (fun y => 1 + ↑y * I) [[a, b]]
Tactic:
fun_prop
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin_aux2c
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₂ σ a b : ℝ
⊢ ∀ x ∈ [[a, b]], 1 + ↑x * I ≠ 0
Tactic:
simp [Complex.ext_iff]
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin_aux2c'
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₂ σ a b : ℝ
⊢ ContinuousOn (fun y => -1 + ↑y * I) [[a, b]]
Tactic:
fun_prop
Proof state after:
no goals
Theorem: ResidueTheoremAtOrigin_aux2c'
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₂ σ a b : ℝ
⊢ ∀ x ∈ [[a, b]], -1 + ↑x * I ≠ 0
Tactic:
simp [Complex.ext_iff]
Proof state after:
no goals
Theorem: RectangleIntegral.const_smul
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 : ℂ → E
z w c : ℂ
⊢ RectangleIntegral (fun s => c • f s) z w = c • RectangleIntegral f z w
Tactic:
simp [RectangleIntegral, HIntegral, VIntegral, smul_add, smul_sub, smul_smul, mul_comm]
Proof state after:
no goals
Theorem: RectangleIntegral.const_mul'
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 : ℂ → E
z w c : ℂ
⊢ RectangleIntegral' (fun s => c • f s) z w = c • RectangleIntegral' f z w
Tactic:
simp [RectangleIntegral', RectangleIntegral.const_smul, smul_smul]
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 : ℂ → E
z w c : ℂ
⊢ (I * ((↑π)⁻¹ * 2⁻¹) * c) • RectangleIntegral (fun s => f s) z w = (c * (I * ((↑π)⁻¹ * 2⁻¹))) • RectangleIntegral f z w
Theorem: RectangleIntegral.const_mul'
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 : ℂ → E
z w c : ℂ
⊢ (I * ((↑π)⁻¹ * 2⁻¹) * c) • RectangleIntegral (fun s => f s) z w = (c * (I * ((↑π)⁻¹ * 2⁻¹))) • RectangleIntegral f z w
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RectangleIntegral.translate
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 : ℂ → E
z w p : ℂ
⊢ RectangleIntegral (fun s => f (s - p)) z w = RectangleIntegral f (z - p) (w - p)
Tactic:
simp_rw [RectangleIntegral, HIntegral, VIntegral, sub_re, sub_im, ← intervalIntegral.integral_comp_sub_right]
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 : ℂ → E
z w p : ℂ
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I - p)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I - p)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I - p)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I - p) =
    (((∫ (x : ℝ) in z.re..w.re, f (↑(x - p.re) + ↑(z.im - p.im) * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(x - p.re) + ↑(w.im - p.im) * I)) +
        I • ∫ (x : ℝ) in z.im..w.im, f (↑(w.re - p.re) + ↑(x - p.im) * I)) -
      I • ∫ (x : ℝ) in z.im..w.im, f (↑(z.re - p.re) + ↑(x - p.im) * I)
Theorem: RectangleIntegral.translate
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 : ℂ → E
z w p : ℂ
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I - p)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I - p)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I - p)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I - p) =
    (((∫ (x : ℝ) in z.re..w.re, f (↑(x - p.re) + ↑(z.im - p.im) * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(x - p.re) + ↑(w.im - p.im) * I)) +
        I • ∫ (x : ℝ) in z.im..w.im, f (↑(w.re - p.re) + ↑(x - p.im) * I)) -
      I • ∫ (x : ℝ) in z.im..w.im, f (↑(z.re - p.re) + ↑(x - p.im) * I)
Tactic:
congr <;> ext <;> congr 1 <;> simp [Complex.ext_iff]
Proof state after:
no goals
Theorem: RectangleIntegral.translate'
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 : ℂ → E
z w p : ℂ
⊢ RectangleIntegral' (fun s => f (s - p)) z w = RectangleIntegral' f (z - p) (w - p)
Tactic:
simp_rw [RectangleIntegral', RectangleIntegral.translate]
Proof state after:
no goals
Theorem: Complex.inv_re_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₂ σ : ℝ
⊢ (↑x + ↑y * I)⁻¹ = (↑x - I * ↑y) / (↑x ^ 2 + ↑y ^ 2)
Tactic:
rw [Complex.inv_def, div_eq_mul_inv]
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₂ σ : ℝ
⊢ (starRingEnd ℂ) (↑x + ↑y * I) * ↑(normSq (↑x + ↑y * I))⁻¹ = (↑x - I * ↑y) * (↑x ^ 2 + ↑y ^ 2)⁻¹
Theorem: Complex.inv_re_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₂ σ : ℝ
⊢ (starRingEnd ℂ) (↑x + ↑y * I) * ↑(normSq (↑x + ↑y * I))⁻¹ = (↑x - I * ↑y) * (↑x ^ 2 + ↑y ^ 2)⁻¹
Tactic:
congr <;> simp [conj_ofReal, normSq] <;> ring
Proof state after:
no goals
Theorem: sq_add_sq_ne_zero
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 ^ 2 + y ^ 2 ≠ 0
Tactic:
linarith [sq_nonneg x, sq_pos_iff.mpr hy]
Proof state after:
no goals
Theorem: integral_self_div_sq_add_sq
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 : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Tactic:
let f (x : ℝ) : ℝ := Real.log (x ^ 2 + y ^ 2) / 2
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
⊢ ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Theorem: integral_self_div_sq_add_sq
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
⊢ ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Tactic:
have e1 {x} := HasDerivAt.add_const (by simpa using hasDerivAt_pow 2 x) (y ^ 2)
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
⊢ ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Theorem: integral_self_div_sq_add_sq
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
⊢ ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Tactic:
have e2 {x} : HasDerivAt f (x / (x ^ 2 + y ^ 2)) x := by
  convert (e1.log (sq_add_sq_ne_zero hy)).div_const 2 using 1 ; field_simp ; 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₂ σ : ℝ
hy : y ≠ 0
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
e2 : ∀ {x : ℝ}, HasDerivAt f (x / (x ^ 2 + y ^ 2)) x
⊢ ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Theorem: integral_self_div_sq_add_sq
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
e2 : ∀ {x : ℝ}, HasDerivAt f (x / (x ^ 2 + y ^ 2)) x
⊢ ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Tactic:
have e3 : deriv f = λ x => x / (x ^ 2 + y ^ 2) := funext (λ _ => e2.deriv)
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
e2 : ∀ {x : ℝ}, HasDerivAt f (x / (x ^ 2 + y ^ 2)) x
e3 : deriv f = fun x => x / (x ^ 2 + y ^ 2)
⊢ ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Theorem: integral_self_div_sq_add_sq
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
e2 : ∀ {x : ℝ}, HasDerivAt f (x / (x ^ 2 + y ^ 2)) x
e3 : deriv f = fun x => x / (x ^ 2 + y ^ 2)
⊢ ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Tactic:
have e4 : Continuous (deriv f) := by simpa only [e3] using continuous_self_div_sq_add_sq 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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
e2 : ∀ {x : ℝ}, HasDerivAt f (x / (x ^ 2 + y ^ 2)) x
e3 : deriv f = fun x => x / (x ^ 2 + y ^ 2)
e4 : Continuous (deriv f)
⊢ ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Theorem: integral_self_div_sq_add_sq
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
e2 : ∀ {x : ℝ}, HasDerivAt f (x / (x ^ 2 + y ^ 2)) x
e3 : deriv f = fun x => x / (x ^ 2 + y ^ 2)
e4 : Continuous (deriv f)
⊢ ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Tactic:
simp_rw [← e2.deriv]
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
e2 : ∀ {x : ℝ}, HasDerivAt f (x / (x ^ 2 + y ^ 2)) x
e3 : deriv f = fun x => x / (x ^ 2 + y ^ 2)
e4 : Continuous (deriv f)
⊢ ∫ (x : ℝ) in x₁..x₂, deriv f x = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Theorem: integral_self_div_sq_add_sq
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
e2 : ∀ {x : ℝ}, HasDerivAt f (x / (x ^ 2 + y ^ 2)) x
e3 : deriv f = fun x => x / (x ^ 2 + y ^ 2)
e4 : Continuous (deriv f)
⊢ ∫ (x : ℝ) in x₁..x₂, deriv f x = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
Tactic:
exact integral_deriv_eq_sub (λ _ _ => e2.differentiableAt) <| e4.intervalIntegrable _ _
Proof state after:
no goals
Theorem: integral_self_div_sq_add_sq
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
x : ?m.447992
⊢ HasDerivAt ?m.448301 ?m.448305 ?m.448306
Tactic:
simpa using hasDerivAt_pow 2 x
Proof state after:
no goals
Theorem: integral_self_div_sq_add_sq
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
x : ℝ
⊢ HasDerivAt f (x / (x ^ 2 + y ^ 2)) x
Tactic:
convert (e1.log (sq_add_sq_ne_zero hy)).div_const 2 using 1
Proof state after:
case h.e'_7
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
x : ℝ
⊢ x / (x ^ 2 + y ^ 2) = 2 * x / (x ^ 2 + y ^ 2) / 2
Theorem: integral_self_div_sq_add_sq
Proof state before:
case h.e'_7
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
x : ℝ
⊢ x / (x ^ 2 + y ^ 2) = 2 * x / (x ^ 2 + y ^ 2) / 2
Tactic:
field_simp
Proof state after:
case h.e'_7
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
x : ℝ
⊢ x * ((x ^ 2 + y ^ 2) * 2) = 2 * x * (x ^ 2 + y ^ 2)
Theorem: integral_self_div_sq_add_sq
Proof state before:
case h.e'_7
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
x : ℝ
⊢ x * ((x ^ 2 + y ^ 2) * 2) = 2 * x * (x ^ 2 + y ^ 2)
Tactic:
ring
Proof state after:
no goals
Theorem: integral_self_div_sq_add_sq
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
e2 : ∀ {x : ℝ}, HasDerivAt f (x / (x ^ 2 + y ^ 2)) x
e3 : deriv f = fun x => x / (x ^ 2 + y ^ 2)
⊢ Continuous (deriv f)
Tactic:
simpa only [e3] using continuous_self_div_sq_add_sq hy
Proof state after:
no goals
Theorem: integral_const_div_sq_add_sq
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 : ℝ) in x₁..x₂, y / (x ^ 2 + y ^ 2) = (x₂ / y).arctan - (x₁ / y).arctan
Tactic:
nth_rewrite 1 [← div_mul_cancel₀ x₁ hy, ← div_mul_cancel₀ x₂ 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
⊢ ∫ (x : ℝ) in x₁ / y * y..x₂ / y * y, y / (x ^ 2 + y ^ 2) = (x₂ / y).arctan - (x₁ / y).arctan
Theorem: integral_const_div_sq_add_sq
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 : ℝ) in x₁ / y * y..x₂ / y * y, y / (x ^ 2 + y ^ 2) = (x₂ / y).arctan - (x₁ / y).arctan
Tactic:
simp_rw [← mul_integral_comp_mul_right, ← integral_const_mul, ← integral_one_div_one_add_sq]
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 : ℝ) in x₁ / y..x₂ / y, y * (y / ((x * y) ^ 2 + y ^ 2)) = ∫ (x : ℝ) in x₁ / y..x₂ / y, 1 / (1 + x ^ 2)
Theorem: integral_const_div_sq_add_sq
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 : ℝ) in x₁ / y..x₂ / y, y * (y / ((x * y) ^ 2 + y ^ 2)) = ∫ (x : ℝ) in x₁ / y..x₂ / y, 1 / (1 + x ^ 2)
Tactic:
exact integral_congr <| λ x _ => by field_simp; ring
Proof state after:
no goals
Theorem: integral_const_div_sq_add_sq
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 : ℝ
x✝ : x ∈ [[x₁ / y, x₂ / y]]
⊢ y * (y / ((x * y) ^ 2 + y ^ 2)) = 1 / (1 + x ^ 2)
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₂ σ : ℝ
hy : y ≠ 0
x : ℝ
x✝ : x ∈ [[x₁ / y, x₂ / y]]
⊢ y * y * (1 + x ^ 2) = (x * y) ^ 2 + y ^ 2
Theorem: integral_const_div_sq_add_sq
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 : ℝ
x✝ : x ∈ [[x₁ / y, x₂ / y]]
⊢ y * y * (1 + x ^ 2) = (x * y) ^ 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
⊢ ∫ (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 e1 {x : ℝ} : A / (x + y * I) = A * x / (x ^ 2 + y ^ 2) - A * I * y / (x ^ 2 + y ^ 2) := by
  ring_nf ; simp_rw [inv_re_add_im] ; 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₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ ∫ (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)
⊢ ∫ (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 e2 : IntervalIntegrable (fun x ↦ A * x / (x ^ 2 + y ^ 2)) volume x₁ x₂ := by
  apply Continuous.intervalIntegrable
  simp_rw [mul_div_assoc] ; norm_cast
  exact continuous_const.mul <| continuous_ofReal.comp <| continuous_self_div_sq_add_sq 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₂
⊢ ∫ (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)