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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
⊢ Integrable (ε := ℝ)
    (fun (v : V) ↦
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
        ‖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 apply : ∀ (p : ℕ × ℕ) (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1)),
  Integrable (ε := ℝ)
    (fun (a : V) ↦
      ‖a‖ ^ p.1 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
          (iteratedFDeriv ℝ p.2 f a))
    μ
Tactic: apply integrable_finsetSum _ (fun p hp ↦ ?_)
-- 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
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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
p : ℕ × ℕ
hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1)
⊢ Integrable (ε := ℝ)
    (fun (a : V) ↦
      ‖a‖ ^ p.1 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
          (iteratedFDeriv ℝ p.2 f a))
    μ
have hp₁ : p.1 ≤ k ∧ p.2 ≤ m
Tactic: simp only [Finset.mem_product, Finset.mem_range_succ_iff] at hp
Cleared hypotheses: hp
-- 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
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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
⊢ Integrable (ε :=
    ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ V)
      (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
    (iteratedFDeriv ℝ m fun (v : V) ↦ fourierPowSMulRight L f v k) μ
have I : Integrable (ε := ℝ)
  (fun (v : V) ↦
    ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
      ‖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))
  μ
Tactic: have I : Integrable (fun v ↦ ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
        ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ := by
      apply integrable_finsetSum _ (fun p hp ↦ ?_)
      simp only [Finset.mem_product, Finset.mem_range_succ_iff] at hp
      exact h'f _ _ ((Nat.cast_le.2 hp.1).trans hk) ((Nat.cast_le.2 hp.2).trans 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
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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
I :
  Integrable (ε := ℝ)
    (fun (v : V) ↦
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
        ‖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))
    μ
⊢ Integrable (ε :=
    ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ V)
      (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
    (iteratedFDeriv ℝ m fun (v : V) ↦ fourierPowSMulRight L f v k) μ
have apply : ∀ᵐ (a : V) ∂μ,
  Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (iteratedFDeriv ℝ m (fun (v : V) ↦ fourierPowSMulRight L f v k) a) ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ m * ‖L‖ ^ k *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
        ‖a‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f a)
Tactic: apply (I.const_mul ((2 * π) ^ k * (2 * k + 2) ^ m * ‖L‖ ^ k)).mono'
      ((hf.fourierPowSMulRight L k).continuous_iteratedFDeriv (mod_cast hm)).aestronglyMeasurable
-- 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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
I :
  Integrable (ε := ℝ)
    (fun (v : V) ↦
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
        ‖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))
    μ
⊢ ∀ᵐ (a : V) ∂μ,
    Norm.norm (E :=
        ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ V)
          (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
        (iteratedFDeriv ℝ m (fun (v : V) ↦ fourierPowSMulRight L f v k) a) ≤
      (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ m * ‖L‖ ^ k *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
          ‖a‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f a)
have h : ∀ (v : V),
  Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (iteratedFDeriv ℝ m (fun (v : V) ↦ fourierPowSMulRight L f v k) v) ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ m * ‖L‖ ^ k *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
        ‖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)
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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
I :
  Integrable (ε := ℝ)
    (fun (v : V) ↦
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
        ‖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 m) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (iteratedFDeriv ℝ m (fun (v : V) ↦ fourierPowSMulRight L f v k) v) ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ m * ‖L‖ ^ k *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
        ‖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 h : ∀ (i : ℕ) (hi : i ≤ m) (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) ≤
    ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
      ‖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)
Tactic: refine norm_iteratedFDeriv_fourierPowSMulRight _ hf (mod_cast hm) (fun i hi j hj ↦ ?_)
-- 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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
I :
  Integrable (ε := ℝ)
    (fun (v : V) ↦
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
        ‖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 ≤ m
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) ≤
    ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
      ‖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 h : ∀ i ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
I :
  Integrable (ε := ℝ)
    (fun (v : V) ↦
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
        ‖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 ≤ m
j : ℕ
hj : j ≤ k
h :
  ∀ i ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 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) ≤
    ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1),
      ‖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 h₁ : (j, i) ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 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
⊢ Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)) w n) ≤
    (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 : Norm.norm (E :=
    ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
      (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (iteratedFDeriv ℝ n fun (v : V) ↦ fourierPowSMulRight L f v k) w) ≤
  (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) ∂μ
Tactic: rw [fourierPowSMulRight_iteratedFDeriv_fourierIntegral L hf h'f hk 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
⊢ Norm.norm (E :=
      ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ V)
        (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E))
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (iteratedFDeriv ℝ n fun (v : V) ↦ fourierPowSMulRight L f v k) w) ≤
    (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 apply : ∫ (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) ∂μ
Tactic: apply (norm_fourierIntegral_le_integral_norm _ _ _ _ _).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
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
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))
    μ
have hp₁ : p.1 ≤ k ∧ p.2 ≤ n
Tactic: simp only [Finset.mem_product, Finset.mem_range_succ_iff] at hp
Cleared hypotheses: hp
-- 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
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
⊢ ∫ (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 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))
    μ
Tactic: have I p (hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)) :
      Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ := by
    simp only [Finset.mem_product, Finset.mem_range_succ_iff] at hp
    exact h'f _ _ (le_trans (by simpa using hp.1) hk) (le_trans (by simpa using hp.2) hn)