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
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_1 : (↑n : ℕ∞) ≤ N
w : V
Z :
  ‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (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))
hn : n ≠ 0
hw : w ≠ 0
⊢ (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)) ≤
    (2 * (π * 1)) ^ 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 inr : (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)) ≤
  (2 * (π * 1)) ^ 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: simp only [mul_assoc]
-- 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
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_1 : (↑n : ℕ∞) ≤ N
w : V
Z :
  ‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (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))
hn : n ≠ 0
hw : w ≠ 0
⊢ (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)) ≤
    (2 * (π * 1)) ^ 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 inr : Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ) ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
⊢ HasDerivAt (𝓕 f) (𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x) w) w
have hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
Tactic: have hf'' : Integrable (fun v : ℝ ↦ ‖v‖ * ‖f v‖) := by simpa only [norm_smul] using hf'.norm
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
⊢ @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ fourierSMulRight L f v) volume
have suffices : @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace
  (fun (v : ℝ) ↦ ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v)) volume
Tactic: suffices Integrable fun v ↦ ContinuousLinearMap.smulRight (L v) (f v) by
      simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using this.smul (-2 * π * I)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
⊢ @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ℝ) ↦ ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v)) volume
have h : ∀ (v : ℝ),
  Eq (α := ℝ →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v))
    (((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) : (a : E) → ℝ →L[ℝ] E)
      (v • f v))
Tactic: convert ((ContinuousLinearMap.toSpanSingletonLIE ℝ
      E).toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with _ v
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
v : ℝ
⊢ Eq (α := ℝ →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v))
    (((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) : (a : E) → ℝ →L[ℝ] E)
      (v • f v))
have h : Eq (α := E) ((ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v) : (a : ℝ) → E) 1 : E)
  (((((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) : (a : E) → ℝ →L[ℝ] E)
            (v • f v) :
          ℝ →L[ℝ] E) :
        (a : ℝ) → E)
      1 :
    E)
Tactic: apply ContinuousLinearMap.ext_ring
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
v : ℝ
⊢ Eq (α := E) ((ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v) : (a : ℝ) → E) 1 : E)
    (((((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) :
                (a : E) → ℝ →L[ℝ] E)
              (v • f v) :
            ℝ →L[ℝ] E) :
          (a : ℝ) → E)
        1 :
      E)
have h : v • f v =
  (HSMul.hSMul (β := ℝ →L[ℝ] E) v
        (((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) :
              (a : E) → ℝ →L[ℝ] E)
            (f v) :
          ℝ →L[ℝ] E) :
      (a : ℝ) → E)
    1
Tactic: rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.flip_apply,
      ContinuousLinearMap.mul_apply', one_mul, map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
⊢ HasDerivAt (𝓕 f) (𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x) w) w
have h_int : @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ fourierSMulRight L f v) volume
Tactic: have h_int : Integrable fun v ↦ fourierSMulRight L f v := by
    suffices Integrable fun v ↦ ContinuousLinearMap.smulRight (L v) (f v) by
      simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using this.smul (-2 * π * I)
    convert ((ContinuousLinearMap.toSpanSingletonLIE ℝ
      E).toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with _ v
    apply ContinuousLinearMap.ext_ring
    rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.flip_apply,
      ContinuousLinearMap.mul_apply', one_mul, map_smul]
    exact congr_arg (fun x ↦ v • x) (one_smul ℝ (f v)).symm
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
h_int :
  @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ fourierSMulRight L f v) volume
⊢ HasDerivAt (𝓕 f) (𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x) w) w
have h : 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x) w =
  (fourierIntegral 𝐞 volume L.toLinearMap₁₂ (fourierSMulRight L f) w : (a : ℝ) → E) 1
Tactic: convert! (VectorFourier.hasFDerivAt_fourierIntegral L hf hf'' w).hasDerivAt using 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
h_int :
  @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ fourierSMulRight L f v) volume
⊢ 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x) w =
    (fourierIntegral 𝐞 volume L.toLinearMap₁₂ (fourierSMulRight L f) w : (a : ℝ) → E) 1
have h : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(v * w)) : Circle) ((-2 * (↑π : ℂ) * I * (↑v : ℂ)) • f v))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
    HSMul.hSMul (α := Circle) (β := E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L.toLinearMap₁₂ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) v : ℝ →ₗ[ℝ] ℝ) : (a : ℝ) → ℝ) w) : Circle)
      ((fourierSMulRight L f v : (a : ℝ) → E) 1 : E))
Tactic: rw [fourierIntegral_continuousLinearMap_apply' h_int, VectorFourier.fourierIntegral,
    fourier_real_eq]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
⊢ deriv (𝓕 f) = 𝓕 (E := (x : ℝ) → E) fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x
have h : ∀ (x : ℝ), deriv (𝓕 f) x = 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : Differentiable ℝ f
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (deriv f) volume
⊢ 𝓕 (deriv f) = fun (x : ℝ) ↦ (2 * (↑π : ℂ) * I * (↑x : ℂ)) • 𝓕 f x
have h : ∀ (x : ℝ), 𝓕 (deriv f) x = (2 * (↑π : ℂ) * I * (↑x : ℂ)) • 𝓕 f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : Differentiable ℝ f
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (deriv f) volume
x : ℝ
⊢ 𝓕 (deriv f) x = (2 * (↑π : ℂ) * I * (↑x : ℂ)) • 𝓕 f x
have I : @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ fderiv ℝ f x) volume
Tactic: have I : Integrable (fun x ↦ fderiv ℝ f x) := by
    simpa only [← toSpanSingleton_deriv] using
      (ContinuousLinearMap.smulRightL ℝ ℝ E 1).integrable_comp hf'
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : Differentiable ℝ f
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (deriv f) volume
x : ℝ
I : @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ fderiv ℝ f x) volume
⊢ 𝓕 (deriv f) x = (2 * (↑π : ℂ) * Complex.I * (↑x : ℂ)) • 𝓕 f x
have this : 𝓕 (deriv f) x = (𝓕 (E := (x : ℝ) → ℝ →L[ℝ] E) (fderiv ℝ f) x : (a : ℝ) → E) 1
Tactic: have : 𝓕 (deriv f) x = 𝓕 (fderiv ℝ f) x 1 := by
    simp only [fourier_continuousLinearMap_apply I, fderiv_apply_one_eq_deriv]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : Differentiable ℝ f
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (deriv f) volume
x : ℝ
I : @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ fderiv ℝ f x) volume
this : 𝓕 (deriv f) x = (𝓕 (E := (x : ℝ) → ℝ →L[ℝ] E) (fderiv ℝ f) x : (a : ℝ) → E) 1
⊢ 𝓕 (deriv f) x = (2 * (↑π : ℂ) * Complex.I * (↑x : ℂ)) • 𝓕 f x
have h : (fourierSMulRight (-innerSL ℝ) (𝓕 f) x : (a : ℝ) → E) 1 = (2 * (↑π : ℂ) * Complex.I * (↑x : ℂ)) • 𝓕 f x
Tactic: rw [this, fourier_fderiv hf h'f I]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable.{u_1, 0} E _ _ _ measurableSpace (fun (x : ℝ) ↦ x ^ n • f x) volume
hn : (↑n : ℕ∞) ≤ N
⊢ iteratedDeriv n (𝓕 f) = 𝓕 (E := (x : ℝ) → E) fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • f x
have h : ∀ (x : ℝ), iteratedDeriv n (𝓕 f) x = 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • f x) x
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n_1 : ℕ
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable.{u_1, 0} E _ _ _ measurableSpace (fun (x : ℝ) ↦ x ^ n • f x) volume
hn_1 : (↑n_1 : ℕ∞) ≤ N
x : ℝ
n : ℕ
hn : (↑n : ℕ∞) ≤ N
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ ^ n * ‖f v‖) volume
have h : ∀ (x : ℝ), ‖x‖ ^ n * ‖f x‖ = ‖x ^ n • f x‖
Tactic: convert! (hf n hn).norm with x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable.{u_1, 0} E _ _ _ measurableSpace (fun (x : ℝ) ↦ x ^ n • f x) volume
hn : (↑n : ℕ∞) ≤ N
x : ℝ
⊢ iteratedDeriv n (𝓕 f) x = 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • f x) x
have A : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ N),
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ ^ n * ‖f v‖) volume
Tactic: have A (n : ℕ) (hn : n ≤ N) : Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) := by
    convert! (hf n hn).norm with x
    simp [norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable.{u_1, 0} E _ _ _ measurableSpace (fun (x : ℝ) ↦ x ^ n • f x) volume
hn : (↑n : ℕ∞) ≤ N
x : ℝ
A :
  ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ N),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ ^ n * ‖f v‖) volume
⊢ iteratedDeriv n (𝓕 f) x = 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • f x) x
have B : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f volume
Tactic: have B : AEStronglyMeasurable f := by simpa using (hf 0 zero_le).1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable.{u_1, 0} E _ _ _ measurableSpace (fun (x : ℝ) ↦ x ^ n • f x) volume
hn : (↑n : ℕ∞) ≤ N
x : ℝ
A :
  ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ N),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f volume
⊢ iteratedDeriv n (𝓕 f) x = 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • f x) x
have h : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
    HSMul.hSMul (α := Circle) (β := E) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle)
      ((fourierPowSMulRight (innerSL ℝ) f v n : (a : (i : Fin n) → ℝ) → E) fun (x : Fin n) ↦ 1 : E))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle)
      ((-2 * (↑π : ℂ) * I * (↑v : ℂ)) ^ n • f v))
Tactic: rw [iteratedDeriv, iteratedFDeriv_fourier A B hn,
    fourier_continuousMultilinearMap_apply (integrable_fourierPowSMulRight _ (A n hn) B),
    fourier_eq, fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable.{u_1, 0} E _ _ _ measurableSpace (fun (x : ℝ) ↦ x ^ n • f x) volume
hn : (↑n : ℕ∞) ≤ N
x : ℝ
A :
  ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ N),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f volume
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (α := Circle) (β := E) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle)
        ((fourierPowSMulRight (innerSL ℝ) f v n : (a : (i : Fin n) → ℝ) → E) fun (x : Fin n) ↦ 1 : E))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle)
        ((-2 * (↑π : ℂ) * I * (↑v : ℂ)) ^ n • f v))
have h : ∀ (y : ℝ),
  HSMul.hSMul (α := Circle) (β := E) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y x) : Circle)
      ((fourierPowSMulRight (innerSL ℝ) f y n : (a : (i : Fin n) → ℝ) → E) fun (x : Fin n) ↦ 1 : E) =
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y x) : Circle)
      ((-2 * (↑π : ℂ) * I * (↑y : ℂ)) ^ n • f y)
Tactic: congr with y
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable.{u_1, 0} E _ _ _ measurableSpace (fun (x : ℝ) ↦ x ^ n • f x) volume
hn : (↑n : ℕ∞) ≤ N
x : ℝ
A :
  ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ N),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f volume
y : ℝ
⊢ HSMul.hSMul (α := Circle) (β := E) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y x) : Circle)
      ((fourierPowSMulRight (innerSL ℝ) f y n : (a : (i : Fin n) → ℝ) → E) fun (x : Fin n) ↦ 1 : E) =
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y x) : Circle)
      ((-2 * (↑π : ℂ) * I * (↑y : ℂ)) ^ n • f y)
have h : (-(2 * (↑π : ℂ) * I)) ^ n • y ^ n • f y = (-(2 * (↑π : ℂ) * I * (↑y : ℂ))) ^ n • f y
Tactic: suffices (-(2 * π * I)) ^ n • y ^ n • f y = (-(2 * π * I * y)) ^ n • f y by
    simpa [innerSL_apply_apply _]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable _ _ _ _ measurableSpace (iteratedDeriv n f) volume
hn : (↑n : ℕ∞) ≤ N
⊢ 𝓕 (iteratedDeriv n f) = fun (x : ℝ) ↦ (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • 𝓕 f x
have h : ∀ (x : ℝ), 𝓕 (iteratedDeriv n f) x = (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • 𝓕 f x
Tactic: ext x : 1