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 : ℕ∞ω
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
x : Fin n
⊢ Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) ≤ ‖L‖ * ‖v‖

Tactic:
ContinuousLinearMap.le_opNorm _ _

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
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
x : Fin n
⊢ Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) ≤ ‖L‖ * ‖v‖

Tactic:
exact ContinuousLinearMap.le_opNorm _ _

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
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 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:
have I₁ m : ‖iteratedFDeriv ℝ m T (fun _ ↦ L v)‖ ≤
      n.descFactorial m * 1 * (‖L‖ * ‖v‖) ^ (n - m) := by
    have : ‖T‖ ≤ 1 := by
      apply (norm_compContinuousLinearMapLRight_le _ _).trans
      simp only [norm_mkPiAlgebra, le_refl]
    apply (ContinuousMultilinearMap.norm_iteratedFDeriv_le _ _ _).trans
    simp only [Fintype.card_fin]
    gcongr
    refine (pi_norm_le_iff_of_nonneg (by positivity)).mpr (fun _ ↦ ?_)
    exact 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
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) ℝ)
I₁ :
  ∀ (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)
m : ℕ
rw :
  Norm.norm (E :=
      ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin m) ↦ V)
        (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
      (compContinuousLinearMap (M₁ := fun (x : Fin m) ↦ V) (M₁' := fun (i : Fin m) ↦ (i : Fin n) → W →L[ℝ] ℝ)
        (iteratedFDeriv ℝ m (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
            ((ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L :
                (a : V) → (i : Fin n) → W →L[ℝ] ℝ)
              v) :
          ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ (i : Fin n) → W →L[ℝ] ℝ)
            (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
        fun (x : Fin m) ↦
        (ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L :
          ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V ((i : Fin n) → W →L[ℝ] ℝ))) ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
⊢ Norm.norm (E :=
      ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin m) ↦ V)
        (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
      (iteratedFDeriv ℝ m
        (Function.comp (β := (i : Fin n) → W →L[ℝ] ℝ)
          (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
          (⇑(ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) :
            (a : V) → (i : Fin n) → W →L[ℝ] ℝ))
        v) ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m

Tactic:
rw [ContinuousLinearMap.iteratedFDeriv_comp_right _ (ContinuousMultilinearMap.contDiff _)
      _ (mod_cast le_top)]

Premises used: ContinuousMultilinearMap.contDiff, ContinuousLinearMap.iteratedFDeriv_comp_right
-- 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) ℝ)
I₁ :
  ∀ (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)
m : ℕ
simp :
  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) ℝ)
            ((ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L :
                (a : V) → (i : Fin n) → W →L[ℝ] ℝ)
              v) :
          ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ (i : Fin n) → W →L[ℝ] ℝ)
            (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)) *
      Norm.norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V ((i : Fin n) → W →L[ℝ] ℝ))
          (ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) ^
        m ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ 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) ℝ)
            ((ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L :
                (a : V) → (i : Fin n) → W →L[ℝ] ℝ)
              v) :
          ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ (i : Fin n) → W →L[ℝ] ℝ)
            (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)) *
      ∏ i : Fin m,
        Norm.norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V ((i : Fin n) → W →L[ℝ] ℝ))
          (ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m

Tactic:
simp only [Finset.prod_const, Finset.card_fin]

Premises used: Finset.prod_const, Finset.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) ℝ)
I₁ :
  ∀ (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)
m : ℕ
h₁ :
  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) ℝ)
          ((ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L :
              (a : V) → (i : Fin n) → W →L[ℝ] ℝ)
            v) :
        ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ (i : Fin n) → W →L[ℝ] ℝ)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)) ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m)
h₂ :
  Norm.norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V ((i : Fin n) → W →L[ℝ] ℝ))
      (ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) ≤
    ‖L‖
⊢ 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) ℝ)
            ((ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L :
                (a : V) → (i : Fin n) → W →L[ℝ] ℝ)
              v) :
          ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ (i : Fin n) → W →L[ℝ] ℝ)
            (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)) *
      Norm.norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V ((i : Fin n) → W →L[ℝ] ℝ))
          (ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) ^
        m ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ 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) ℝ)
I₁ :
  ∀ (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)
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) ℝ)
          ((ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L :
              (a : V) → (i : Fin n) → W →L[ℝ] ℝ)
            v) :
        ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ (i : Fin n) → W →L[ℝ] ℝ)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)) ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m)

Tactic:
I₁ m
-- 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) ℝ)
I₁ :
  ∀ (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)
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) ℝ)
          ((ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L :
              (a : V) → (i : Fin n) → W →L[ℝ] ℝ)
            v) :
        ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ (i : Fin n) → W →L[ℝ] ℝ)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)) ≤
    HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m)

Tactic:
exact I₁ m
-- 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) ℝ)
I₁ :
  ∀ (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)
m : ℕ
⊢ Norm.norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V ((i : Fin n) → W →L[ℝ] ℝ))
      (ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) ≤
    ‖L‖

Tactic:
ContinuousLinearMap.norm_pi_le_of_le (fun _ ↦ le_rfl) (norm_nonneg _)

Premises used: le_rfl, ContinuousLinearMap.norm_pi_le_of_le
-- 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) ℝ)
I₁ :
  ∀ (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)
⊢ ∀ (m : ℕ),
    Norm.norm (E :=
        ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin m) ↦ V)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
        (iteratedFDeriv ℝ m
          (Function.comp (β := (i : Fin n) → W →L[ℝ] ℝ)
            (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
            (⇑(ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) :
              (a : V) → (i : Fin n) → W →L[ℝ] ℝ))
          v) ≤
      HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m

Tactic:
have I₂ m : ‖iteratedFDeriv ℝ m (T ∘ (ContinuousLinearMap.pi (fun (_ : Fin n) ↦ L))) v‖ ≤
      (n.descFactorial m * 1 * (‖L‖ * ‖v‖) ^ (n - m)) * ‖L‖ ^ m := by
    rw [ContinuousLinearMap.iteratedFDeriv_comp_right _ (ContinuousMultilinearMap.contDiff _)
      _ (mod_cast le_top)]
    apply (norm_compContinuousLinearMap_le _ _).trans
    simp only [Finset.prod_const, Finset.card_fin]
    gcongr
    · exact I₁ m
    · exact ContinuousLinearMap.norm_pi_le_of_le (fun _ ↦ le_rfl) (norm_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
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) ℝ)
I₁ :
  ∀ (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)
I₂ :
  ∀ (m : ℕ),
    Norm.norm (E :=
        ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin m) ↦ V)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
        (iteratedFDeriv ℝ m
          (Function.comp (β := (i : Fin n) → W →L[ℝ] ℝ)
            (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
            (⇑(ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) :
              (a : V) → (i : Fin n) → W →L[ℝ] ℝ))
          v) ≤
      HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
m : ℕ
apply :
  HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m =
    (↑(n.descFactorial m) : ℝ) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
⊢ Norm.norm (E :=
      ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin m) ↦ V)
        (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
      (iteratedFDeriv ℝ m
        (Function.comp (β := (i : Fin n) → W →L[ℝ] ℝ)
          (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
          (⇑(ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) :
            (a : V) → (i : Fin n) → W →L[ℝ] ℝ))
        v) ≤
    (↑(n.descFactorial m) : ℝ) * ‖L‖ ^ n * ‖v‖ ^ (n - m)

Tactic:
apply (I₂ m).trans (le_of_eq _)

Premises used: LE.le.trans, le_of_eq