Theorem: SchwartzMap.Real.fourierIntegral_iteratedDeriv (ForML/SchwartzRealFourier.lean)

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
Tactic:
induction n with
| zero => simp
| succ n IH =>
  rw [iteratedDeriv_succ]
  conv => lhs; arg 1; intro x; arg 1; intro z
  simp only [iteratedDeriv_eq_iteratedPDeriv]
  rw [fourierIntegral_deriv]
  simp only [← iteratedDeriv_eq_iteratedPDeriv]
  rw [IH]
  simp [pow_succ, smul_smul]
State after:
no goals

State before:
case zero
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => iteratedDeriv Nat.zero (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.zero • 𝓕 (fun x => f x) ξ
Tactic:
simp
State after:
no goals

State before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => iteratedDeriv (Nat.succ n) (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun x => f x) ξ
Tactic:
rw [iteratedDeriv_succ]
State after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => deriv (iteratedDeriv n fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun x => f x) ξ

State before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => deriv (iteratedDeriv n fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun x => f x) ξ
Tactic:
conv => lhs; arg 1; intro x; arg 1; intro z
State after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => deriv (fun z => iteratedDeriv n (fun y => f y) z) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun x => f x) ξ

State before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => deriv (fun z => iteratedDeriv n (fun y => f y) z) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun x => f x) ξ
Tactic:
simp only [iteratedDeriv_eq_iteratedPDeriv]
State after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => deriv (fun z => ((iteratedPDeriv ℝ fun x => 1) f) z) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ

State before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => deriv (fun z => ((iteratedPDeriv ℝ fun x => 1) f) z) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
Tactic:
rw [fourierIntegral_deriv]
State after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => ((iteratedPDeriv ℝ fun x => 1) f) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ

State before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => ((iteratedPDeriv ℝ fun x => 1) f) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
Tactic:
simp only [← iteratedDeriv_eq_iteratedPDeriv]
State after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => iteratedDeriv n (⇑f) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ

State before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => iteratedDeriv n (⇑f) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
Tactic:
rw [IH]
State after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ

State before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
Tactic:
simp [pow_succ, smul_smul]
State after:
no goals