-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
lemma hasDerivAt_fourierIntegral
    {f : ℝ → E} (hf : Integrable f) (hf' : Integrable (fun x : ℝ ↦ x • f x)) (w : ℝ) :
    HasDerivAt (𝓕 f) (𝓕 (fun x : ℝ ↦ (-2 * π * I * x) • f x) w) w

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
this : Integrable (fun v => (L v).smulRight (f v)) volume
⊢ Integrable (fun v => fourierSMulRight L f v) volume

Tactic:
simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using this.smul (-2 * π * I)

Result:
no goals

Proof state:
case h.e'_6.h.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
v : ℝ
⊢ ((L v).smulRight (f v)) 1 = (↑(ContinuousLinearMap.ring_lmap_equiv_self ℝ E).symm.toContinuousLinearEquiv (v • f v)) 1

Tactic:
rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.mul_apply', mul_one,
  ContinuousLinearMap.map_smul]

Result:
case h.e'_6.h.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
v : ℝ
⊢ v • f v = (v • ↑(ContinuousLinearMap.ring_lmap_equiv_self ℝ E).symm.toContinuousLinearEquiv (f v)) 1

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
h_int : Integrable (fun v => fourierSMulRight L f v) volume
⊢ HasDerivAt (𝓕 f) (𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w) w

Tactic:
rw [← VectorFourier.fourierIntegral_convergent_iff continuous_fourierChar L.continuous₂ w]
  at h_int

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
h_int : Integrable (fun v => 𝐞 (-((LinearMap.mul ℝ ℝ) v) w) • fourierSMulRight L f v) volume
⊢ HasDerivAt (𝓕 f) (𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w) w

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
⊢ HasDerivAt (𝓕 f) (𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w) w

Tactic:
have h_int : Integrable fun v ↦ fourierSMulRight L f v := by
  suffices Integrable fun v ↦ ContinuousLinearMap.smulRight (L v) (f v) by
    simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using this.smul (-2 * π * I)
  convert ((ContinuousLinearMap.ring_lmap_equiv_self ℝ
    E).symm.toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with v
  apply ContinuousLinearMap.ext_ring
  rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.mul_apply', mul_one,
    ContinuousLinearMap.map_smul]
  exact congr_arg (fun x ↦ v • x) (one_smul ℝ (f v)).symm

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
h_int : Integrable (fun v => fourierSMulRight L f v) volume
⊢ HasDerivAt (𝓕 f) (𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w) w

Proof state:
case h.e'_9
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
h_int : Integrable (fun v => 𝐞 (-((LinearMap.mul ℝ ℝ) v) w) • fourierSMulRight L f v) volume
⊢ 𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w =
    (VectorFourier.fourierIntegral 𝐞 volume L.toLinearMap₂ (fourierSMulRight L f) w) 1

Tactic:
erw [ContinuousLinearMap.integral_apply h_int]

Result:
case h.e'_9
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
h_int : Integrable (fun v => 𝐞 (-((LinearMap.mul ℝ ℝ) v) w) • fourierSMulRight L f v) volume
⊢ 𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w =
    ∫ (x : ℝ), (𝐞 (-((LinearMap.mul ℝ ℝ) x) w) • fourierSMulRight L f x) 1 ∂volume

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
⊢ Integrable (fun v => (L v).smulRight (f v)) volume

Tactic:
convert ((ContinuousLinearMap.ring_lmap_equiv_self ℝ
  E).symm.toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with v

Result:
case h.e'_6.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
v : ℝ
⊢ (L v).smulRight (f v) = ↑(ContinuousLinearMap.ring_lmap_equiv_self ℝ E).symm.toContinuousLinearEquiv (v • f v)

Proof state:
case h.e'_6.h.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
v : ℝ
⊢ v • f v = (v • ↑(ContinuousLinearMap.ring_lmap_equiv_self ℝ E).symm.toContinuousLinearEquiv (f v)) 1

Tactic:
exact congr_arg (fun x ↦ v • x) (one_smul ℝ (f v)).symm

Result:
no goals

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

Tactic:
have hf'' : Integrable (fun v : ℝ ↦ ‖v‖ * ‖f v‖) := by simpa only [norm_smul] using hf'.norm

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
⊢ HasDerivAt (𝓕 f) (𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w) w

Proof state:
case h.e'_6.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
v : ℝ
⊢ (L v).smulRight (f v) = ↑(ContinuousLinearMap.ring_lmap_equiv_self ℝ E).symm.toContinuousLinearEquiv (v • f v)

Tactic:
apply ContinuousLinearMap.ext_ring

Result:
case h.e'_6.h.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
w : ℝ
hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ
v : ℝ
⊢ ((L v).smulRight (f v)) 1 = (↑(ContinuousLinearMap.ring_lmap_equiv_self ℝ E).symm.toContinuousLinearEquiv (v • f v)) 1