awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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
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) ∂μ
⊢ 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:
apply (norm_fourierIntegral_le_integral_norm _ _ _ _ _).trans

Premises used: LE.le.trans, VectorFourier.norm_fourierIntegral_le_integral_norm
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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)
⊢ p.1 ≤ k ∧ p.2 ≤ n

Tactic:
simp only [Finset.mem_product, Finset.mem_range_succ_iff] at hp

Premises used: Finset.mem_range_succ_iff, Finset.mem_product
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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.1 ≤ k ∧ p.2 ≤ n
⊢ LE.le (α := ℕ∞) (↑p.1 : ℕ∞) (↑k : ℕ∞)

Tactic:
simpa using hp.1

Premises used: And.left
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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.1 ≤ k ∧ p.2 ≤ n
⊢ LE.le (α := ℕ∞) (↑p.2 : ℕ∞) (↑n : ℕ∞)

Tactic:
simpa using hp.2

Premises used: And.right
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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.1 ≤ k ∧ p.2 ≤ n
⊢ 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:
exact h'f _ _ (le_trans (by simpa using hp.1) hk) (le_trans (by simpa using hp.2) hn)

Premises used: le_trans
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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))
      μ

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)
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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))
      μ
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) ∂μ)
⊢ ∫ (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:
rw [← integral_finsetSum _ I, ← integral_const_mul]

Premises used: MeasureTheory.integral_const_mul, MeasureTheory.integral_finsetSum
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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))
    μ
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)
⊢ 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:
apply integral_mono_of_nonneg

Premises used: MeasureTheory.integral_mono_of_nonneg
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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
⊢ 0 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)

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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
hf₂ hf₃ :
  ∀ (v : V),
    0 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)
⊢ (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:
filter_upwards with v using norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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))
      μ
⊢ 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:
(integrable_finsetSum _ I).const_mul _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.integrable_finsetSum
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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))
      μ
⊢ 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:
exact (integrable_finsetSum _ I).const_mul _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.integrable_finsetSum
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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))
      μ
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)
⊢ (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:
filter_upwards with v