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
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        Integrable (ε := ℝ)
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          μ
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : W
I :
  ∀ (p : ℕ × ℕ) (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)),
    Integrable (ε := ℝ)
      (fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v))
      μ
⊢ ∫ (v : V),
      Norm.norm (E :=
        ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
          (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
        (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) v) ∂μ ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n * ‖L‖ ^ k *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        ∫ (v : V),
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v) ∂μ
have rw : LE.le (α := ℝ)
  (∫ (v : V),
    Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) v) ∂μ)
  (∫ (a : V),
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n * ‖L‖ ^ k *
      ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        ‖a‖ ^ i.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
            (iteratedFDeriv ℝ i.2 f a) ∂μ)
Tactic: rw [← integral_finsetSum _ I, ← integral_const_mul]
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        Integrable (ε := ℝ)
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          μ
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : W
I :
  ∀ (p : ℕ × ℕ) (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)),
    Integrable (ε := ℝ)
      (fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v))
      μ
⊢ LE.le (α := ℝ)
    (∫ (v : V),
      Norm.norm (E :=
        ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
          (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
        (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) v) ∂μ)
    (∫ (a : V),
      (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n * ‖L‖ ^ k *
        ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          ‖a‖ ^ i.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
              (iteratedFDeriv ℝ i.2 f a) ∂μ)
have hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : V) ↦
  Norm.norm (E :=
    ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
      (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
    (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) a)
Tactic: apply integral_mono_of_nonneg
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        Integrable (ε := ℝ)
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          μ
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : W
I :
  ∀ (p : ℕ × ℕ) (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)),
    Integrable (ε := ℝ)
      (fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v))
      μ
hf₁ :
  (ae μ).EventuallyLE (β := ℝ) 0 fun (a : V) ↦
    Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) a)
⊢ LE.le (α := ℝ)
    (∫ (v : V),
      Norm.norm (E :=
        ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
          (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
        (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) v) ∂μ)
    (∫ (a : V),
      (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n * ‖L‖ ^ k *
        ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          ‖a‖ ^ i.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
              (iteratedFDeriv ℝ i.2 f a) ∂μ)
have hgi : Integrable (ε := ℝ)
  (fun (a : V) ↦
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n * ‖L‖ ^ k *
      ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        ‖a‖ ^ i.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
            (iteratedFDeriv ℝ i.2 f a))
  μ
Tactic: apply integral_mono_of_nonneg
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        Integrable (ε := ℝ)
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          μ
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : W
I :
  ∀ (p : ℕ × ℕ) (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)),
    Integrable (ε := ℝ)
      (fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v))
      μ
hf₁ :
  (ae μ).EventuallyLE (β := ℝ) 0 fun (a : V) ↦
    Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) a)
hgi :
  Integrable (ε := ℝ)
    (fun (a : V) ↦
      (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n * ‖L‖ ^ k *
        ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          ‖a‖ ^ i.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
              (iteratedFDeriv ℝ i.2 f a))
    μ
⊢ LE.le (α := ℝ)
    (∫ (v : V),
      Norm.norm (E :=
        ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
          (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
        (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) v) ∂μ)
    (∫ (a : V),
      (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n * ‖L‖ ^ k *
        ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          ‖a‖ ^ i.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
              (iteratedFDeriv ℝ i.2 f a) ∂μ)
have h : (ae μ).EventuallyLE (β := ℝ)
  (fun (a : V) ↦
    Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) a))
  fun (a : V) ↦
  (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n * ‖L‖ ^ k *
    ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
      ‖a‖ ^ i.1 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
          (iteratedFDeriv ℝ i.2 f a)
Tactic: apply integral_mono_of_nonneg
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        Integrable (ε := ℝ)
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          μ
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : W
I :
  ∀ (p : ℕ × ℕ) (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)),
    Integrable (ε := ℝ)
      (fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v))
      μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : V) ↦
    Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) a)
have hf₁ : ∀ (a : V),
  Membership.mem (γ := Set V)
    {x : V |
      (fun (x : V) ↦
          LE.le (α := ℝ) (0 x)
            ((fun (a : V) ↦
                Norm.norm (E :=
                  ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
                    (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
                  (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) a))
              x))
        x}
    a
Tactic: filter_upwards with v using norm_nonneg _
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        Integrable (ε := ℝ)
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          μ
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : W
I :
  ∀ (p : ℕ × ℕ) (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)),
    Integrable (ε := ℝ)
      (fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v))
      μ
hf₁ :
  ∀ (a : V),
    Membership.mem (γ := Set V)
      {x : V |
        (fun (x : V) ↦
            LE.le (α := ℝ) (0 x)
              ((fun (a : V) ↦
                  Norm.norm (E :=
                    ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
                      (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
                    (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) a))
                x))
          x}
      a
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : V) ↦
    Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) a)
have hf₂ : ∀ (a : V),
  0 a ≤
    Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) a)
Tactic: filter_upwards with v using norm_nonneg _
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        Integrable (ε := ℝ)
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          μ
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : W
I :
  ∀ (p : ℕ × ℕ) (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)),
    Integrable (ε := ℝ)
      (fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v))
      μ
⊢ (ae μ).EventuallyLE (β := ℝ)
    (fun (a : V) ↦
      Norm.norm (E :=
        ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
          (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
        (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) a))
    fun (a : V) ↦
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n * ‖L‖ ^ k *
      ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        ‖a‖ ^ i.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
            (iteratedFDeriv ℝ i.2 f a)
have h : ∀ (v : V),
  Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) v) ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n * ‖L‖ ^ k *
      ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        ‖v‖ ^ i.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
            (iteratedFDeriv ℝ i.2 f v)
Tactic: filter_upwards with v
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        Integrable (ε := ℝ)
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          μ
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : W
I :
  ∀ (p : ℕ × ℕ) (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)),
    Integrable (ε := ℝ)
      (fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v))
      μ
v : V
⊢ Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (iteratedFDeriv ℝ n (fun (v : V) ↦ fourierPowSMulRight L f v k) v) ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n * ‖L‖ ^ k *
      ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        ‖v‖ ^ i.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
            (iteratedFDeriv ℝ i.2 f v)
have apply : ∀ i ≤ n,
  ∀ j ≤ k,
    ‖v‖ ^ j *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E) (iteratedFDeriv ℝ i f v) ≤
      ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        ‖v‖ ^ i.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
            (iteratedFDeriv ℝ i.2 f v)
Tactic: apply norm_iteratedFDeriv_fourierPowSMulRight _ hf (mod_cast hn) _
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        Integrable (ε := ℝ)
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          μ
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : W
I :
  ∀ (p : ℕ × ℕ) (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)),
    Integrable (ε := ℝ)
      (fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v))
      μ
v : V
i : ℕ
hi : i ≤ n
j : ℕ
hj : j ≤ k
⊢ ‖v‖ ^ j *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E) (iteratedFDeriv ℝ i f v) ≤
    ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
      ‖v‖ ^ i.1 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
          (iteratedFDeriv ℝ i.2 f v)
have hf₁ : ∀ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
  LE.le (α := ℝ) 0
    ((fun (p : ℕ × ℕ) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v))
      i)
Tactic: apply Finset.single_le_sum (f := fun p ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) (a := (j, i))
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        Integrable (ε := ℝ)
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          μ
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : W
I :
  ∀ (p : ℕ × ℕ) (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)),
    Integrable (ε := ℝ)
      (fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v))
      μ
v : V
i : ℕ
hi : i ≤ n
j : ℕ
hj : j ≤ k
hf₁ :
  ∀ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
    LE.le (α := ℝ) 0
      ((fun (p : ℕ × ℕ) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v))
        i)
⊢ ‖v‖ ^ j *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E) (iteratedFDeriv ℝ i f v) ≤
    ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
      ‖v‖ ^ i.1 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i.2) ↦ V) E)
          (iteratedFDeriv ℝ i.2 f v)
have h : (j, i) ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)
Tactic: apply Finset.single_le_sum (f := fun p ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) (a := (j, i))
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        Integrable (ε := ℝ)
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          μ
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : W
I :
  ∀ (p : ℕ × ℕ) (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)),
    Integrable (ε := ℝ)
      (fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v))
      μ
v : V
i : ℕ
hi : i ≤ n
j : ℕ
hj : j ≤ k
⊢ (j, i) ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)
have h : j ≤ k ∧ i ≤ n
Tactic: simp only [Finset.mem_product, Finset.mem_range_succ_iff]