awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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 ℝ (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) k fun (v : V) ↦
    VectorFourier.fourierPowSMulRight L f v n
have simp_rw : 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: simp_rw [fourierPowSMulRight_eq_comp]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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 ℝ (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)
have 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)
Tactic: apply ContDiff.const_smul
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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 ℝ (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)
have 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
Tactic: apply (smulRightL ℝ (fun (_ : Fin n) ↦ W) E).isBoundedBilinearMap.contDiff.comp₂ _ hf
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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 := 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
have 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
Tactic: apply (ContinuousMultilinearMap.contDiff _).comp
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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 : ℕ
⊢ 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‖
have 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‖
Tactic: apply ContinuousMultilinearMap.opNorm_le_bound (by positivity) (fun m ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
⊢ (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‖)
have 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‖
Tactic: gcongr with i _hi
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
⊢ (2 * π) ^ n * ((∏ x : Fin n, ‖L‖ * ‖v‖ * ‖m x‖) * ‖f v‖) = (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ i : Fin n, ‖m i‖
have 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‖
Tactic: simp [Finset.prod_mul_distrib, mul_pow]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ i : Fin n, ‖m i‖
have 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‖)
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
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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‖)
⊢ 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‖
have 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‖)
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
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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‖)
⊢ 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‖
have L₃ : (2 * π) ^ n * ((∏ x : Fin n, ‖L‖ * ‖v‖ * ‖m x‖) * ‖f v‖) = (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
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
⊢ 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
have 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
Tactic: simp_rw [fourierPowSMulRight_eq_comp]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
have apply : Norm.norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ) (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) ≤
  1
Tactic: apply (norm_compContinuousLinearMapLRight_le _ _).trans
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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)
have this : ‖T‖ ≤ 1
Tactic: have : ‖T‖ ≤ 1 := by
      apply (norm_compContinuousLinearMapLRight_le _ _).trans
      simp only [norm_mkPiAlgebra, le_refl]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
⊢ 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)
have 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)
Tactic: apply (ContinuousMultilinearMap.norm_iteratedFDeriv_le _ _ _).trans
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
⊢ (↑((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)
have 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)
Tactic: simp only [Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
⊢ (↑(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)
have h₂ : (Norm.norm.{u_3} (E := (i : Fin n) → W →L[ℝ] ℝ) fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) ≤ ‖L‖ * ‖v‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
⊢ (Norm.norm.{u_3} (E := (i : Fin n) → W →L[ℝ] ℝ) fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) ≤ ‖L‖ * ‖v‖
have h₂ : ∀ (x : Fin n), Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) ≤ ‖L‖ * ‖v‖
Tactic: refine (pi_norm_le_iff_of_nonneg (by positivity)).mpr (fun _ ↦ ?_)