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

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

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k * (|ξ| ^ k * ‖(-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ‖) =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
Tactic:
rw [norm_smul, mul_rotate' _ ‖_ ^ n‖, mul_rotate' _ ‖_ ^ n‖]
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖(-(2 * ↑π * I)) ^ n‖ * (‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k) =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖(-(2 * ↑π * I)) ^ n‖ * (‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k) =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
Tactic:
refine congrArg₂ _ (by simp [abs_of_nonneg Real.pi_pos.le]) ?_
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k = ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k = ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
Tactic:
simp only [← hasTemperateGrowth_smul_apply (Function.hasTemperateGrowth_pow n)]
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖ * |ξ| ^ k *
      (2 * π) ^ k =
    ‖𝓕
        (fun x =>
          iteratedDeriv k (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) x)
        ξ‖

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖ * |ξ| ^ k *
      (2 * π) ^ k =
    ‖𝓕
        (fun x =>
          iteratedDeriv k (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) x)
        ξ‖
Tactic:
rw [fourierIntegral_iteratedDeriv]
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖ * |ξ| ^ k *
      (2 * π) ^ k =
    ‖(2 * ↑π * I * ↑ξ) ^ k •
        𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖ * |ξ| ^ k *
      (2 * π) ^ k =
    ‖(2 * ↑π * I * ↑ξ) ^ k •
        𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖
Tactic:
simp only [hasTemperateGrowth_smul_apply, norm_smul]
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖ * ‖𝓕 (fun x => x ^ n • f x) ξ‖

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖ * ‖𝓕 (fun x => x ^ n • f x) ξ‖
Tactic:
rw [mul_assoc, mul_comm]
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * (2 * π) ^ k * ‖𝓕 (fun x => x ^ n • f x) ξ‖ = ‖(2 * ↑π * I * ↑ξ) ^ k‖ * ‖𝓕 (fun x => x ^ n • f x) ξ‖

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * (2 * π) ^ k * ‖𝓕 (fun x => x ^ n • f x) ξ‖ = ‖(2 * ↑π * I * ↑ξ) ^ k‖ * ‖𝓕 (fun x => x ^ n • f x) ξ‖
Tactic:
refine congrArg₂ _ ?_ rfl
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * (2 * π) ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * (2 * π) ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖
Tactic:
rw [mul_comm]
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k * |ξ| ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k * |ξ| ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖
Tactic:
simp [mul_pow, abs_of_nonneg Real.pi_pos.le]
State after:
no goals

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖(-(2 * ↑π * I)) ^ n‖ = (2 * π) ^ n
Tactic:
simp [abs_of_nonneg Real.pi_pos.le]
State after:
no goals