internlm/Lean-Github huggingface dataset:
Theorem: Real.fderiv_fourierChar_apply
Proof 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]
Proof 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
Theorem: Real.fderiv_fourierChar_apply
Proof 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
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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 _
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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]
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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]
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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]
Proof 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
Theorem: Real.fderiv_fourierChar_apply
Proof 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
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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 _
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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]
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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']
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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
Proof 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))
Theorem: Real.fderiv_fourierChar_apply
Proof 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
Proof state after:
no goals
Theorem: Real.fderiv_fourierChar_apply
Proof 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]
Proof 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
Theorem: Real.fderiv_fourierChar_apply
Proof 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 _
Proof state after:
no goals
Theorem: Real.fderiv_fourierChar_apply
Proof 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 _
Proof state after:
no goals
Theorem: Real.fderiv_fourierChar
Proof 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 ?_
Proof 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
Theorem: Real.fderiv_fourierChar
Proof 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
Proof 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
Theorem: Real.fderiv_fourierChar
Proof 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]
Proof 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
Theorem: Real.fderiv_fourierChar
Proof 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
Proof 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
Theorem: Real.fderiv_fourierChar
Proof 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
Proof state after:
no goals
Theorem: Real.hasTemperateGrowth_cos
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cos x
Tactic:
simp_rw [cos, Complex.cos]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => ((cexp (↑x * I) + cexp (-↑x * I)) / 2).re
Theorem: Real.hasTemperateGrowth_cos
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => ((cexp (↑x * I) + cexp (-↑x * I)) / 2).re
Tactic:
refine ((Function.HasTemperateGrowth.add ?_ ?_).div_const 2).re
Proof state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑x * I)

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-↑x * I)
Theorem: Real.hasTemperateGrowth_cos
Proof state before:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑x * I)

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-↑x * I)
Tactic:
. simp_rw [← Complex.real_smul]
  exact Complex.hasTemperateGrowth_exp_real_smul_I
Proof state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-↑x * I)
Theorem: Real.hasTemperateGrowth_cos
Proof state before:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-↑x * I)
Tactic:
norm_cast
Proof state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑(-x) * I)
Theorem: Real.hasTemperateGrowth_cos
Proof state before:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑(-x) * I)
Tactic:
simp_rw [← Complex.real_smul]
Proof state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-x • I)
Theorem: Real.hasTemperateGrowth_cos
Proof state before:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-x • I)
Tactic:
exact Function.hasTemperateGrowth_neg.cexp_real_smul_I
Proof state after:
no goals
Theorem: Real.hasTemperateGrowth_cos
Proof state before:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑x * I)
Tactic:
simp_rw [← Complex.real_smul]
Proof state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (x • I)
Theorem: Real.hasTemperateGrowth_cos
Proof state before:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (x • I)
Tactic:
exact Complex.hasTemperateGrowth_exp_real_smul_I
Proof state after:
no goals
Theorem: Real.hasTemperateGrowth_sin
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => sin x
Tactic:
simp_rw [sin, Complex.sin]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => ((cexp (-↑x * I) - cexp (↑x * I)) * I / 2).re
Theorem: Real.hasTemperateGrowth_sin
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => ((cexp (-↑x * I) - cexp (↑x * I)) * I / 2).re
Tactic:
refine (((Function.HasTemperateGrowth.sub ?_ ?_).mul_const Complex.I).div_const 2).re
Proof state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-↑x * I)

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑x * I)
Theorem: Real.hasTemperateGrowth_sin
Proof state before:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-↑x * I)

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑x * I)
Tactic:
. norm_cast
  simp_rw [← Complex.real_smul]
  exact Function.hasTemperateGrowth_neg.cexp_real_smul_I
Proof state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑x * I)
Theorem: Real.hasTemperateGrowth_sin
Proof state before:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑x * I)
Tactic:
simp_rw [← Complex.real_smul]
Proof state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (x • I)
Theorem: Real.hasTemperateGrowth_sin
Proof state before:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (x • I)
Tactic:
exact Complex.hasTemperateGrowth_exp_real_smul_I
Proof state after:
no goals
Theorem: Real.hasTemperateGrowth_sin
Proof state before:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-↑x * I)
Tactic:
norm_cast
Proof state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑(-x) * I)
Theorem: Real.hasTemperateGrowth_sin
Proof state before:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑(-x) * I)
Tactic:
simp_rw [← Complex.real_smul]
Proof state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-x • I)
Theorem: Real.hasTemperateGrowth_sin
Proof state before:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-x • I)
Tactic:
exact Function.hasTemperateGrowth_neg.cexp_real_smul_I
Proof state after:
no goals
Theorem: Real.hasTemperateGrowth_fourierChar
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => ↑(fourierChar (Multiplicative.ofAdd x))
Tactic:
simp [fourierChar_apply]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (2 * ↑π * ↑x * I)
Theorem: Real.hasTemperateGrowth_fourierChar
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (2 * ↑π * ↑x * I)
Tactic:
norm_cast
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑(2 * π * x) * I)
Theorem: Real.hasTemperateGrowth_fourierChar
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑(2 * π * x) * I)
Tactic:
simp_rw [← Complex.real_smul]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp ((2 * π * x) • I)
Theorem: Real.hasTemperateGrowth_fourierChar
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp ((2 * π * x) • I)
Tactic:
exact (Function.hasTemperateGrowth_const_mul (2 * π)).cexp_real_smul_I
Proof state after:
no goals