-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
theorem iteratedDeriv_fourierIntegral {f : ℝ → E} {N : ℕ∞} {n : ℕ}
    (hf : ∀ (n : ℕ), n ≤ N → Integrable (fun x ↦ x^n • f x)) (hn : n ≤ N) :
    iteratedDeriv n (𝓕 f) = 𝓕 (fun x : ℝ ↦ (-2 * π * I * x) ^ n • f x)

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable f volume
⊢ iteratedDeriv n (𝓕 f) x = 𝓕 (fun x => (-2 * ↑π * I * ↑x) ^ n • f x) x

Tactic:
rw [iteratedDeriv, iteratedFDeriv_fourierIntegral A B hn,
  fourierIntegral_continuousMultilinearMap_apply (integrable_fourierPowSMulRight _ (A n hn) B),
  fourierIntegral_eq, fourierIntegral_eq]

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable f volume
⊢ (∫ (v : ℝ), 𝐞 (-inner v x) • (fourierPowSMulRight (innerSL ℝ) f v n) fun x => 1) =
    ∫ (v : ℝ), 𝐞 (-inner v x) • (-2 * ↑π * I * ↑v) ^ n • f v

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable f volume
y : ℝ
this : (-(2 * ↑π * I)) ^ n • y ^ n • f y = (-(2 * ↑π * I * ↑y)) ^ n • f y
⊢ (𝐞 (-inner y x) • (fourierPowSMulRight (innerSL ℝ) f y n) fun x => 1) = 𝐞 (-inner y x) • (-2 * ↑π * I * ↑y) ^ n • f y

Tactic:
simpa [innerSL_apply _]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
⊢ iteratedDeriv n (𝓕 f) = 𝓕 fun x => (-2 * ↑π * I * ↑x) ^ n • f x

Tactic:
ext x : 1

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
⊢ iteratedDeriv n (𝓕 f) x = 𝓕 (fun x => (-2 * ↑π * I * ↑x) ^ n • f x) x

Proof state:
case h.e'_6.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n✝ : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn✝ : ↑n✝ ≤ N
x✝ : ℝ
n : ℕ
hn : ↑n ≤ N
x : ℝ
⊢ ‖x‖ ^ n * ‖f x‖ = ‖x ^ n • f x‖

Tactic:
simp [norm_smul]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume
⊢ AEStronglyMeasurable f volume

Tactic:
simpa using (hf 0 (zero_le _)).1

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
⊢ iteratedDeriv n (𝓕 f) x = 𝓕 (fun x => (-2 * ↑π * I * ↑x) ^ n • f x) x

Tactic:
have A (n : ℕ) (hn : n ≤ N) : Integrable (fun v ↦ ‖v‖^n * ‖f v‖) := by
  convert (hf n hn).norm with x
  simp [norm_smul]

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume
⊢ iteratedDeriv n (𝓕 f) x = 𝓕 (fun x => (-2 * ↑π * I * ↑x) ^ n • f x) x

Proof state:
case h.e_f.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable f volume
y : ℝ
⊢ (-(2 * ↑π * I)) ^ n • y ^ n • f y = (-(2 * ↑π * I * ↑y)) ^ n • f y

Tactic:
simp only [← neg_mul, ← coe_smul, smul_smul, mul_pow, ofReal_pow, mul_assoc]

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable f volume
⊢ (∫ (v : ℝ), 𝐞 (-inner v x) • (fourierPowSMulRight (innerSL ℝ) f v n) fun x => 1) =
    ∫ (v : ℝ), 𝐞 (-inner v x) • (-2 * ↑π * I * ↑v) ^ n • f v

Tactic:
congr with y

Result:
case h.e_f.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable f volume
y : ℝ
⊢ (𝐞 (-inner y x) • (fourierPowSMulRight (innerSL ℝ) f y n) fun x => 1) = 𝐞 (-inner y x) • (-2 * ↑π * I * ↑y) ^ n • f y

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n✝ : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn✝ : ↑n✝ ≤ N
x : ℝ
n : ℕ
hn : ↑n ≤ N
⊢ Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume

Tactic:
convert (hf n hn).norm with x

Result:
case h.e'_6.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n✝ : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn✝ : ↑n✝ ≤ N
x✝ : ℝ
n : ℕ
hn : ↑n ≤ N
x : ℝ
⊢ ‖x‖ ^ n * ‖f x‖ = ‖x ^ n • f x‖

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume
⊢ iteratedDeriv n (𝓕 f) x = 𝓕 (fun x => (-2 * ↑π * I * ↑x) ^ n • f x) x

Tactic:
have B : AEStronglyMeasurable f := by simpa using (hf 0 (zero_le _)).1

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable f volume
⊢ iteratedDeriv n (𝓕 f) x = 𝓕 (fun x => (-2 * ↑π * I * ↑x) ^ n • f x) x

Proof state:
case h.e_f.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable f volume
y : ℝ
⊢ (𝐞 (-inner y x) • (fourierPowSMulRight (innerSL ℝ) f y n) fun x => 1) = 𝐞 (-inner y x) • (-2 * ↑π * I * ↑y) ^ n • f y

Tactic:
suffices (-(2 * π * I)) ^ n • y ^ n • f y = (-(2 * π * I * y)) ^ n • f y by
  simpa [innerSL_apply _]

Result:
case h.e_f.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable f volume
y : ℝ
⊢ (-(2 * ↑π * I)) ^ n • y ^ n • f y = (-(2 * ↑π * I * ↑y)) ^ n • f y