awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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) ↦
      -(2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ)) • g x • f x)
    μ

Tactic:
this
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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)
    μ
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
⊢ Integrable.{u_1, u_2} (ε := E) (fun (x : V) ↦ HSMul.hSMul (α := ℂ) ((fderiv ℝ g x : (a : V) → ℂ) y : ℂ) (f x)) μ

Tactic:
convert! this using 2 with x
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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)
    μ
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:
simp only [A, neg_mul, neg_smul, smul_smul]

Premises used: neg_smul, smul_smul, neg_mul
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E)) μ

Tactic:
(fourierIntegral_convergent_iff' _ _).2 (hf'.apply_continuousLinearMap _)

Premises used: Iff.mpr, Real.fourierIntegral_convergent_iff', MeasureTheory.Integrable.apply_continuousLinearMap
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 (β := E) (g x) ((fderiv ℝ f x : (a : V) → E) y : E)) μ

Tactic:
exact (fourierIntegral_convergent_iff' _ _).2 (hf'.apply_continuousLinearMap _)

Premises used: Iff.mpr, Real.fourierIntegral_convergent_iff', MeasureTheory.Integrable.apply_continuousLinearMap
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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) ↦ g x • f x) μ

Tactic:
(fourierIntegral_convergent_iff' _ _).2 hf

Premises used: Iff.mpr, Real.fourierIntegral_convergent_iff'
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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) ↦ g x • f x) μ

Tactic:
exact (fourierIntegral_convergent_iff' _ _).2 hf

Premises used: Iff.mpr, Real.fourierIntegral_convergent_iff'
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
⊢ ∀ x ∈ tsupport f, DifferentiableAt ℝ g x

Tactic:
fun _ _ ↦ (differentiable_fourierChar_neg_bilinear_left _ _).differentiableAt

Premises used: Differentiable.differentiableAt, Real.differentiable_fourierChar_neg_bilinear_left
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
⊢ ∀ x ∈ tsupport f, DifferentiableAt ℝ g x

Tactic:
exact fun _ _ ↦ (differentiable_fourierChar_neg_bilinear_left _ _).differentiableAt

Premises used: Differentiable.differentiableAt, Real.differentiable_fourierChar_neg_bilinear_left
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
⊢ ∀ x ∈ tsupport g, DifferentiableAt ℝ f x

Tactic:
fun _ _ ↦ h'f.differentiableAt

Premises used: Differentiable.differentiableAt
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
⊢ ∀ x ∈ tsupport g, DifferentiableAt ℝ f x

Tactic:
exact fun _ _ ↦ h'f.differentiableAt

Premises used: Differentiable.differentiableAt
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
v : V
n : ℕ
m : Fin n → W
⊢ (fourierPowSMulRight L f v n : (a : (i : Fin n) → W) → E) m =
    (-(2 * (↑π : ℂ) * I)) ^ n •
      HSMul.hSMul (α := ℝ) (∏ i : Fin n, (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) (m i)) (f v)

Tactic:
simp [fourierPowSMulRight]

Premises used: VectorFourier.fourierPowSMulRight
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
v : V
n : ℕ
⊢ fourierPowSMulRight L f v n =
    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:
rfl

Premises used: Multiset.foldr, VectorFourier.fourierPowSMulRight, Multiset.prod, Finset.prod, rfl
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 : ℕ
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)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (v : V) ↦
    VectorFourier.fourierPowSMulRight L f v n

Tactic:
simp_rw [fourierPowSMulRight_eq_comp]

Premises used: VectorFourier.fourierPowSMulRight_eq_comp
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 : ℕ
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)
⊢ 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:
apply Continuous.const_smul

Premises used: Continuous.const_smul
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 : ℕ
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
⊢ 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 (smulRightL ℝ (fun (_ : Fin n) ↦ W) E).continuous₂.comp₂ _ hf

Premises used: ContinuousLinearMap.continuous₂, Real, Continuous.comp₂, ContinuousMultilinearMap.smulRightL
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 (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:
Continuous.comp (map_continuous _) (continuous_pi (fun _ ↦ L.continuous))

Premises used: Continuous.comp, continuous_pi, ContinuousLinearMap.continuous, ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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 (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:
exact Continuous.comp (map_continuous _) (continuous_pi (fun _ ↦ L.continuous))

Premises used: Continuous.comp, continuous_pi, ContinuousLinearMap.continuous, ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
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
k : ℕ∞ω
hf : ContDiff ℝ k f
n : ℕ
simp_rw :
  ContDiff ℝ (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) k 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)
⊢ ContDiff ℝ (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) k fun (v : V) ↦
    VectorFourier.fourierPowSMulRight L f v n

Tactic:
simp_rw [fourierPowSMulRight_eq_comp]

Premises used: VectorFourier.fourierPowSMulRight_eq_comp