case hderiv
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

case hint
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ IntervalIntegrable (fun y => Complex.cos (z * ↑y)) MeasureTheory.volume a b
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ (∫ (x : ℝ) in a..b, Complex.cos (z * ↑x)) = Complex.sin (z * ↑b) / z - Complex.sin (z * ↑a) / z
apply integral_eq_sub_of_hasDerivAt
case hint
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ IntervalIntegrable (fun y => Complex.cos (z * ↑y)) MeasureTheory.volume a b

case hderiv
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
case hderiv
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

case hint
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ IntervalIntegrable (fun y => Complex.cos (z * ↑y)) MeasureTheory.volume a b
swap
case hderiv
a✝¹ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
case hderiv
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
intro x _
case hderiv
a✝² b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b x : ℝ
a✝ : x ∈ [[a✝¹, b]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
case hderiv
a✝¹ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
have a := Complex.hasDerivAt_sin (↑x * z)
case hderiv
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
case hderiv
a✝² b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b x : ℝ
a✝ : x ∈ [[a✝¹, b]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
have b : HasDerivAt (fun y => y * z : ℂ → ℂ) z ↑x := hasDerivAt_mul_const _
case hderiv
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
case hderiv
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
have c : HasDerivAt (fun y : ℂ => Complex.sin (y * z)) _ ↑x := HasDerivAt.comp (𝕜 := ℂ) x a b
case hderiv
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (↑y * z) / z) (Complex.cos (↑x * z) * z / z) x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
case hderiv
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
have d := HasDerivAt.comp_ofReal (c.div_const z)
case hderiv
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
case hderiv
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (↑y * z) / z) (Complex.cos (↑x * z) * z / z) x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
simp only [mul_comm] at d
case h.e'_7
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
⊢ Complex.cos (z * ↑x) = z * Complex.cos (z * ↑x) / z
case hderiv
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
convert d using 1
case h.e'_7
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
⊢ Complex.cos (z * ↑x) = Complex.cos (z * ↑x) * z / z
case h.e'_7
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
⊢ Complex.cos (z * ↑x) = z * Complex.cos (z * ↑x) / z
conv_rhs => arg 1; rw [mul_comm]
no goals
case h.e'_7
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
⊢ Complex.cos (z * ↑x) = Complex.cos (z * ↑x) * z / z
rw [mul_div_cancel _ hz]
case hint.hu
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ Continuous fun y => Complex.cos (z * ↑y)
case hint
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ IntervalIntegrable (fun y => Complex.cos (z * ↑y)) MeasureTheory.volume a b
apply Continuous.intervalIntegrable
no goals
case hint.hu
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ Continuous fun y => Complex.cos (z * ↑y)
exact Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)