-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
/-- One can bound `‖w‖^n * ‖D^k (𝓕 f) w‖` in terms of integrals of the derivatives of `f` (or order
at most `n`) multiplied by powers of `v` (of order at most `k`). -/
lemma pow_mul_norm_iteratedFDeriv_fourierIntegral_le
    {K N : ℕ∞} (hf : ContDiff ℝ N f)
    (h'f : ∀ (k n : ℕ), k ≤ K → n ≤ N → Integrable (fun v ↦ ‖v‖^k * ‖iteratedFDeriv ℝ n f v‖))
    {k n : ℕ} (hk : k ≤ K) (hn : n ≤ N) (w : V) :
    ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * π) ^ k * (2 * k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        ∫ v, ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : V
⊢ ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

Tactic:
have Z : ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n * ((2 * (π * ‖innerSL (E := V) ℝ‖)) ^ k * ((2 * k + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂volume)) := by
  have := VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le (innerSL ℝ) hf h'f hk hn
    w w
  simp only [innerSL_apply _ w w, real_inner_self_eq_norm_sq w, abs_pow, abs_norm,
    mul_assoc] at this
  rwa [pow_two, mul_pow, mul_assoc] at this

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : V
Z :
  ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
⊢ ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

Proof state:
case inr.inr.h.hab.h.h
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn✝ : ↑n ≤ N
w : V
Z :
  ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (2 * (π * ‖innerSL ℝ‖)) ^ k *
      ((2 * ↑k + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖)
hn : n ≠ 0
hw : w ≠ 0
⊢ ‖innerSL ℝ‖ ≤ 1

Tactic:
exact norm_innerSL_le _

Result:
no goals

Proof state:
case inl
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k : ℕ
hk : ↑k ≤ K
w : V
hn : ↑0 ≤ N
Z :
  ‖w‖ ^ 0 * (‖w‖ ^ 0 * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ 0 *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ 0 *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (0 + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
⊢ ‖w‖ ^ 0 * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ 0 *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (0 + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

Tactic:
simp only [pow_zero, one_mul, mul_one, zero_add, Finset.range_one, Finset.product_singleton,
  Finset.sum_map, Function.Embedding.coeFn_mk, norm_iteratedFDeriv_zero] at Z ⊢

Result:
case inl
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k : ℕ
hk : ↑k ≤ K
w : V
hn : ↑0 ≤ N
Z : ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * (π * ‖innerSL ℝ‖)) ^ k * ∑ x ∈ Finset.range (k + 1), ∫ (v : V), ‖v‖ ^ x * ‖f v‖
⊢ ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * π) ^ k * ∑ x ∈ Finset.range (k + 1), ∫ (v : V), ‖v‖ ^ x * ‖f v‖

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : V
this :
  |((innerSL ℝ) w) w| ^ n * ‖iteratedFDeriv ℝ k (VectorFourier.fourierIntegral 𝐞 volume (innerSL ℝ).toLinearMap₂ f) w‖ ≤
    ‖w‖ ^ n * (2 * π * ‖innerSL ℝ‖) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂volume
⊢ ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))

Tactic:
simp only [innerSL_apply _ w w, real_inner_self_eq_norm_sq w, abs_pow, abs_norm,
  mul_assoc] at this

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : V
this :
  (‖w‖ ^ 2) ^ n * ‖iteratedFDeriv ℝ k (VectorFourier.fourierIntegral 𝐞 volume (innerSL ℝ).toLinearMap₂ f) w‖ ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂volume))
⊢ ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))