-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
theorem fourierIntegral_deriv
    {f : ℝ → E} (hf : Integrable f) (h'f : Differentiable ℝ f) (hf' : Integrable (deriv f)) :
    𝓕 (deriv f) = fun (x : ℝ) ↦ (2 * π * I * x) • (𝓕 f x)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
⊢ 𝓕 (deriv f) = fun x => (2 * ↑π * I * ↑x) • 𝓕 f x

Tactic:
ext x

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
⊢ 𝓕 (deriv f) x = (2 * ↑π * I * ↑x) • 𝓕 f x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
⊢ Integrable (fun x => fderiv ℝ f x) volume

Tactic:
simpa only [← deriv_fderiv] using (ContinuousLinearMap.smulRightL ℝ ℝ E 1).integrable_comp hf'

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x => fderiv ℝ f x) volume
⊢ 𝓕 (deriv f) x = (𝓕 (fderiv ℝ f) x) 1

Tactic:
simp only [fourierIntegral_continuousLinearMap_apply I, fderiv_deriv]

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
⊢ 𝓕 (deriv f) x = (2 * ↑π * I * ↑x) • 𝓕 f x

Tactic:
have I : Integrable (fun x ↦ fderiv ℝ f x) := by
  simpa only [← deriv_fderiv] using (ContinuousLinearMap.smulRightL ℝ ℝ E 1).integrable_comp hf'

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x => fderiv ℝ f x) volume
⊢ 𝓕 (deriv f) x = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x => fderiv ℝ f x) volume
⊢ 𝓕 (deriv f) x = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x

Tactic:
have : 𝓕 (deriv f) x = 𝓕 (fderiv ℝ f) x 1 := by
  simp only [fourierIntegral_continuousLinearMap_apply I, fderiv_deriv]

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x => fderiv ℝ f x) volume
this : 𝓕 (deriv f) x = (𝓕 (fderiv ℝ f) x) 1
⊢ 𝓕 (deriv f) x = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x => fderiv ℝ f x) volume
this : 𝓕 (deriv f) x = (𝓕 (fderiv ℝ f) x) 1
⊢ (fourierSMulRight (-innerSL ℝ) (𝓕 f) x) 1 = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x

Tactic:
simp only [fourierSMulRight_apply, ContinuousLinearMap.neg_apply, innerSL_apply, smul_smul,
  RCLike.inner_apply, conj_trivial, mul_one, neg_smul, smul_neg, neg_neg, neg_mul, ← coe_smul]

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x => fderiv ℝ f x) volume
this : 𝓕 (deriv f) x = (𝓕 (fderiv ℝ f) x) 1
⊢ 𝓕 (deriv f) x = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x

Tactic:
rw [this, fourierIntegral_fderiv hf h'f I]

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x => fderiv ℝ f x) volume
this : 𝓕 (deriv f) x = (𝓕 (fderiv ℝ f) x) 1
⊢ (fourierSMulRight (-innerSL ℝ) (𝓕 f) x) 1 = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x