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 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
⊢ Eq (α := (x : W) → W →L[ℝ] E) (fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f))
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f))
have h : ∀ (w : W),
  Eq (α := W →L[ℝ] E) (fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w)
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w)
Tactic: ext w : 1
-- 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
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (ε := V →L[ℝ] E) (fderiv ℝ f) μ
⊢ Eq (α := (w : W) → V →L[ℝ] E) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fderiv ℝ f))
    (fourierSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f))
have h : ∀ (w : W) (y : V),
  Eq.{u_1 + 1} (α := E) ((fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fderiv ℝ f) w : (a : V) → E) y : E)
    ((fourierSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w : (a : V) → E) y : E)
Tactic: ext w y
-- 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
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (ε := V →L[ℝ] E) (fderiv ℝ f) μ
w : W
y : V
g : (v : V) → ℂ :=
  fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
this :
  Eq.{u_1 + 1} (α := E) (∫ (x : V), HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
⊢ Eq.{u_1 + 1} (α := E) ((fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fderiv ℝ f) w : (a : V) → E) y : E)
    ((fourierSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w : (a : V) → E) y : E)
have rw : Eq.{u_1 + 1} (α := E) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (x : V) ↦ (fderiv ℝ f x : (a : V) → E) y) w : E)
  ((fourierSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w : (a : V) → E) y : E)
Tactic: rw [fourierIntegral_continuousLinearMap_apply' 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (ε := V →L[ℝ] E) (fderiv ℝ f) μ
w : W
y : V
g : (v : V) → ℂ :=
  fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
⊢ Eq.{u_1 + 1} (α := E) ((fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fderiv ℝ f) w : (a : V) → E) y : E)
    ((fourierSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w : (a : V) → E) y : E)
have h : Eq.{u_1 + 1} (α := E) (∫ (x : V), HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E) ∂μ)
  (∫ (x : V), (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
Tactic: suffices ∫ x, g x • fderiv ℝ f x y ∂μ = ∫ x, (2 * ↑π * I * L y w * g x) • f x ∂μ by
    rw [fourierIntegral_continuousLinearMap_apply' hf']
    simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply, fourierSMulRight_apply,
      ContinuousLinearMap.neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
      smul_neg, ← smul_smul, coe_smul, neg_neg]
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (ε := V →L[ℝ] E) (fderiv ℝ f) μ
w : W
y : V
g : (v : V) → ℂ :=
  fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : V), HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
have A : ∀ (x : V),
  (fderiv ℝ g x : (a : V) → ℂ) y =
    -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x
Tactic: have A x : fderiv ℝ g x y = - 2 * ↑π * I * L y w * g x :=
    fderiv_fourierChar_neg_bilinear_left_apply _ _ _ _
-- 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
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (ε := V →L[ℝ] E) (fderiv ℝ f) μ
w : W
y : V
g : (v : V) → ℂ :=
  fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
A :
  ∀ (x : V),
    (fderiv ℝ g x : (a : V) → ℂ) y =
      -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : V), HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
have h : Eq.{u_1 + 1} (α := E) (∫ (a : V), -HSMul.hSMul (α := ℂ) ((fderiv ℝ g a : (a : V) → ℂ) y : ℂ) (f a) ∂μ)
  (∫ (x : V), (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
Tactic: rw [integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable, ← integral_neg]
-- 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
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (ε := V →L[ℝ] E) (fderiv ℝ f) μ
w : W
y : V
g : (v : V) → ℂ :=
  fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
A :
  ∀ (x : V),
    (fderiv ℝ g x : (a : V) → ℂ) y =
      -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x
h :
  Eq.{u_1 + 1} (α := E) (∫ (a : V), -HSMul.hSMul (α := ℂ) ((fderiv ℝ g a : (a : V) → ℂ) y : ℂ) (f a) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : V), HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
have h₁ : Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ HSMul.hSMul (α := ℂ) ((fderiv ℝ g x : (a : V) → ℂ) y : ℂ) (f x)) μ
Tactic: rw [integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable, ← integral_neg]
-- 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
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (ε := V →L[ℝ] E) (fderiv ℝ f) μ
w : W
y : V
g : (v : V) → ℂ :=
  fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
A :
  ∀ (x : V),
    (fderiv ℝ g x : (a : V) → ℂ) y =
      -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x
h :
  Eq.{u_1 + 1} (α := E) (∫ (a : V), -HSMul.hSMul (α := ℂ) ((fderiv ℝ g a : (a : V) → ℂ) y : ℂ) (f a) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
h₁ : Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ HSMul.hSMul (α := ℂ) ((fderiv ℝ g x : (a : V) → ℂ) y : ℂ) (f x)) μ
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : V), HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
have h₂ : Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E)) μ
Tactic: rw [integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable, ← integral_neg]
-- 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
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (ε := V →L[ℝ] E) (fderiv ℝ f) μ
w : W
y : V
g : (v : V) → ℂ :=
  fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
A :
  ∀ (x : V),
    (fderiv ℝ g x : (a : V) → ℂ) y =
      -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x
h :
  Eq.{u_1 + 1} (α := E) (∫ (a : V), -HSMul.hSMul (α := ℂ) ((fderiv ℝ g a : (a : V) → ℂ) y : ℂ) (f a) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
h₁ : Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ HSMul.hSMul (α := ℂ) ((fderiv ℝ g x : (a : V) → ℂ) y : ℂ) (f x)) μ
h₂ : Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E)) μ
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : V), HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
have h₃ : Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ g x • f x) μ
Tactic: rw [integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable, ← integral_neg]
-- 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
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (ε := V →L[ℝ] E) (fderiv ℝ f) μ
w : W
y : V
g : (v : V) → ℂ :=
  fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
A :
  ∀ (x : V),
    (fderiv ℝ g x : (a : V) → ℂ) y =
      -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x
h :
  Eq.{u_1 + 1} (α := E) (∫ (a : V), -HSMul.hSMul (α := ℂ) ((fderiv ℝ g a : (a : V) → ℂ) y : ℂ) (f a) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
h₁ : Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ HSMul.hSMul (α := ℂ) ((fderiv ℝ g x : (a : V) → ℂ) y : ℂ) (f x)) μ
h₂ : Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E)) μ
h₃ : Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ g x • f x) μ
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : V), HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
have h₄ : ∀ x ∈ tsupport f, DifferentiableAt ℝ g x
Tactic: rw [integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable, ← integral_neg]
-- 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
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (ε := V →L[ℝ] E) (fderiv ℝ f) μ
w : W
y : V
g : (v : V) → ℂ :=
  fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
A :
  ∀ (x : V),
    (fderiv ℝ g x : (a : V) → ℂ) y =
      -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x
h :
  Eq.{u_1 + 1} (α := E) (∫ (a : V), -HSMul.hSMul (α := ℂ) ((fderiv ℝ g a : (a : V) → ℂ) y : ℂ) (f a) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
h₁ : Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ HSMul.hSMul (α := ℂ) ((fderiv ℝ g x : (a : V) → ℂ) y : ℂ) (f x)) μ
h₂ : Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E)) μ
h₃ : Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ g x • f x) μ
h₄ : ∀ x ∈ tsupport f, DifferentiableAt ℝ g x
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : V), HSMul.hSMul (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E) ∂μ)
    (∫ (x : V),
      (2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x) • f x ∂μ)
have h₅ : ∀ x ∈ tsupport g, DifferentiableAt ℝ f x
Tactic: rw [integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable, ← integral_neg]
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (ε := V →L[ℝ] E) (fderiv ℝ f) μ
w : W
y : V
g : (v : V) → ℂ :=
  fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
A :
  ∀ (x : V),
    (fderiv ℝ g x : (a : V) → ℂ) y =
      -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x
⊢ Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ HSMul.hSMul (α := ℂ) ((fderiv ℝ g x : (a : V) → ℂ) y : ℂ) (f x)) μ
have this : Integrable.{u_1, u_2} (ε := E)
  (fun (x : V) ↦ -(2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ)) • g x • f x)
  μ
Tactic: have : Integrable (fun x ↦ (-(2 * ↑π * I * ↑((L y) w)) • ((g x : ℂ) • f x))) μ :=
      ((fourierIntegral_convergent_iff' _ _).2 hf).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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (ε := V →L[ℝ] E) (fderiv ℝ f) μ
w : W
y : V
g : (v : V) → ℂ :=
  fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
A :
  ∀ (x : V),
    (fderiv ℝ g x : (a : V) → ℂ) y =
      -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * g x
this :
  Integrable.{u_1, u_2} (ε := E)
    (fun (x : V) ↦
      -(2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ)) • g x • f x)
    μ
⊢ Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ HSMul.hSMul (α := ℂ) ((fderiv ℝ g x : (a : V) → ℂ) y : ℂ) (f x)) μ
have h : ∀ (x : V),
  HSMul.hSMul (α := ℂ) ((fderiv ℝ g x : (a : V) → ℂ) y : ℂ) (f x) =
    -(2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ)) • g x • f x
Tactic: convert! this using 2 with x
-- 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
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
n : ℕ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (v : V) ↦
    VectorFourier.fourierPowSMulRight L f v n
have simp_rw : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] 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)
Tactic: simp_rw [fourierPowSMulRight_eq_comp]
-- 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
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
n : ℕ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] 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 hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] 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 Continuous.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
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
n : ℕ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] 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 : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (w : 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 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) w
Tactic: apply (smulRightL ℝ (fun (_ : Fin n) ↦ W) E).continuous₂.comp₂ _ hf