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 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
v : V
w' : W
h : w' ∈ Metric.ball w 1
⊢ Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) ≤ B v

Tactic:
exact norm_fourierSMulRight_le L f v

Premises used: VectorFourier.norm_fourierSMulRight_le
-- 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 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
⊢ ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v

Tactic:
have h4 : (∀ᵐ v ∂μ, ∀ (w' : W), w' ∈ Metric.ball w 1 → ‖F' w' v‖ ≤ B v) := by
    filter_upwards with v w' _
    rw [Circle.norm_smul _ (fourierSMulRight L f v)]
    exact norm_fourierSMulRight_le L f v
-- 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 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
⊢ Integrable B μ

Tactic:
simpa only [← mul_assoc] using hf'.const_mul (2 * π * ‖L‖)

Premises used: Norm.norm, Real.pi, HMul.hMul, MeasureTheory.Integrable.const_mul, mul_assoc, OfNat.ofNat
-- 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 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
⊢ Integrable B μ

Tactic:
have h5 : Integrable B μ := by simpa only [← mul_assoc] using hf'.const_mul (2 * π * ‖L‖)
-- 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 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
h5 : Integrable B μ
⊢ ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, HasFDerivAt (fun (x : W) ↦ F x v) (F' w' v) w'

Tactic:
have h6 : ∀ᵐ v ∂μ, ∀ w', w' ∈ Metric.ball w 1 → HasFDerivAt (fun x ↦ F x v) (F' w' v) w' :=
    ae_of_all _ (fun v w' _ ↦ hasFDerivAt_fourierChar_smul L f v w')
-- 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 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
h5 : Integrable B μ
h6 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, HasFDerivAt (fun (x : W) ↦ F x v) (F' w' v) w'
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w) w

Tactic:
hasFDerivAt_integral_of_dominated_of_fderiv_le (Metric.ball_mem_nhds _ one_pos) h1 (h0 w)
    h3 h4 h5 h6

Premises used: VectorFourier.fourierIntegral, Metric.ball_mem_nhds, hasFDerivAt_integral_of_dominated_of_fderiv_le, one_pos
-- 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 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
h5 : Integrable B μ
h6 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, HasFDerivAt (fun (x : W) ↦ F x v) (F' w' v) w'
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w) w

Tactic:
exact hasFDerivAt_integral_of_dominated_of_fderiv_le (Metric.ball_mem_nhds _ one_pos) h1 (h0 w)
    h3 h4 h5 h6

Premises used: Metric.ball_mem_nhds, hasFDerivAt_integral_of_dominated_of_fderiv_le, one_pos
-- 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 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
h :
  ∀ (w : W),
    Eq (α := W →L[ℝ] E) (fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w)
⊢ Eq (α := (x : W) → W →L[ℝ] E) (fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f))
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f))

Tactic:
ext w : 1
-- 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 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
⊢ Eq (α := W →L[ℝ] E) (fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w)
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w)

Tactic:
(hasFDerivAt_fourierIntegral L hf hf' w).fderiv

Premises used: VectorFourier.hasFDerivAt_fourierIntegral, HasFDerivAt.fderiv
-- 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 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
⊢ Eq (α := W →L[ℝ] E) (fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w)
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w)

Tactic:
exact (hasFDerivAt_fourierIntegral L hf hf' w).fderiv

Premises used: VectorFourier.hasFDerivAt_fourierIntegral, HasFDerivAt.fderiv
-- 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 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
⊢ Differentiable ℝ (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)

Tactic:
fun w ↦ (hasFDerivAt_fourierIntegral L hf hf' w).differentiableAt

Premises used: Differentiable, VectorFourier.hasFDerivAt_fourierIntegral, HasFDerivAt.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) μ
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)
⊢ Eq (α := (w : W) → V →L[ℝ] E) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fderiv ℝ f))
    (fourierSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f))

Tactic:
ext w y
-- 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)) : ℂ)
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 ∂μ)
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)
⊢ 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:
rw [fourierIntegral_continuousLinearMap_apply' hf']

Premises used: Real.fourierIntegral_continuousLinearMap_apply'
-- 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)) : ℂ)
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₁₂ (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:
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]

Premises used: neg_smul, ContinuousLinearMap.toLinearMap₁₂_apply, MeasureTheory.integral_smul, ContinuousLinearMap.flip_apply, smul_smul, VectorFourier.fourierIntegral, neg_neg, smul_neg, VectorFourier.fourierSMulRight_apply, ContinuousLinearMap.neg_apply, Complex.coe_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
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)) : ℂ)
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 ∂μ)
⊢ 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:
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]
-- 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)) : ℂ)
⊢ ∀ (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 _ _ _ _
-- 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
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
h₅ : ∀ x ∈ tsupport g, DifferentiableAt ℝ 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 ∂μ)

Tactic:
rw [integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable, ← integral_neg]

Premises used: integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable, MeasureTheory.integral_neg
-- 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
⊢ 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:
simp only [A, neg_mul, neg_smul, neg_neg]

Premises used: neg_smul, neg_neg, 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) ↦
      -(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 _