awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
k : ℕ∞ω
hf : ContDiff ℝ k f
n : ℕ
hf₁ :
  ContDiff ℝ (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) k fun (y : V) ↦
    ((smulRightL ℝ (fun (x : Fin n) ↦ W) E :
            (a : ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) →
              E →L[ℝ] ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
          ((compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
                (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
              (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
            fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) y) :
        (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
      (f y)
⊢ ContDiff ℝ (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) k fun (v : V) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E) ((-(2 * (↑π : ℂ) * I)) ^ n)
      (((smulRightL ℝ (fun (x : Fin n) ↦ W) E :
                (a : ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) →
                  E →L[ℝ] ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
              ((compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
                    (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
                  (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
                fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) :
            (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
          (f v) :
        ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E)

Tactic:
apply ContDiff.const_smul

Premises used: ContDiff.const_smul
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
k : ℕ∞ω
hf : ContDiff ℝ k f
n : ℕ
apply :
  ContDiff.{0, u_2, u_3} ℝ (F := ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) k fun (x : V) ↦
    (compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
          (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
        (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
      fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x
⊢ ContDiff ℝ (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) k fun (y : V) ↦
    ((smulRightL ℝ (fun (x : Fin n) ↦ W) E :
            (a : ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) →
              E →L[ℝ] ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
          ((compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
                (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
              (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
            fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) y) :
        (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
      (f y)

Tactic:
apply (smulRightL ℝ (fun (_ : Fin n) ↦ W) E).isBoundedBilinearMap.contDiff.comp₂ _ hf

Premises used: Real, IsBoundedBilinearMap.contDiff, ContinuousLinearMap.isBoundedBilinearMap, ContDiff.comp₂, ContinuousMultilinearMap.smulRightL
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
k : ℕ∞ω
hf : ContDiff ℝ k f
n : ℕ
apply :
  ContDiff.{0, u_2, u_3} ℝ (F := (i : Fin n) → W →L[ℝ] ℝ) k fun (x : V) (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x
⊢ ContDiff.{0, u_2, u_3} ℝ (F := ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) k fun (x : V) ↦
    (compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
          (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
        (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
      fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x

Tactic:
apply (ContinuousMultilinearMap.contDiff _).comp

Premises used: ContinuousMultilinearMap.contDiff, ContDiff.comp
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
k : ℕ∞ω
hf : ContDiff ℝ k f
n : ℕ
⊢ ContDiff.{0, u_2, u_3} ℝ (F := (i : Fin n) → W →L[ℝ] ℝ) k fun (x : V) (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x

Tactic:
contDiff_pi.2 (fun _ ↦ L.contDiff)

Premises used: Iff.mpr, ContinuousLinearMap.contDiff, contDiff_pi
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
k : ℕ∞ω
hf : ContDiff ℝ k f
n : ℕ
⊢ ContDiff.{0, u_2, u_3} ℝ (F := (i : Fin n) → W →L[ℝ] ℝ) k fun (x : V) (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x

Tactic:
exact contDiff_pi.2 (fun _ ↦ L.contDiff)

Premises used: Iff.mpr, ContinuousLinearMap.contDiff, contDiff_pi
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
v : V
n : ℕ
⊢ 0 ≤ (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
v : V
n : ℕ
apply :
  ∀ (m : (i : Fin n) → W),
    Norm.norm.{u_1} (E := E) ((fourierPowSMulRight L f v n : (a : (i : Fin n) → W) → E) m : E) ≤
      (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ i : Fin n, ‖m i‖
⊢ Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) (fourierPowSMulRight L f v n) ≤
    (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖

Tactic:
apply ContinuousMultilinearMap.opNorm_le_bound (by positivity) (fun m ↦ ?_)

Premises used: ContinuousMultilinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
v : V
n : ℕ
m : (i : Fin n) → W
⊢ Norm.norm.{u_1} (E := E) ((fourierPowSMulRight L f v n : (a : (i : Fin n) → W) → E) m : E) =
    (2 * π) ^ n * ((∏ x : Fin n, |(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) (m x)|) * ‖f v‖)

Tactic:
simp [abs_of_nonneg pi_nonneg, norm_smul]

Premises used: norm_smul, Real.pi_nonneg, abs_of_nonneg
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
v : V
n : ℕ
m : (i : Fin n) → W
hbc :
  ∀ (i : Fin n) (_hi : Membership.mem (γ := Finset (Fin n)) Finset.univ i),
    |(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) (m i)| ≤ ‖L‖ * ‖v‖ * ‖m i‖
⊢ (2 * π) ^ n * ((∏ x : Fin n, |(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) (m x)|) * ‖f v‖) ≤
    (2 * π) ^ n * ((∏ x : Fin n, ‖L‖ * ‖v‖ * ‖m x‖) * ‖f v‖)

Tactic:
gcongr with i _hi
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
v : V
n : ℕ
m : (i : Fin n) → W
i : Fin n
_hi : Membership.mem (γ := Finset (Fin n)) Finset.univ i
⊢ |(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) (m i)| ≤ ‖L‖ * ‖v‖ * ‖m i‖

Tactic:
L.le_opNorm₂ v (m i)

Premises used: ContinuousLinearMap.le_opNorm₂
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
v : V
n : ℕ
m : (i : Fin n) → W
i : Fin n
_hi : Membership.mem (γ := Finset (Fin n)) Finset.univ i
⊢ |(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) (m i)| ≤ ‖L‖ * ‖v‖ * ‖m i‖

Tactic:
exact L.le_opNorm₂ v (m i)

Premises used: ContinuousLinearMap.le_opNorm₂
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
v : V
n : ℕ
m : (i : Fin n) → W
simp :
  HPow.hPow (α := ℝ) 2 n * π ^ n * ((‖L‖ ^ n * ‖v‖ ^ n * ∏ x : Fin n, ‖m x‖) * ‖f v‖) =
    HPow.hPow (α := ℝ) 2 n * π ^ n * ‖L‖ ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ x : Fin n, ‖m x‖
⊢ (2 * π) ^ n * ((∏ x : Fin n, ‖L‖ * ‖v‖ * ‖m x‖) * ‖f v‖) = (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ i : Fin n, ‖m i‖

Tactic:
simp [Finset.prod_mul_distrib, mul_pow]

Premises used: Finset.prod_mul_distrib, mul_pow
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
v : V
n : ℕ
m : (i : Fin n) → W
⊢ HPow.hPow (α := ℝ) 2 n * π ^ n * ((‖L‖ ^ n * ‖v‖ ^ n * ∏ x : Fin n, ‖m x‖) * ‖f v‖) =
    HPow.hPow (α := ℝ) 2 n * π ^ n * ‖L‖ ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ x : Fin n, ‖m x‖

Tactic:
ring
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
v : V
n : ℕ
m : (i : Fin n) → W
L₁ :
  Norm.norm.{u_1} (E := E) ((fourierPowSMulRight L f v n : (a : (i : Fin n) → W) → E) m : E) =
    (2 * π) ^ n * ((∏ x : Fin n, |(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) (m x)|) * ‖f v‖)
L₂ :
  (2 * π) ^ n * ((∏ x : Fin n, |(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) (m x)|) * ‖f v‖) ≤
    (2 * π) ^ n * ((∏ x : Fin n, ‖L‖ * ‖v‖ * ‖m x‖) * ‖f v‖)
L₃ : (2 * π) ^ n * ((∏ x : Fin n, ‖L‖ * ‖v‖ * ‖m x‖) * ‖f v‖) = (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ i : Fin n, ‖m i‖
⊢ Norm.norm.{u_1} (E := E) ((fourierPowSMulRight L f v n : (a : (i : Fin n) → W) → E) m : E) ≤
    (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ i : Fin n, ‖m i‖

Tactic:
calc
  ‖fourierPowSMulRight L f v n m‖
    = (2 * π) ^ n * ((∏ x : Fin n, |(L v) (m x)|) * ‖f v‖) := by
      simp [abs_of_nonneg pi_nonneg, norm_smul]
  _ ≤ (2 * π) ^ n * ((∏ x : Fin n, ‖L‖ * ‖v‖ * ‖m x‖) * ‖f v‖) := by
      gcongr with i _hi
      exact L.le_opNorm₂ v (m i)
  _ = (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ i : Fin n, ‖m i‖ := by
      simp [Finset.prod_mul_distrib, mul_pow]; ring

Premises used: Norm.norm, Real.pi, HMul.hMul, VectorFourier.fourierPowSMulRight, Finset.univ, abs, Finset.prod, OfNat.ofNat, Fin, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : (↑k : ℕ∞ω) ≤ K
v : V
hv :
  ∀ i ≤ k,
    ∀ j ≤ n,
      ‖v‖ ^ j *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E)
            (iteratedFDeriv ℝ i f v) ≤
        C
simp_rw :
  Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin k) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E))
      (iteratedFDeriv ℝ k
        (fun (v : V) ↦
          HSMul.hSMul (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E)
            ((-(2 * (↑π : ℂ) * I)) ^ n)
            (((smulRightL ℝ (fun (x : Fin n) ↦ W) E :
                      (a : ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) →
                        E →L[ℝ] ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
                    ((compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
                          (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
                        (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
                      fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) :
                  (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
                (f v) :
              ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E))
        v) ≤
    (2 * π) ^ n * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k * ‖L‖ ^ n * C
⊢ Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin k) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E))
      (iteratedFDeriv ℝ k (fun (v : V) ↦ fourierPowSMulRight L f v n) v) ≤
    (2 * π) ^ n * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k * ‖L‖ ^ n * C

Tactic:
simp_rw [fourierPowSMulRight_eq_comp]

Premises used: VectorFourier.fourierPowSMulRight_eq_comp
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : (↑k : ℕ∞ω) ≤ K
v : V
hv :
  ∀ i ≤ k,
    ∀ j ≤ n,
      ‖v‖ ^ j *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E)
            (iteratedFDeriv ℝ i f v) ≤
        C
T : ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) :=
  compContinuousLinearMapLRight (E := fun (i : Fin n) ↦ W) (E₁ := fun (i : Fin n) ↦ ℝ)
    (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ)
m : ℕ
apply :
  Norm.norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
      (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) ≤
    1
⊢ ‖T‖ ≤ 1

Tactic:
apply (norm_compContinuousLinearMapLRight_le _ _).trans

Premises used: ContinuousMultilinearMap.norm_compContinuousLinearMapLRight_le, LE.le.trans
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : (↑k : ℕ∞ω) ≤ K
v : V
hv :
  ∀ i ≤ k,
    ∀ j ≤ n,
      ‖v‖ ^ j *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E)
            (iteratedFDeriv ℝ i f v) ≤
        C
T : ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) :=
  compContinuousLinearMapLRight (E := fun (i : Fin n) ↦ W) (E₁ := fun (i : Fin n) ↦ ℝ)
    (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ)
m : ℕ
⊢ Norm.norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
      (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) ≤
    1

Tactic:
simp only [norm_mkPiAlgebra, le_refl]

Premises used: le_refl, ContinuousMultilinearMap.norm_mkPiAlgebra
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : (↑k : ℕ∞ω) ≤ K
v : V
hv :
  ∀ i ≤ k,
    ∀ j ≤ n,
      ‖v‖ ^ j *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E)
            (iteratedFDeriv ℝ i f v) ≤
        C
T : ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) :=
  compContinuousLinearMapLRight (E := fun (i : Fin n) ↦ W) (E₁ := fun (i : Fin n) ↦ ℝ)
    (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ)
m : ℕ
⊢ ‖T‖ ≤ 1

Tactic:
have : ‖T‖ ≤ 1 := by
      apply (norm_compContinuousLinearMapLRight_le _ _).trans
      simp only [norm_mkPiAlgebra, le_refl]
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : (↑k : ℕ∞ω) ≤ K
v : V
hv :
  ∀ i ≤ k,
    ∀ j ≤ n,
      ‖v‖ ^ j *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E)
            (iteratedFDeriv ℝ i f v) ≤
        C
T : ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) :=
  compContinuousLinearMapLRight (E := fun (i : Fin n) ↦ W) (E₁ := fun (i : Fin n) ↦ ℝ)
    (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ)
m : ℕ
this : ‖T‖ ≤ 1
apply :
  (↑((Fintype.card (Fin n)).descFactorial m) : ℝ) * ‖T‖ *
      (Norm.norm.{u_3} (E := (i : Fin n) → W →L[ℝ] ℝ) fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) ^
        (Fintype.card (Fin n) - m) ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m)
⊢ Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ (i : Fin n) → W →L[ℝ] ℝ)
        (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
      (iteratedFDeriv ℝ m (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
        fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m)

Tactic:
apply (ContinuousMultilinearMap.norm_iteratedFDeriv_le _ _ _).trans

Premises used: ContinuousMultilinearMap.norm_iteratedFDeriv_le, LE.le.trans
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : (↑k : ℕ∞ω) ≤ K
v : V
hv :
  ∀ i ≤ k,
    ∀ j ≤ n,
      ‖v‖ ^ j *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E)
            (iteratedFDeriv ℝ i f v) ≤
        C
T : ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) :=
  compContinuousLinearMapLRight (E := fun (i : Fin n) ↦ W) (E₁ := fun (i : Fin n) ↦ ℝ)
    (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ)
m : ℕ
this : ‖T‖ ≤ 1
simp :
  (↑(n.descFactorial m) : ℝ) * ‖T‖ *
      (Norm.norm.{u_3} (E := (i : Fin n) → W →L[ℝ] ℝ) fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) ^ (n - m) ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m)
⊢ (↑((Fintype.card (Fin n)).descFactorial m) : ℝ) * ‖T‖ *
      (Norm.norm.{u_3} (E := (i : Fin n) → W →L[ℝ] ℝ) fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) ^
        (Fintype.card (Fin n) - m) ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m)

Tactic:
simp only [Fintype.card_fin]

Premises used: Fintype.card_fin
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : (↑k : ℕ∞ω) ≤ K
v : V
hv :
  ∀ i ≤ k,
    ∀ j ≤ n,
      ‖v‖ ^ j *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E)
            (iteratedFDeriv ℝ i f v) ≤
        C
T : ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) :=
  compContinuousLinearMapLRight (E := fun (i : Fin n) ↦ W) (E₁ := fun (i : Fin n) ↦ ℝ)
    (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ)
m : ℕ
this : ‖T‖ ≤ 1
h₂ : (Norm.norm.{u_3} (E := (i : Fin n) → W →L[ℝ] ℝ) fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) ≤ ‖L‖ * ‖v‖
⊢ (↑(n.descFactorial m) : ℝ) * ‖T‖ *
      (Norm.norm.{u_3} (E := (i : Fin n) → W →L[ℝ] ℝ) fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) ^ (n - m) ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : (↑k : ℕ∞ω) ≤ K
v : V
hv :
  ∀ i ≤ k,
    ∀ j ≤ n,
      ‖v‖ ^ j *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E)
            (iteratedFDeriv ℝ i f v) ≤
        C
T : ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) :=
  compContinuousLinearMapLRight (E := fun (i : Fin n) ↦ W) (E₁ := fun (i : Fin n) ↦ ℝ)
    (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ)
m : ℕ
this : ‖T‖ ≤ 1
h₂ : ∀ (x : Fin n), Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) ≤ ‖L‖ * ‖v‖
⊢ (Norm.norm.{u_3} (E := (i : Fin n) → W →L[ℝ] ℝ) fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) ≤ ‖L‖ * ‖v‖

Tactic:
refine (pi_norm_le_iff_of_nonneg (by positivity)).mpr (fun _ ↦ ?_)

Premises used: Iff.mpr, pi_norm_le_iff_of_nonneg