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

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

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

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖ =
    (2 * π) ^ k * (|ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖) / (2 * π) ^ k
Tactic:
rw [mul_div_cancel_left]
State after:
case ha
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k ≠ 0

State before:
case ha
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k ≠ 0
Tactic:
simp [Real.pi_pos.ne']
State after:
no goals