awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
x : V
ξ : W
⊢ Eq.{u_6 + 1} (α := G)
    ((((M.flip : (a : F) → E →L⋆[ℂ] G) (g ξ) : E →L⋆[ℂ] G) : (a : E) → G)
        (HSMul.hSMul (α := 𝕊) (β := ℂ)
            ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊) 1 •
          f x) :
      G)
    ((((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
        (HSMul.hSMul (α := 𝕊) (β := ℂ)
            ((e : (a : 𝕜) → 𝕊) ((((L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) 1 •
          g ξ) :
      G)

Tactic:
simp only [map_smulₛₗ, ContinuousLinearMap.flip_apply, LinearMap.flip_apply, RingHom.id_apply,
      Circle.smul_def, smul_eq_mul, mul_one, ← Circle.coe_inv_eq_conj, AddChar.map_neg_eq_inv,
      inv_inv]

Premises used: RingHom.id_apply, AddChar.map_neg_eq_inv, Circle.smul_def, ContinuousLinearMap.flip_apply, Circle.coe_inv_eq_conj, MulActionSemiHomClass.map_smulₛₗ, LinearMap.flip_apply, inv_inv, smul_eq_mul, mul_one
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
⊢ Eq.{u_6 + 1} (α := G)
    (∫ (x : V),
      ∫ (ξ : W),
        (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
          (HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) ((((L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ)) ∂ν ∂μ)
    (∫ (x : V),
      ∫ (ξ : W),
        (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
          (HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ)) ∂ν ∂μ)

Tactic:
simp only [LinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower, LinearMap.neg_apply,
      neg_neg]

Premises used: ContinuousLinearMap.map_smul_of_tower, LinearMap.neg_apply, neg_neg, LinearMap.flip_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
e_f :
  ∀ (x : V),
    Eq.{u_6 + 1} (α := G)
      (∫ (ξ : W),
          (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
            (HSMul.hSMul (α := 𝕊)
              ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ)) ∂ν :
        G)
      ((((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
          (∫ (ξ : W),
            HSMul.hSMul (α := 𝕊)
              ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ) ∂ν) :
        G)
⊢ Eq.{u_6 + 1} (α := G)
    (∫ (x : V),
      ∫ (ξ : W),
        (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
          (HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ)) ∂ν ∂μ)
    (∫ (x : V),
      (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
        (∫ (ξ : W),
          HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ) ∂ν) ∂μ)

Tactic:
congr with x
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
x : V
e_f :
  Integrable.{u_5, u_3} (ε := F)
    (fun (x_1 : W) ↦
      HSMul.hSMul (α := 𝕊)
        ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) x_1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g x_1))
    ν
⊢ Eq.{u_6 + 1} (α := G)
    (∫ (ξ : W),
        (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
          (HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ)) ∂ν :
      G)
    ((((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
        (∫ (ξ : W),
          HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ) ∂ν) :
      G)

Tactic:
apply ContinuousLinearMap.integral_comp_comm

Premises used: ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
x : V
⊢ Continuous[instTopologicalSpaceProd, inst_12] fun (p : W × V) ↦
    ((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) p.1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) p.2

Tactic:
have hLflip : Continuous fun (p : W × V) => (-L.flip p.1) p.2 :=
      (continuous_neg.comp hL).comp continuous_swap
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
x : V
hLflip :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : W × V) ↦
    ((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) p.1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) p.2
⊢ Integrable.{u_5, u_3} (ε := F)
    (fun (x_1 : W) ↦
      HSMul.hSMul (α := 𝕊)
        ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) x_1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g x_1))
    ν

Tactic:
(fourierIntegral_convergent_iff (L := -L.flip) he hLflip x).2 hg

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
x : V
hLflip :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : W × V) ↦
    ((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) p.1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) p.2
⊢ Integrable.{u_5, u_3} (ε := F)
    (fun (x_1 : W) ↦
      HSMul.hSMul (α := 𝕊)
        ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) x_1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g x_1))
    ν

Tactic:
exact (fourierIntegral_convergent_iff (L := -L.flip) he hLflip x).2 hg

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_7
W : Type u_8
x : MeasurableSpace V
inst_2 : AddCommGroup V
inst_3 : Module ℝ V
inst_4 : AddCommGroup W
inst_5 : Module ℝ W
L : LinearMap.{0, 0, u_7, u_8} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
μ : Measure V
f : V → E
w : W
simp_rw :
  Eq.{u_4 + 1} (α := E)
    (∫ (v : V),
      HSMul.hSMul (α := 𝕊)
        ((Real.probChar : (a : ℝ) → 𝕊) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : 𝕊) (f v) ∂μ)
    (∫ (v : V),
      Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ)
simp_rw₁ :
  Eq.{u_4 + 1} (α := E)
    (∫ (v : V),
      HSMul.hSMul (α := ℂ)
        (↑((Real.probChar : (a : ℝ) → 𝕊) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) (f v) ∂μ)
    (∫ (v : V),
      Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ)
simp_rw₂ :
  Eq.{u_4 + 1} (α := E)
    (∫ (v : V),
      Complex.exp ((↑(-(((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ)
    (∫ (v : V),
      Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ)
⊢ fourierIntegral Real.probChar μ L f w =
    ∫ (v : V), Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ

Tactic:
simp_rw [fourierIntegral, Circle.smul_def, Real.probChar_apply, Complex.ofReal_neg]

Premises used: Complex.ofReal_neg, Circle.smul_def, VectorFourier.fourierIntegral, Real.probChar_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : NormedAddCommGroup W
inst_6 : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedAddCommGroup E
inst_10 : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : 𝕜) → 𝕊)
hf : Integrable f μ
rw :
  Eq.{u_3 + 1} (α := E)
    (∫ (x : V),
      (HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊)
                (-((((ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜)
                                (E := V) (F := W) (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L :
                              V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) :
                            (a : V) → W →ₗ[𝕜] 𝕜)
                          x :
                        W →ₗ[𝕜] 𝕜) :
                      (a : W) → 𝕜)
                    w) :
              𝕊)
            (f x) :
          (a : F) → E)
        a ∂μ)
    (fourierIntegral e μ
      (ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V) (F := W)
        (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L)
      (fun (x : V) ↦ (f x : (a : F) → E) a) w)
φ_int :
  Integrable (ε := F →L[ℝ] E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊)
        ((e : (a : 𝕜) → 𝕊)
            (-((((ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V)
                            (F := W) (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L :
                          V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) :
                        (a : V) → W →ₗ[𝕜] 𝕜)
                      v :
                    W →ₗ[𝕜] 𝕜) :
                  (a : W) → 𝕜)
                w) :
          𝕊)
        (f v))
    μ
⊢ Eq.{u_3 + 1} (α := E)
    ((fourierIntegral e μ
            (ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V)
              (F := W) (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L)
            f w :
          (a : F) → E)
        a :
      E)
    (fourierIntegral e μ
        (ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V) (F := W)
          (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L)
        (fun (x : V) ↦ (f x : (a : F) → E) a) w :
      E)

Tactic:
rw [fourierIntegral, ContinuousLinearMap.integral_apply]

Premises used: ContinuousLinearMap.integral_apply, VectorFourier.fourierIntegral
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : NormedAddCommGroup W
inst_6 : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedAddCommGroup E
inst_10 : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : 𝕜) → 𝕊)
hf : Integrable f μ
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (x : V),
      (HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊)
                (-((((ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜)
                                (E := V) (F := W) (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L :
                              V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) :
                            (a : V) → W →ₗ[𝕜] 𝕜)
                          x :
                        W →ₗ[𝕜] 𝕜) :
                      (a : W) → 𝕜)
                    w) :
              𝕊)
            (f x) :
          (a : F) → E)
        a ∂μ)
    (fourierIntegral e μ
      (ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V) (F := W)
        (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L)
      (fun (x : V) ↦ (f x : (a : F) → E) a) w)

Tactic:
rfl
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : NormedAddCommGroup W
inst_6 : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedAddCommGroup E
inst_10 : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : 𝕜) → 𝕊)
hf : Integrable f μ
apply :
  Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : V × W) ↦
    ((((ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V) (F := W)
                  (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L :
                V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) :
              (a : V) → W →ₗ[𝕜] 𝕜)
            p.1 :
          W →ₗ[𝕜] 𝕜) :
        (a : W) → 𝕜)
      p.2
⊢ Integrable (ε := F →L[ℝ] E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊)
        ((e : (a : 𝕜) → 𝕊)
            (-((((ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V)
                            (F := W) (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L :
                          V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) :
                        (a : V) → W →ₗ[𝕜] 𝕜)
                      v :
                    W →ₗ[𝕜] 𝕜) :
                  (a : W) → 𝕜)
                w) :
          𝕊)
        (f v))
    μ

Tactic:
apply (fourierIntegral_convergent_iff he _ _).2 hf

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : NormedAddCommGroup W
inst_6 : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedAddCommGroup E
inst_10 : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : 𝕜) → 𝕊)
hf : Integrable f μ
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : V × W) ↦
    ((((ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V) (F := W)
                  (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L :
                V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) :
              (a : V) → W →ₗ[𝕜] 𝕜)
            p.1 :
          W →ₗ[𝕜] 𝕜) :
        (a : W) → 𝕜)
      p.2

Tactic:
L.continuous₂

Premises used: ContinuousLinearMap.continuous₂
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : NormedAddCommGroup W
inst_6 : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedAddCommGroup E
inst_10 : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : 𝕜) → 𝕊)
hf : Integrable f μ
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : V × W) ↦
    ((((ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V) (F := W)
                  (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L :
                V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) :
              (a : V) → W →ₗ[𝕜] 𝕜)
            p.1 :
          W →ₗ[𝕜] 𝕜) :
        (a : W) → 𝕜)
      p.2

Tactic:
exact L.continuous₂

Premises used: ContinuousLinearMap.continuous₂