awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
x : ℝ
⊢ deriv (𝓕 f) x = 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x) x

Tactic:
(hasDerivAt_fourier hf hf' x).deriv

Premises used: Real.hasDerivAt_fourier, HasDerivAt.deriv
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
x : ℝ
⊢ deriv (𝓕 f) x = 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x) x

Tactic:
exact (hasDerivAt_fourier hf hf' x).deriv

Premises used: Real.hasDerivAt_fourier, HasDerivAt.deriv
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
h : ∀ (x : ℝ), 𝓕 (deriv f) x = (2 * (↑π : ℂ) * I * (↑x : ℂ)) • 𝓕 f x
⊢ 𝓕 (deriv f) = fun (x : ℝ) ↦ (2 * (↑π : ℂ) * I * (↑x : ℂ)) • 𝓕 f x

Tactic:
ext x
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 : ℝ
⊢ @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ fderiv ℝ f x) volume

Tactic:
simpa only [← toSpanSingleton_deriv] using
      (ContinuousLinearMap.smulRightL ℝ ℝ E 1).integrable_comp hf'

Premises used: Real, ContinuousLinearMap.smulRightL, ContinuousLinearMap.integrable_comp, toSpanSingleton_deriv, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 : ℝ
⊢ @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'
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 = (𝓕 (E := (x : ℝ) → ℝ →L[ℝ] E) (fderiv ℝ f) x : (a : ℝ) → E) 1

Tactic:
simp only [fourier_continuousLinearMap_apply I, fderiv_apply_one_eq_deriv]

Premises used: Real.fourier_continuousLinearMap_apply, fderiv_apply_one_eq_deriv
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 = (𝓕 (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]
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
h : (fourierSMulRight (-innerSL ℝ) (𝓕 f) x : (a : ℝ) → E) 1 = (2 * (↑π : ℂ) * Complex.I * (↑x : ℂ)) • 𝓕 f x
⊢ 𝓕 (deriv f) x = (2 * (↑π : ℂ) * Complex.I * (↑x : ℂ)) • 𝓕 f x

Tactic:
rw [this, fourier_fderiv hf h'f I]

Premises used: Real.fourier_fderiv
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
⊢ (fourierSMulRight (-innerSL ℝ) (𝓕 f) x : (a : ℝ) → E) 1 = (2 * (↑π : ℂ) * Complex.I * (↑x : ℂ)) • 𝓕 f x

Tactic:
simp only [fourierSMulRight_apply, ContinuousLinearMap.neg_apply, innerSL_apply_apply, smul_smul,
    RCLike.inner_apply', conj_trivial, mul_one, neg_smul, smul_neg, neg_neg, neg_mul, ← coe_smul]

Premises used: RCLike.inner_apply', neg_smul, innerSL_apply_apply, smul_smul, neg_neg, smul_neg, conj_trivial, VectorFourier.fourierSMulRight_apply, ContinuousLinearMap.neg_apply, Complex.coe_smul, neg_mul, mul_one
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
h : ∀ (x : ℝ), iteratedDeriv n (𝓕 f) x = 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • f x) x
⊢ iteratedDeriv n (𝓕 f) = 𝓕 (E := (x : ℝ) → E) fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • f x

Tactic:
ext x : 1
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 ℝ _ _ _ measurableSpace (fun (a : ℝ) ↦ ‖a ^ n • f a‖) volume

Tactic:
(hf n hn).norm

Premises used: MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
h : ∀ (x : ℝ), ‖x‖ ^ n * ‖f x‖ = ‖x ^ n • f x‖
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ ^ n * ‖f v‖) volume

Tactic:
convert! (hf n hn).norm with x

Premises used: MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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_1 : ℝ
n : ℕ
hn : (↑n : ℕ∞) ≤ N
x : ℝ
⊢ ‖x‖ ^ n * ‖f x‖ = ‖x ^ n • f x‖

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 : ℝ
⊢ ∀ (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]
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
⊢ AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f volume

Tactic:
simpa using (hf 0 zero_le).1

Premises used: zero_le, And.left, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
⊢ AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f volume

Tactic:
have B : AEStronglyMeasurable f := by simpa using (hf 0 zero_le).1
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
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))
⊢ iteratedDeriv n (𝓕 f) x = 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • f x) x

Tactic:
rw [iteratedDeriv, iteratedFDeriv_fourier A B hn,
    fourier_continuousMultilinearMap_apply (integrable_fourierPowSMulRight _ (A n hn) B),
    fourier_eq, fourier_eq]

Premises used: Real.fourier_eq, Real.iteratedFDeriv_fourier, Real.fourier_continuousMultilinearMap_apply, iteratedDeriv, VectorFourier.integrable_fourierPowSMulRight
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
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)
⊢ 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:
congr with y
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 : ℝ
this : (-(2 * (↑π : ℂ) * I)) ^ n • y ^ n • f y = (-(2 * (↑π : ℂ) * I * (↑y : ℂ))) ^ n • f 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:
simpa [innerSL_apply_apply _]

Premises used: innerSL_apply_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 : ℝ
h : (-(2 * (↑π : ℂ) * I)) ^ n • y ^ n • f y = (-(2 * (↑π : ℂ) * I * (↑y : ℂ))) ^ n • f 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:
suffices (-(2 * π * I)) ^ n • y ^ n • f y = (-(2 * π * I * y)) ^ n • f y by
    simpa [innerSL_apply_apply _]
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 : ℝ
⊢ (-(2 * (↑π : ℂ) * I)) ^ n • y ^ n • f y = (-(2 * (↑π : ℂ) * I * (↑y : ℂ))) ^ n • f y

Tactic:
simp only [← neg_mul, ← coe_smul, smul_smul, mul_pow, ofReal_pow, mul_assoc]

Premises used: mul_assoc, smul_smul, Complex.coe_smul, neg_mul, mul_pow, Complex.ofReal_pow
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
h : ∀ (x : ℝ), 𝓕 (iteratedDeriv n f) x = (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • 𝓕 f x
⊢ 𝓕 (iteratedDeriv n f) = fun (x : ℝ) ↦ (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • 𝓕 f x

Tactic:
ext x : 1
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n_1 : ℕ
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable _ _ _ _ measurableSpace (iteratedDeriv n f) volume
hn_1 : (↑n_1 : ℕ∞) ≤ N
x : ℝ
n : ℕ
hn : (↑n : ℕ∞) ≤ N
rw :
  @Integrable (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) E) _ _ _ measurableSpace
    ((⇑(ContinuousMultilinearMap.piFieldEquiv ℝ (Fin n) E) :
        (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ ℝ) E) ∘
      iteratedDeriv n f)
    volume
⊢ @Integrable (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) E) _ _ _ measurableSpace (iteratedFDeriv ℝ n f) volume

Tactic:
rw [iteratedFDeriv_eq_equiv_comp]

Premises used: iteratedFDeriv_eq_equiv_comp
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n_1 : ℕ
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable _ _ _ _ measurableSpace (iteratedDeriv n f) volume
hn_1 : (↑n_1 : ℕ∞) ≤ N
x : ℝ
n : ℕ
hn : (↑n : ℕ∞) ≤ N
⊢ @Integrable (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) E) _ _ _ measurableSpace
    ((⇑(ContinuousMultilinearMap.piFieldEquiv ℝ (Fin n) E) :
        (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ ℝ) E) ∘
      iteratedDeriv n f)
    volume

Tactic:
(LinearIsometryEquiv.integrable_comp_iff _).2 (h'f n hn)

Premises used: Iff.mpr, LinearIsometryEquiv.integrable_comp_iff
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n_1 : ℕ
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable _ _ _ _ measurableSpace (iteratedDeriv n f) volume
hn_1 : (↑n_1 : ℕ∞) ≤ N
x : ℝ
n : ℕ
hn : (↑n : ℕ∞) ≤ N
⊢ @Integrable (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) E) _ _ _ measurableSpace
    ((⇑(ContinuousMultilinearMap.piFieldEquiv ℝ (Fin n) E) :
        (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ ℝ) E) ∘
      iteratedDeriv n f)
    volume

Tactic:
exact (LinearIsometryEquiv.integrable_comp_iff _).2 (h'f n hn)

Premises used: Iff.mpr, LinearIsometryEquiv.integrable_comp_iff
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
x : ℝ
⊢ ∀ (n : ℕ),
    (↑n : ℕ∞) ≤ N →
      @Integrable (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) E) _ _ _ measurableSpace (iteratedFDeriv ℝ n f)
        volume

Tactic:
have A : ∀ (n : ℕ), n ≤ N → Integrable (iteratedFDeriv ℝ n f) := by
    intro n hn
    rw [iteratedFDeriv_eq_equiv_comp]
    exact (LinearIsometryEquiv.integrable_comp_iff _).2 (h'f n hn)
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
x : ℝ
A :
  ∀ (n : ℕ),
    (↑n : ℕ∞) ≤ N →
      @Integrable (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) E) _ _ _ measurableSpace (iteratedFDeriv ℝ n f)
        volume
h : 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ iteratedDeriv n f x) x = (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • 𝓕 f x
⊢ 𝓕 (iteratedDeriv n f) x = (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • 𝓕 f x

Tactic:
change 𝓕 (fun x ↦ iteratedDeriv n f x) x = _

Premises used: FourierTransform.fourier, iteratedDeriv
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
x : ℝ
A :
  ∀ (n : ℕ),
    (↑n : ℕ∞) ≤ N →
      @Integrable (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) E) _ _ _ measurableSpace (iteratedFDeriv ℝ n f)
        volume
h :
  ((fourierPowSMulRight (-innerSL ℝ) (𝓕 f) x n : (a : (i : Fin n) → ℝ) → E) fun (x : Fin n) ↦ 1) =
    (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • 𝓕 f x
⊢ 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ iteratedDeriv n f x) x = (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • 𝓕 f x

Tactic:
simp_rw [iteratedDeriv, ← fourier_continuousMultilinearMap_apply (A n hn),
    fourier_iteratedFDeriv hf A hn]

Premises used: Real.fourier_iteratedFDeriv, Real.fourier_continuousMultilinearMap_apply, iteratedDeriv
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
x : ℝ
A :
  ∀ (n : ℕ),
    (↑n : ℕ∞) ≤ N →
      @Integrable (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) E) _ _ _ measurableSpace (iteratedFDeriv ℝ n f)
        volume
⊢ ((fourierPowSMulRight (-innerSL ℝ) (𝓕 f) x n : (a : (i : Fin n) → ℝ) → E) fun (x : Fin n) ↦ 1) =
    (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • 𝓕 f x

Tactic:
simp [← coe_smul, smul_smul, ← mul_pow]

Premises used: smul_smul, Complex.coe_smul, mul_pow
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
apply : ∀ᵐ (a : V), Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a) atTop (𝓝 (f a))
apply₁ :
  ∀ᶠ (n : ℝ) in atTop,
    AEStronglyMeasurable.{u_1, u_2} (β := E) (m₀ := MeasureSpace.toMeasurableSpace)
      (fun (a : V) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a) volume
apply₂ : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : V), ‖cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a‖ ≤ ‖f a‖
⊢ Tendsto.{0, u_2} (β := E)
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v)
    atTop (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ f v))

Tactic:
apply tendsto_integral_filter_of_dominated_convergence _ _ _ hf.norm

Premises used: MeasureTheory.tendsto_integral_filter_of_dominated_convergence, MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h : ∀ (v : V), Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v) atTop (𝓝 (f v))
⊢ ∀ᵐ (a : V), Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a) atTop (𝓝 (f a))

Tactic:
filter_upwards with v
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
⊢ f v = cexp (-(↑0 : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h :
  Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v) atTop
    (𝓝 (cexp (-(↑0 : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v))
⊢ Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v) atTop (𝓝 (f v))

Tactic:
nth_rewrite 2 [show f v = cexp (- (0 : ℝ) * ‖v‖ ^ 2) • f v by simp]