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 : ℕ∞ω
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 : ℕ
hm : m ≤ n
⊢ ‖L‖ ^ n = ‖L‖ ^ (m + (n - m))
have rw : ‖L‖ ^ n = ‖L‖ ^ n
Tactic: rw [Nat.add_sub_cancel' hm]
-- 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) ℝ)
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 : ℕ
hm : m ≤ n
⊢ HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m =
    (↑(n.descFactorial m) : ℝ) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
have inl : HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m =
  (↑(n.descFactorial m) : ℝ) * (‖L‖ ^ m * ‖L‖ ^ (n - m)) * ‖v‖ ^ (n - m)
Tactic: rw [show ‖L‖ ^ n = ‖L‖ ^ (m + (n - m)) by rw [Nat.add_sub_cancel' hm], pow_add]
-- 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) ℝ)
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
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) ≤
      (↑(n.descFactorial m) : ℝ) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A :
  ContDiff.{0, u_2, u_3} ℝ (F := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) K fun (y : V) ↦
    (T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) fun (x : Fin n) ↦
      (L : (a : V) → W →L[ℝ] ℝ) y
i : ℕ
hi : i ∈ Finset.range (k + 1)
⊢ (↑(n.descFactorial i) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) k
have h : n.descFactorial i ≤ (n + 1) ^ k
Tactic: norm_cast
-- 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) ℝ)
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
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) ≤
      (↑(n.descFactorial m) : ℝ) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A :
  ContDiff.{0, u_2, u_3} ℝ (F := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) K fun (y : V) ↦
    (T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) fun (x : Fin n) ↦
      (L : (a : V) → W →L[ℝ] ℝ) y
i : ℕ
hi : i ∈ Finset.range (k + 1)
⊢ n ^ i ≤ (n + 1) ^ i
have hab : n ≤ n + 1
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) ℝ)
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
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) ≤
      (↑(n.descFactorial m) : ℝ) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A :
  ContDiff.{0, u_2, u_3} ℝ (F := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) K fun (y : V) ↦
    (T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) fun (x : Fin n) ↦
      (L : (a : V) → W →L[ℝ] ℝ) y
i : ℕ
hi : i ∈ Finset.range (k + 1)
⊢ (n + 1) ^ i ≤ (n + 1) ^ k
have ha : 1 ≤ n + 1
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) ℝ)
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
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) ≤
      (↑(n.descFactorial m) : ℝ) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A :
  ContDiff.{0, u_2, u_3} ℝ (F := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) K fun (y : V) ↦
    (T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) fun (x : Fin n) ↦
      (L : (a : V) → W →L[ℝ] ℝ) y
i : ℕ
hi : i ∈ Finset.range (k + 1)
ha : 1 ≤ n + 1
⊢ (n + 1) ^ i ≤ (n + 1) ^ k
have hmn : i ≤ k
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) ℝ)
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
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) ≤
      (↑(n.descFactorial m) : ℝ) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A :
  ContDiff.{0, u_2, u_3} ℝ (F := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) K fun (y : V) ↦
    (T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) fun (x : Fin n) ↦
      (L : (a : V) → W →L[ℝ] ℝ) y
i : ℕ
hi : i ∈ Finset.range (k + 1)
⊢ n.descFactorial i ≤ (n + 1) ^ k
have calc : n ^ i ≤ (n + 1) ^ i
Tactic: calc n.descFactorial i ≤ n ^ i := Nat.descFactorial_le_pow _ _
      _ ≤ (n + 1) ^ i := by gcongr; lia
      _ ≤ (n + 1) ^ k := by gcongr; exacts [le_add_self, Finset.mem_range_succ_iff.mp 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
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
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) ≤
      (↑(n.descFactorial m) : ℝ) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A :
  ContDiff.{0, u_2, u_3} ℝ (F := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) K fun (y : V) ↦
    (T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) fun (x : Fin n) ↦
      (L : (a : V) → W →L[ℝ] ℝ) y
i : ℕ
hi : i ∈ Finset.range (k + 1)
calc : n ^ i ≤ (n + 1) ^ i
⊢ n.descFactorial i ≤ (n + 1) ^ k
have calc₁ : (n + 1) ^ i ≤ (n + 1) ^ k
Tactic: calc n.descFactorial i ≤ n ^ i := Nat.descFactorial_le_pow _ _
      _ ≤ (n + 1) ^ i := by gcongr; lia
      _ ≤ (n + 1) ^ k := by gcongr; exacts [le_add_self, Finset.mem_range_succ_iff.mp 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
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
hf : AEStronglyMeasurable f μ
n : ℕ
⊢ AEStronglyMeasurable (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ VectorFourier.fourierPowSMulRight L f v n) μ
have simp_rw : AEStronglyMeasurable (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
  (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]