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
μ : Measure V
inst_8 : SecondCountableTopology V
hf : AEStronglyMeasurable f μ
n : ℕ
⊢ AEStronglyMeasurable (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦
      HSMul.hSMul (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E) ((-(2 * (↑π : ℂ) * I)) ^ n)
        (((smulRightL ℝ (fun (x : Fin n) ↦ W) E :
                  (a : ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) →
                    E →L[ℝ] ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
                ((compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
                      (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
                    (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
                  fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) :
              (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
            (f v) :
          ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E))
    μ
have hf₁ : AEStronglyMeasurable (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
  (fun (x : V) ↦
    ((smulRightL ℝ (fun (x : Fin n) ↦ W) E :
            (a : ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) →
              E →L[ℝ] ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
          ((compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
                (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
              (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
            fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x) :
        (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
      (f x))
  μ
Tactic: apply AEStronglyMeasurable.const_smul'
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
hf : AEStronglyMeasurable f μ
n : ℕ
⊢ AEStronglyMeasurable (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (x : V) ↦
      ((smulRightL ℝ (fun (x : Fin n) ↦ W) E :
              (a : ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) →
                E →L[ℝ] ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
            ((compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
                  (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
                (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
              fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x) :
          (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
        (f x))
    μ
have apply : AEStronglyMeasurable.{u_2, u_3} (β := ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
  (fun (x : V) ↦
    (compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
          (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
        (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
      fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x)
  μ
Tactic: apply (smulRightL ℝ (fun (_ : Fin n) ↦ W) E).continuous₂.comp_aestronglyMeasurable₂ _ hf
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
hf : AEStronglyMeasurable f μ
n : ℕ
⊢ AEStronglyMeasurable.{u_2, u_3} (β := ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
    (fun (x : V) ↦
      (compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
            (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
          (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
        fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x)
    μ
have hf₁ : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : V) ↦
  (compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
        (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
      (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
    fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x
Tactic: apply Continuous.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
μ : Measure V
inst_8 : SecondCountableTopology V
n : ℕ
hf : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
⊢ Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
have refine : ∀ᵐ (a : V) ∂μ,
  Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) (fourierPowSMulRight L f a n) ≤
    (2 * π * ‖L‖) ^ n * (‖a‖ ^ n * ‖f a‖)
Tactic: refine (hf.const_mul ((2 * π * ‖L‖) ^ n)).mono' (h'f.fourierPowSMulRight L n) ?_
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
n : ℕ
hf : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
⊢ ∀ᵐ (a : V) ∂μ,
    Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) (fourierPowSMulRight L f a n) ≤
      (2 * π * ‖L‖) ^ n * (‖a‖ ^ n * ‖f a‖)
have h : ∀ (v : V),
  Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) (fourierPowSMulRight L f v n) ≤
    (2 * π * ‖L‖) ^ n * (‖v‖ ^ n * ‖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
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
⊢ HasFTaylorSeriesUpTo (𝕜 := ℝ) N (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) fun (w : W) (n : ℕ) ↦
    fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) w
have zero_eq : ∀ (x : W),
  curry0.{0, u_3, u_1} (𝕜 := ℝ) (G := W)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v 0) x) =
    fourierIntegral 𝐞 μ L.toLinearMap₁₂ f x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
zero_eq :
  ∀ (x : W),
    curry0.{0, u_3, u_1} (𝕜 := ℝ) (G := W)
        (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v 0) x) =
      fourierIntegral 𝐞 μ L.toLinearMap₁₂ f x
⊢ HasFTaylorSeriesUpTo (𝕜 := ℝ) N (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) fun (w : W) (n : ℕ) ↦
    fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) w
have fderiv : ∀ (m : ℕ),
  (↑m : ℕ∞ω) < N →
    ∀ (x : W),
      HasFDerivAt (𝕜 := ℝ) (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin m) ↦ W) E)
        (fun (y : W) ↦ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v m) y)
        (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin m.succ) ↦ W) (G := E)
          (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v m.succ) x))
        x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
zero_eq :
  ∀ (x : W),
    curry0.{0, u_3, u_1} (𝕜 := ℝ) (G := W)
        (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v 0) x) =
      fourierIntegral 𝐞 μ L.toLinearMap₁₂ f x
fderiv :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) < N →
      ∀ (x : W),
        HasFDerivAt (𝕜 := ℝ) (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin m) ↦ W) E)
          (fun (y : W) ↦ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v m) y)
          (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin m.succ) ↦ W) (G := E)
            (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v m.succ) x))
          x
⊢ HasFTaylorSeriesUpTo (𝕜 := ℝ) N (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) fun (w : W) (n : ℕ) ↦
    fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) w
have cont : ∀ (m : ℕ),
  (↑m : ℕ∞ω) ≤ N →
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : W) ↦
      fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v m) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
w : W
⊢ curry0.{0, u_3, u_1} (𝕜 := ℝ) (G := W)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v 0) w) =
    fourierIntegral 𝐞 μ L.toLinearMap₁₂ f w
have zero_eq : fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (x : V) ↦ (fourierPowSMulRight L f x 0 : (a : (i : Fin 0) → W) → E) ![]) w =
  fourierIntegral 𝐞 μ L.toLinearMap₁₂ f w
Tactic: rw [curry0_apply, Matrix.zero_empty, fourierIntegral_continuousMultilinearMap_apply'
      (integrable_fourierPowSMulRight L (hf 0 bot_le) h'f)]
-- 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
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
⊢ HasFDerivAt (𝕜 := ℝ) (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (y : W) ↦ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) y)
    (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin n.succ) ↦ W) (G := E)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n.succ) w))
    w
have I₁ : Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
  (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
Tactic: have I₁ : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ :=
      integrable_fourierPowSMulRight L (hf n hn.le) h'f
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
⊢ Integrable (ε := ℝ)
    (fun (v : V) ↦
      ‖v‖ *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
          (fourierPowSMulRight L f v n))
    μ
have apply : ∀ᵐ (a : V) ∂μ,
  ‖HMul.hMul (α := V → ℝ) (β := V → ℝ) (fun (a : V) ↦ ‖a‖)
        (fun (x : V) ↦
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
            (fourierPowSMulRight L f x n))
        a‖ ≤
    (2 * π * ‖L‖) ^ n * (‖a‖ ^ (n + 1) * ‖f a‖)
Tactic: apply ((hf (n + 1) (ENat.add_one_natCast_le_withTop_of_lt hn)).const_mul
          ((2 * π * ‖L‖) ^ n)).mono'
        (continuous_norm.aestronglyMeasurable.mul (h'f.fourierPowSMulRight L n).norm)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
⊢ ∀ᵐ (a : V) ∂μ,
    ‖HMul.hMul (α := V → ℝ) (β := V → ℝ) (fun (a : V) ↦ ‖a‖)
          (fun (x : V) ↦
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
              (fourierPowSMulRight L f x n))
          a‖ ≤
      (2 * π * ‖L‖) ^ n * (‖a‖ ^ (n + 1) * ‖f a‖)
have h : ∀ (v : V),
  ‖HMul.hMul (α := V → ℝ) (β := V → ℝ) (fun (a : V) ↦ ‖a‖)
        (fun (x : V) ↦
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
            (fourierPowSMulRight L f x n))
        v‖ ≤
    (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖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
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
v : V
⊢ ‖HMul.hMul (α := V → ℝ) (β := V → ℝ) (fun (a : V) ↦ ‖a‖)
        (fun (x : V) ↦
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
            (fourierPowSMulRight L f x n))
        v‖ ≤
    (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖)
have h : ‖v‖ *
    Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) (fourierPowSMulRight L f v n) ≤
  (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖)
Tactic: simp only [Pi.mul_apply, norm_mul, norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
v : V
⊢ ‖v‖ *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
        (fourierPowSMulRight L f v n) ≤
    ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖)
have hbc : Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) (fourierPowSMulRight L f v n) ≤
  (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖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
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
v : V
⊢ ‖v‖ *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
        (fourierPowSMulRight L f v n) ≤
    (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖)
have L₁ : ‖v‖ *
    Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) (fourierPowSMulRight L f v n) ≤
  ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖)
Tactic: calc
      ‖v‖ * ‖fourierPowSMulRight L f v n‖
        ≤ ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖) := by
          gcongr; apply norm_fourierPowSMulRight_le
      _ = (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖) := by rw [pow_succ]; ring
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
v : V
L₁ :
  ‖v‖ *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
        (fourierPowSMulRight L f v n) ≤
    ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖)
⊢ ‖v‖ *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
        (fourierPowSMulRight L f v n) ≤
    (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖)
have L₂ : ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖) = (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖)
Tactic: calc
      ‖v‖ * ‖fourierPowSMulRight L f v n‖
        ≤ ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖) := by
          gcongr; apply norm_fourierPowSMulRight_le
      _ = (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖) := by rw [pow_succ]; ring
-- 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
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
⊢ HasFDerivAt (𝕜 := ℝ) (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (y : W) ↦ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) y)
    (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin n.succ) ↦ W) (G := E)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n.succ) w))
    w
have I₂ : Integrable (ε := ℝ)
  (fun (v : V) ↦
    ‖v‖ *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
        (fourierPowSMulRight L f v n))
  μ
Tactic: have I₂ : Integrable (fun v ↦ ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ := by
      apply ((hf (n + 1) (ENat.add_one_natCast_le_withTop_of_lt hn)).const_mul
          ((2 * π * ‖L‖) ^ n)).mono'
        (continuous_norm.aestronglyMeasurable.mul (h'f.fourierPowSMulRight L n).norm)
      filter_upwards with v
      simp only [Pi.mul_apply, norm_mul, norm_norm]
      calc
      ‖v‖ * ‖fourierPowSMulRight L f v n‖
        ≤ ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖) := by
          gcongr; apply norm_fourierPowSMulRight_le
      _ = (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖) := by rw [pow_succ]; ring