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

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ fderiv ℝ (fun x => ↑(fourierChar (Multiplicative.ofAdd x))) x =
    (2 * ↑π * I * ↑(fourierChar (Multiplicative.ofAdd x))) • ofRealCLM
Tactic:
refine ContinuousLinearMap.ext ?_
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ ∀ (x_1 : ℝ),
    (fderiv ℝ (fun x => ↑(fourierChar (Multiplicative.ofAdd x))) x) x_1 =
      ((2 * ↑π * I * ↑(fourierChar (Multiplicative.ofAdd x))) • ofRealCLM) x_1

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ ∀ (x_1 : ℝ),
    (fderiv ℝ (fun x => ↑(fourierChar (Multiplicative.ofAdd x))) x) x_1 =
      ((2 * ↑π * I * ↑(fourierChar (Multiplicative.ofAdd x))) • ofRealCLM) x_1
Tactic:
intro dx
State after:
𝕜 : 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 * ↑π * I * ↑(fourierChar (Multiplicative.ofAdd x))) • ofRealCLM) dx

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 * ↑π * I * ↑(fourierChar (Multiplicative.ofAdd x))) • ofRealCLM) dx
Tactic:
rw [fderiv_fourierChar_apply]
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (2 * π * dx) • (I * ↑(fourierChar (Multiplicative.ofAdd x))) =
    ((2 * ↑π * I * ↑(fourierChar (Multiplicative.ofAdd x))) • ofRealCLM) dx

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

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