Theorem: Real.fderiv_fourierChar_apply (ForML/Trigonometric.lean)

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (fderiv ℝ (fun x => ↑(fourierChar (Multiplicative.ofAdd x))) x) dx =
    (2 * π * dx) • (I * ↑(fourierChar (Multiplicative.ofAdd x)))
Tactic:
simp [Real.fourierChar]
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (fderiv ℝ (fun x => cexp (2 * ↑π * ↑x * I)) x) dx = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (fderiv ℝ (fun x => cexp (2 * ↑π * ↑x * I)) x) dx = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))
Tactic:
norm_cast
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (fderiv ℝ (fun x => cexp (↑(2 * π * x) * I)) x) dx = ↑(2 * π * dx) * (I * cexp (↑(2 * π * x) * I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (fderiv ℝ (fun x => cexp (↑(2 * π * x) * I)) x) dx = ↑(2 * π * dx) * (I * cexp (↑(2 * π * x) * I))
Tactic:
rw [fderiv_cexp_real]
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (cexp (↑(2 * π * x) * I) • fderiv ℝ (fun x => ↑(2 * π * x) * I) x) dx = ↑(2 * π * dx) * (I * cexp (↑(2 * π * x) * I))

𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => ↑(2 * π * x) * I) x

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (cexp (↑(2 * π * x) * I) • fderiv ℝ (fun x => ↑(2 * π * x) * I) x) dx = ↑(2 * π * dx) * (I * cexp (↑(2 * π * x) * I))

𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => ↑(2 * π * x) * I) x
Tactic:
swap
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => ↑(2 * π * x) * I) x

𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (cexp (↑(2 * π * x) * I) • fderiv ℝ (fun x => ↑(2 * π * x) * I) x) dx = ↑(2 * π * dx) * (I * cexp (↑(2 * π * x) * I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => ↑(2 * π * x) * I) x

𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (cexp (↑(2 * π * x) * I) • fderiv ℝ (fun x => ↑(2 * π * x) * I) x) dx = ↑(2 * π * dx) * (I * cexp (↑(2 * π * x) * I))
Tactic:
. simp_rw [← Complex.real_smul]
  exact (differentiableAt_id.const_mul _).smul_const _
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (cexp (↑(2 * π * x) * I) • fderiv ℝ (fun x => ↑(2 * π * x) * I) x) dx = ↑(2 * π * dx) * (I * cexp (↑(2 * π * x) * I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (cexp (↑(2 * π * x) * I) • fderiv ℝ (fun x => ↑(2 * π * x) * I) x) dx = ↑(2 * π * dx) * (I * cexp (↑(2 * π * x) * I))
Tactic:
simp
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (cexp (2 * ↑π * ↑x * I) • fderiv ℝ (fun x => 2 * ↑π * ↑x * I) x) dx = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (cexp (2 * ↑π * ↑x * I) • fderiv ℝ (fun x => 2 * ↑π * ↑x * I) x) dx = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))
Tactic:
rw [ContinuousLinearMap.smul_apply]
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp (2 * ↑π * ↑x * I) • (fderiv ℝ (fun x => 2 * ↑π * ↑x * I) x) dx = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp (2 * ↑π * ↑x * I) • (fderiv ℝ (fun x => 2 * ↑π * ↑x * I) x) dx = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))
Tactic:
simp
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp (2 * ↑π * ↑x * I) * (fderiv ℝ (fun x => 2 * ↑π * ↑x * I) x) dx = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp (2 * ↑π * ↑x * I) * (fderiv ℝ (fun x => 2 * ↑π * ↑x * I) x) dx = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))
Tactic:
norm_cast
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp (↑(2 * π * x) * I) * (fderiv ℝ (fun x => ↑(2 * π * x) * I) x) dx = ↑(2 * π * dx) * (I * cexp (↑(2 * π * x) * I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp (↑(2 * π * x) * I) * (fderiv ℝ (fun x => ↑(2 * π * x) * I) x) dx = ↑(2 * π * dx) * (I * cexp (↑(2 * π * x) * I))
Tactic:
simp_rw [← Complex.real_smul]
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp ((2 * π * x) • I) * (fderiv ℝ (fun x => (2 * π * x) • I) x) dx = (2 * π * dx) • (I * cexp ((2 * π * x) • I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp ((2 * π * x) • I) * (fderiv ℝ (fun x => (2 * π * x) • I) x) dx = (2 * π * dx) • (I * cexp ((2 * π * x) • I))
Tactic:
rw [fderiv_smul_const]
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp ((2 * π * x) • I) * (ContinuousLinearMap.smulRight (fderiv ℝ (fun x => 2 * π * x) x) I) dx =
    (2 * π * dx) • (I * cexp ((2 * π * x) • I))

case hc
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => 2 * π * x) x

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp ((2 * π * x) • I) * (ContinuousLinearMap.smulRight (fderiv ℝ (fun x => 2 * π * x) x) I) dx =
    (2 * π * dx) • (I * cexp ((2 * π * x) • I))

case hc
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => 2 * π * x) x
Tactic:
swap
State after:
case hc
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => 2 * π * x) x

𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp ((2 * π * x) • I) * (ContinuousLinearMap.smulRight (fderiv ℝ (fun x => 2 * π * x) x) I) dx =
    (2 * π * dx) • (I * cexp ((2 * π * x) • I))

State before:
case hc
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => 2 * π * x) x

𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp ((2 * π * x) • I) * (ContinuousLinearMap.smulRight (fderiv ℝ (fun x => 2 * π * x) x) I) dx =
    (2 * π * dx) • (I * cexp ((2 * π * x) • I))
Tactic:
. exact DifferentiableAt.const_mul differentiableAt_id _
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp ((2 * π * x) • I) * (ContinuousLinearMap.smulRight (fderiv ℝ (fun x => 2 * π * x) x) I) dx =
    (2 * π * dx) • (I * cexp ((2 * π * x) • I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp ((2 * π * x) • I) * (ContinuousLinearMap.smulRight (fderiv ℝ (fun x => 2 * π * x) x) I) dx =
    (2 * π * dx) • (I * cexp ((2 * π * x) • I))
Tactic:
rw [ContinuousLinearMap.smulRight_apply]
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp ((2 * π * x) • I) * (fderiv ℝ (fun x => 2 * π * x) x) dx • I = (2 * π * dx) • (I * cexp ((2 * π * x) • I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp ((2 * π * x) • I) * (fderiv ℝ (fun x => 2 * π * x) x) dx • I = (2 * π * dx) • (I * cexp ((2 * π * x) • I))
Tactic:
simp
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp (2 * ↑π * ↑x * I) * (↑((fderiv ℝ (fun x => 2 * π * x) x) dx) * I) = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp (2 * ↑π * ↑x * I) * (↑((fderiv ℝ (fun x => 2 * π * x) x) dx) * I) = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))
Tactic:
rw [fderiv_const_mul differentiableAt_id']
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp (2 * ↑π * ↑x * I) * (↑(((2 * π) • fderiv ℝ (fun x => x) x) dx) * I) = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp (2 * ↑π * ↑x * I) * (↑(((2 * π) • fderiv ℝ (fun x => x) x) dx) * I) = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))
Tactic:
simp
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp (2 * ↑π * ↑x * I) * (2 * ↑π * ↑dx * I) = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp (2 * ↑π * ↑x * I) * (2 * ↑π * ↑dx * I) = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))
Tactic:
ring_nf
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => ↑(2 * π * x) * I) x
Tactic:
simp_rw [← Complex.real_smul]
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => (2 * π * x) • I) x

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => (2 * π * x) • I) x
Tactic:
exact (differentiableAt_id.const_mul _).smul_const _
State after:
no goals

State before:
case hc
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => 2 * π * x) x
Tactic:
exact DifferentiableAt.const_mul differentiableAt_id _
State after:
no goals