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

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
Tactic:
induction n generalizing ξ with
| zero => simp
| succ n IH =>
  rw [iteratedDeriv_succ]
  conv => lhs; arg 1; intro ζ
  simp only [IH, ← hasTemperateGrowth_smul_apply (Function.hasTemperateGrowth_pow n)]
  rw [deriv_const_smul _ (differentiable_fourierIntegral _ ξ), deriv_fourierIntegral]
  simp [hasTemperateGrowth_smul_apply, pow_succ', smul_smul, mul_comm (_ ^ n)]
State after:
no goals

State before:
case zero
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ iteratedDeriv Nat.zero (fun ξ => 𝓕 (fun x => f x) ξ) ξ =
    (-(2 * ↑π * I)) ^ Nat.zero • 𝓕 (fun x => x ^ Nat.zero • 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 : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ iteratedDeriv (Nat.succ n) (fun ξ => 𝓕 (fun x => f x) ξ) ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • 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 : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ deriv (iteratedDeriv n fun ξ => 𝓕 (fun x => f x) ξ) ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ

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

State before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ deriv (fun ζ => iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ζ) ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
Tactic:
simp only [IH, ← hasTemperateGrowth_smul_apply (Function.hasTemperateGrowth_pow n)]
State after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ deriv
      (fun ζ =>
        (-(2 * ↑π * I)) ^ n •
          𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ζ)
      ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ

State before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ deriv
      (fun ζ =>
        (-(2 * ↑π * I)) ^ n •
          𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ζ)
      ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
Tactic:
rw [deriv_const_smul _ (differentiable_fourierIntegral _ ξ), deriv_fourierIntegral]
State after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ (-(2 * ↑π * I)) ^ n •
      -((2 * ↑π * I) •
          𝓕 (fun x => x • ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ) =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ

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