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
v : V
w : W
⊢ HPow.hPow (α := ℝ) (|(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w| : ℝ) n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E)
        (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w) ≤
    (2 * π) ^ n *
      (HPow.hPow (α := ℝ) (|(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w| : ℝ) n *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin k) ↦ W) E)
          (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w))
have apply : 1 ≤ (2 * π) ^ n
Tactic: apply le_mul_of_one_le_left (by positivity)
-- 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
v : V
w : W
⊢ 1 ≤ (2 * π) ^ n
have ha : 1 ≤ 2 * π
Tactic: apply one_le_pow₀
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
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
v : V
w : W
⊢ 1 ≤ 2 * π
have linarith : 2 * π < 1 → 2 / 2 = 1
Tactic: linarith [one_le_pi_div_two]
-- 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
v : V
w : W
linarith : 2 * π < 1 → 2 / 2 = 1
⊢ 1 ≤ 2 * π
have linarith₁ : 2 * π < 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [one_le_pi_div_two]
-- 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
v : V
w : W
linarith : 2 * π < 1 → 2 / 2 = 1
linarith₁ : 2 * π < 1 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 ≤ 2 * π
have linarith₂ : 2 * π < 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith [one_le_pi_div_two]
-- 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
v : V
w : W
linarith : 2 * π < 1 → 2 / 2 = 1
linarith₁ : 2 * π < 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * π < 1 → GT.gt (α := ℝ) 2 0
⊢ 1 ≤ 2 * π
have linarith₃ : 2 * π < 1 → HMul.hMul (α := ℝ) 3 (-1) + (2 * π - 1) + 2 * (HMul.hMul (α := ℝ) 2 1 - 1 * π) = 0
Tactic: linarith [one_le_pi_div_two]
-- 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
v : V
w : W
linarith : 2 * π < 1 → 2 / 2 = 1
linarith₁ : 2 * π < 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * π < 1 → GT.gt (α := ℝ) 2 0
linarith₃ : 2 * π < 1 → HMul.hMul (α := ℝ) 3 (-1) + (2 * π - 1) + 2 * (HMul.hMul (α := ℝ) 2 1 - 1 * π) = 0
⊢ 1 ≤ 2 * π
have linarith₄ : 2 * π < 1 → GT.gt (α := ℝ) 3 0
Tactic: linarith [one_le_pi_div_two]
-- 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
v : V
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) *
      ∏ x : Fin n, ‖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) ∂μ) *
      ‖v‖ ^ n
have h₁ : 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) ∂μ
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
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
v : V
w : W
h₁ :
  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) ∂μ
⊢ 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) *
      ∏ x : Fin n, ‖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) ∂μ) *
      ‖v‖ ^ n
have h₂ : ∏ x : Fin n, ‖v‖ ≤ ‖v‖ ^ n
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
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
v : V
w : 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) ∂μ) *
      ‖v‖ ^ n =
    ‖v‖ ^ n * (2 * π * ‖L‖) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ 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 simp : (HPow.hPow (α := ℝ) 2 k * π ^ 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) ∂μ) *
    ‖v‖ ^ n =
  ‖v‖ ^ n * (HPow.hPow (α := ℝ) 2 k * π ^ k * ‖L‖ ^ k) * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
    ∑ 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: simp [mul_pow]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : Differentiable ℝ f
hf' : @Integrable (V →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fderiv ℝ f) volume
⊢ 𝓕 (E := (x : V) → V →L[ℝ] E) (fderiv ℝ f) = fourierSMulRight (-innerSL ℝ) (𝓕 f)
have rw : 𝓕 (E := (x : V) → V →L[ℝ] E) (fderiv ℝ f) = fourierSMulRight (-ContinuousLinearMap.flip (innerSL ℝ)) (𝓕 f)
Tactic: rw [← flip_innerSL_real 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
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (n : ℕ),
    (↑n : ℕ∞) ≤ N →
      @Integrable (ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) _ _ _ inst_5
        (iteratedFDeriv ℝ n f) (volume : Measure V)
n : ℕ
hn : (↑n : ℕ∞) ≤ N
⊢ 𝓕 (E := V → ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) (iteratedFDeriv ℝ n f) =
    fun (w : V) ↦ fourierPowSMulRight (-innerSL ℝ) (𝓕 f) w n
have rw : 𝓕 (E := V → ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) (iteratedFDeriv ℝ n f) = fun (w : V) ↦
  fourierPowSMulRight (-ContinuousLinearMap.flip (innerSL ℝ)) (𝓕 f) w n
Tactic: rw [← flip_innerSL_real V]
-- 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
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (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))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : V
⊢ ‖w‖ ^ n *
      (‖w‖ ^ n *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) w)) ≤
    ‖w‖ ^ n *
      ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume 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 this : HPow.hPow (α := ℝ) (|(((innerSL ℝ : (a : V) → V →L[ℝ] ℝ) w : V →L[ℝ] ℝ) : (a : V) → ℝ) w| : ℝ) n *
    Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
      (iteratedFDeriv ℝ k (fourierIntegral 𝐞 (volume : Measure V) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) f)
        w) ≤
  ‖w‖ ^ n * (2 * π * Norm.norm.{u_2} (E := V →L[ℝ] V →L[ℝ] ℝ) (innerSL ℝ)) ^ k *
      (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
    ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
      @integral _ _ _ _ inst_5 (volume : Measure V) 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 := VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le (innerSL ℝ) hf h'f hk hn
      w w
-- 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
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (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))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : V
this :
  HPow.hPow (α := ℝ) (|(((innerSL ℝ : (a : V) → V →L[ℝ] ℝ) w : V →L[ℝ] ℝ) : (a : V) → ℝ) w| : ℝ) n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (fourierIntegral 𝐞 (volume : Measure V) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) f)
          w) ≤
    ‖w‖ ^ n * (2 * π * Norm.norm.{u_2} (E := V →L[ℝ] V →L[ℝ] ℝ) (innerSL ℝ)) ^ k *
        (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ inst_5 (volume : Measure V) 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)
⊢ ‖w‖ ^ n *
      (‖w‖ ^ n *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) w)) ≤
    ‖w‖ ^ n *
      ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume 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 this₁ : HPow.hPow (β := ℕ) ‖w‖ 2 ^ n *
    Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
      (iteratedFDeriv ℝ k (fourierIntegral 𝐞 (volume : Measure V) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) f)
        w) ≤
  ‖w‖ ^ n *
    ((2 * (π * Norm.norm.{u_2} (E := V →L[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          @integral _ _ _ _ inst_5 (volume : Measure V) 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: simp only [innerSL_apply_apply _ w w, real_inner_self_eq_norm_sq w, abs_pow, abs_norm,
      mul_assoc] at this
Cleared hypotheses: this
-- 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
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (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))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : V
⊢ ‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume 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 Z : ‖w‖ ^ n *
    (‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w)) ≤
  ‖w‖ ^ n *
    ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume 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 Z : ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
      ‖w‖ ^ n * ((2 * (π * ‖innerSL (E := V) ℝ‖)) ^ k * ((2 * k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂volume)) := by
    have := VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le (innerSL ℝ) hf h'f hk hn
      w w
    simp only [innerSL_apply_apply _ w w, real_inner_self_eq_norm_sq w, abs_pow, abs_norm,
      mul_assoc] at this
    rwa [pow_two, mul_pow, mul_assoc] at this