Theorem: integral_self_div_sq_add_sq (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₂ σ : ℝ
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
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

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)
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

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
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

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)
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

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
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

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]
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

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 _ _
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₂ σ : ℝ
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
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₂ σ : ℝ
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
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

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
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)

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
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₂ σ : ℝ
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
State after:
no goals