awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
V : Type u_5
W : Type u_6
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℂ E
M : ι → Type u_7
inst_10 : (i : ι) → NormedAddCommGroup (M i)
inst_11 : (i : ι) → NormedSpace ℝ (M i)
f : V → ContinuousMultilinearMap ℝ M E
m : (i : ι) → M i
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 : (i : ι) → M i) → E)
        m ∂μ)
    (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 : (i : ι) → M i) → E) m) w)
φ_int :
  Integrable (ε := ContinuousMultilinearMap ℝ M 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 : (i : ι) → M i) → E)
        m :
      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 : (i : ι) → M i) → E) m) w :
      E)

Tactic:
rw [fourierIntegral, ContinuousMultilinearMap.integral_apply]

Premises used: VectorFourier.fourierIntegral, ContinuousMultilinearMap.integral_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
V : Type u_5
W : Type u_6
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℂ E
M : ι → Type u_7
inst_10 : (i : ι) → NormedAddCommGroup (M i)
inst_11 : (i : ι) → NormedSpace ℝ (M i)
f : V → ContinuousMultilinearMap ℝ M E
m : (i : ι) → M i
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 : (i : ι) → M i) → E)
        m ∂μ)
    (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 : (i : ι) → M i) → E) m) w)

Tactic:
rfl
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
V : Type u_5
W : Type u_6
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℂ E
M : ι → Type u_7
inst_10 : (i : ι) → NormedAddCommGroup (M i)
inst_11 : (i : ι) → NormedSpace ℝ (M i)
f : V → ContinuousMultilinearMap ℝ M E
m : (i : ι) → M i
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 (ε := ContinuousMultilinearMap ℝ M 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
ι : Type u_2
E : Type u_3
V : Type u_5
W : Type u_6
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℂ E
M : ι → Type u_7
inst_10 : (i : ι) → NormedAddCommGroup (M i)
inst_11 : (i : ι) → NormedSpace ℝ (M i)
f : V → ContinuousMultilinearMap ℝ M E
m : (i : ι) → M i
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
ι : Type u_2
E : Type u_3
V : Type u_5
W : Type u_6
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℂ E
M : ι → Type u_7
inst_10 : (i : ι) → NormedAddCommGroup (M i)
inst_11 : (i : ι) → NormedSpace ℝ (M i)
f : V → ContinuousMultilinearMap ℝ M E
m : (i : ι) → M i
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₂
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : MeasurableSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure 𝕜
f : 𝕜 → E
w : 𝕜
⊢ fourierIntegral e μ f w = ∫ (v : 𝕜), HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(v * w)) : 𝕊) (f v) ∂μ

Tactic:
rfl

Premises used: VectorFourier.fourierIntegral, Fourier.fourierIntegral, rfl
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : MeasurableSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure 𝕜
f : 𝕜 → E
r : ℂ
⊢ fourierIntegral e μ (r • f) = r • fourierIntegral e μ f

Tactic:
VectorFourier.fourierIntegral_const_smul _ _ _ _ _

Premises used: VectorFourier.fourierIntegral_const_smul, Fourier.fourierIntegral
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : MeasurableSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure 𝕜
f : 𝕜 → E
w : 𝕜
⊢ ‖fourierIntegral e μ f w‖ ≤ ∫ (x : 𝕜), ‖f x‖ ∂μ

Tactic:
VectorFourier.norm_fourierIntegral_le_integral_norm _ _ _ _ _

Premises used: Fourier.fourierIntegral, VectorFourier.norm_fourierIntegral_le_integral_norm
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : MeasurableSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℂ E
inst_4 : MeasurableAdd 𝕜
e : AddChar 𝕜 𝕊
μ : Measure 𝕜
inst_5 : μ.IsAddRightInvariant
f : 𝕜 → E
v₀ : 𝕜
⊢ fourierIntegral e μ (f ∘ fun (v : 𝕜) ↦ v + v₀) = fun (w : 𝕜) ↦
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (v₀ * w) : 𝕊) (fourierIntegral e μ f w)

Tactic:
VectorFourier.fourierIntegral_comp_add_right _ _ _ _ _

Premises used: Fourier.fourierIntegral, VectorFourier.fourierIntegral_comp_add_right
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module ℝ V
inst_4 : MeasurableSpace V
W : Type u_5
inst_5 : AddCommGroup W
inst_6 : Module ℝ W
L : LinearMap.{0, 0, u_4, u_5} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
μ : Measure V
f : V → E
w : W
simp_rw :
  Eq.{u_3 + 1} (α := E)
    (∫ (v : V),
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : 𝕊)
        (f v) ∂μ)
    (∫ (v : V),
      Complex.exp
          ((↑(HMul.hMul (β := ℝ) (-2 * π) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) : ℂ) *
            Complex.I) •
        f v ∂μ)
simp_rw₁ :
  Eq.{u_3 + 1} (α := E)
    (∫ (v : V),
      HSMul.hSMul (α := ℂ) (↑((𝐞 : (a : ℝ) → 𝕊) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
        (f v) ∂μ)
    (∫ (v : V),
      Complex.exp
          ((↑(HMul.hMul (β := ℝ) (-2 * π) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) : ℂ) *
            Complex.I) •
        f v ∂μ)
simp_rw₂ :
  Eq.{u_3 + 1} (α := E)
    (∫ (v : V),
      Complex.exp
          ((↑(HMul.hMul (β := ℝ) (2 * π) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) : ℂ) *
            Complex.I) •
        f v ∂μ)
    (∫ (v : V),
      Complex.exp
          ((↑(HMul.hMul (β := ℝ) (-2 * π) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) : ℂ) *
            Complex.I) •
        f v ∂μ)
simp_rw₃ :
  Eq.{u_3 + 1} (α := E)
    (∫ (v : V),
      Complex.exp
          ((↑(-HMul.hMul (β := ℝ) (2 * π) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) : ℂ) *
            Complex.I) •
        f v ∂μ)
    (∫ (v : V),
      Complex.exp
          ((↑(HMul.hMul (β := ℝ) (-2 * π) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) : ℂ) *
            Complex.I) •
        f v ∂μ)
⊢ VectorFourier.fourierIntegral 𝐞 μ L f w =
    ∫ (v : V),
      Complex.exp
          ((↑(HMul.hMul (β := ℝ) (-2 * π) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) : ℂ) *
            Complex.I) •
        f v ∂μ

Tactic:
simp_rw [VectorFourier.fourierIntegral, Circle.smul_def, Real.fourierChar_apply, mul_neg,
    neg_mul]

Premises used: Circle.smul_def, VectorFourier.fourierIntegral, Real.fourierChar_apply, neg_mul, mul_neg
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_4
W : Type u_5
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
f : V → E
L : ContinuousLinearMap.{0, 0, u_4, u_5} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
w : W
⊢ Integrable.{u_3, u_4} (ε := E)
      (fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : 𝕊)
          (f v))
      μ ↔
    Integrable f μ

Tactic:
VectorFourier.fourierIntegral_convergent_iff (E := E) (L := L.toLinearMap₁₂)
    continuous_fourierChar L.continuous₂ _

Premises used: ContinuousLinearMap.continuous₂, VectorFourier.fourierIntegral_convergent_iff, Real.continuous_fourierChar
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_5
V : Type u_6
W : Type u_7
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
μ : Measure V
L : ContinuousLinearMap.{0, 0, u_6, u_7} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℝ F
f : V → F →L[ℝ] E
a : F
w : W
hf : Integrable f μ
⊢ Eq.{u_3 + 1} (α := E) ((VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₁₂ f w : (a : F) → E) a : E)
    (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (x : V) ↦ (f x : (a : F) → E) a) w : E)

Tactic:
VectorFourier.fourierIntegral_continuousLinearMap_apply continuous_fourierChar hf

Premises used: VectorFourier.fourierIntegral_continuousLinearMap_apply, Real.continuous_fourierChar
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ι : Type u_4
V : Type u_6
W : Type u_7
inst_2 : Fintype ι
inst_3 : NormedAddCommGroup V
inst_4 : NormedSpace ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
inst_7 : NormedAddCommGroup W
inst_8 : NormedSpace ℝ W
μ : Measure V
L : ContinuousLinearMap.{0, 0, u_6, u_7} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
M : ι → Type u_8
inst_9 : (i : ι) → NormedAddCommGroup (M i)
inst_10 : (i : ι) → NormedSpace ℝ (M i)
f : V → ContinuousMultilinearMap ℝ M E
m : (i : ι) → M i
w : W
hf : Integrable f μ
⊢ Eq.{u_3 + 1} (α := E) ((VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₁₂ f w : (a : (i : ι) → M i) → E) m : E)
    (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (x : V) ↦ (f x : (a : (i : ι) → M i) → E) m) w : E)

Tactic:
VectorFourier.fourierIntegral_continuousMultilinearMap_apply continuous_fourierChar hf

Premises used: Real.continuous_fourierChar, VectorFourier.fourierIntegral_continuousMultilinearMap_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
μ : Measure V
f : V → E
w : V
⊢ Integrable.{u_3, u_1} (ε := E) (fun (v : V) ↦ HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, w⟫) : 𝕊) (f v)) μ ↔
    Integrable f μ

Tactic:
fourierIntegral_convergent_iff' (innerSL ℝ) w

Premises used: Real, innerSL, Real.fourierIntegral_convergent_iff'
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
w : V
⊢ 𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, w⟫) : 𝕊) (f v)

Tactic:
rfl

Premises used: VectorFourier.fourierIntegral, rfl
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
w : V
simp_rw :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, w⟫) : 𝕊) (f v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(-2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v)
simp_rw₁ :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := ℂ) (↑((𝐞 : (a : ℝ) → 𝕊) (-⟪v, w⟫)) : ℂ) (f v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(-2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v)
simp_rw₂ :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(2 * π * -⟪v, w⟫) : ℂ) * Complex.I) • f v)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(-2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v)
simp_rw₃ :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(-(2 * π * ⟪v, w⟫)) : ℂ) * Complex.I) • f v)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(-2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v)
⊢ 𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(-2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v

Tactic:
simp_rw [fourier_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul]

Premises used: Circle.smul_def, Real.fourier_eq, Real.fourierChar_apply, neg_mul, mul_neg
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f₁ f₂ : V → E
hf : f₁ =ᶠ[ae (F := Measure V) volume] f₂
x : V
h :
  EventuallyEq.{u_1, u_3} (β := E) (ae (F := Measure V) volume)
    (fun (a : V) ↦
      HSMul.hSMul (α := 𝕊)
        ((𝐞 : (a : ℝ) → 𝕊) (-((((innerₗ V : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : (a : V) → V →ₗ[ℝ] ℝ) a : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) x) :
          𝕊)
        (f₁ a))
    fun (a : V) ↦
    HSMul.hSMul (α := 𝕊)
      ((𝐞 : (a : ℝ) → 𝕊) (-((((innerₗ V : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : (a : V) → V →ₗ[ℝ] ℝ) a : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) x) :
        𝕊)
      (f₂ a)
⊢ 𝓕 f₁ x = 𝓕 f₂ x

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f₁ f₂ : V → E
hf : f₁ =ᶠ[ae (F := Measure V) volume] f₂
x : V
h :
  ∀ (a : V) (hf' : f₁ a = f₂ a),
    HSMul.hSMul (α := 𝕊)
        ((𝐞 : (a : ℝ) → 𝕊) (-((((innerₗ V : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : (a : V) → V →ₗ[ℝ] ℝ) a : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) x) :
          𝕊)
        (f₁ a) =
      HSMul.hSMul (α := 𝕊)
        ((𝐞 : (a : ℝ) → 𝕊) (-((((innerₗ V : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : (a : V) → V →ₗ[ℝ] ℝ) a : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) x) :
          𝕊)
        (f₂ a)
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae (F := Measure V) volume)
    (fun (a : V) ↦
      HSMul.hSMul (α := 𝕊)
        ((𝐞 : (a : ℝ) → 𝕊) (-((((innerₗ V : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : (a : V) → V →ₗ[ℝ] ℝ) a : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) x) :
          𝕊)
        (f₁ a))
    fun (a : V) ↦
    HSMul.hSMul (α := 𝕊)
      ((𝐞 : (a : ℝ) → 𝕊) (-((((innerₗ V : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : (a : V) → V →ₗ[ℝ] ℝ) a : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) x) :
        𝕊)
      (f₂ a)

Tactic:
filter_upwards [hf] with _ hf'
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f₁ f₂ : V → E
hf : f₁ =ᶠ[ae (F := Measure V) volume] f₂
x a : V
hf' : f₁ a = f₂ a
h h₁ :
  HSMul.hSMul (α := 𝕊)
      ((𝐞 : (a : ℝ) → 𝕊) (-((((innerₗ V : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : (a : V) → V →ₗ[ℝ] ℝ) a : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) x) :
        𝕊)
      (f₂ a) =
    HSMul.hSMul (α := 𝕊)
      ((𝐞 : (a : ℝ) → 𝕊) (-((((innerₗ V : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : (a : V) → V →ₗ[ℝ] ℝ) a : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) x) :
        𝕊)
      (f₂ a)
⊢ HSMul.hSMul (α := 𝕊)
      ((𝐞 : (a : ℝ) → 𝕊) (-((((innerₗ V : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : (a : V) → V →ₗ[ℝ] ℝ) a : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) x) :
        𝕊)
      (f₁ a) =
    HSMul.hSMul (α := 𝕊)
      ((𝐞 : (a : ℝ) → 𝕊) (-((((innerₗ V : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : (a : V) → V →ₗ[ℝ] ℝ) a : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) x) :
        𝕊)
      (f₂ a)

Tactic:
rw [hf']
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
w : V
⊢ 𝓕⁻ f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) ⟪v, w⟫ : 𝕊) (f v)

Tactic:
simp [FourierTransformInv.fourierInv, VectorFourier.fourierIntegral]

Premises used: VectorFourier.fourierIntegral, FourierTransformInv.fourierInv
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
w : V
simp_rw :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) ⟪v, w⟫ : 𝕊) (f v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v)
simp_rw₁ :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := ℂ) (↑((𝐞 : (a : ℝ) → 𝕊) ⟪v, w⟫) : ℂ) (f v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v)
⊢ 𝓕⁻ f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v

Tactic:
simp_rw [fourierInv_eq, Circle.smul_def, Real.fourierChar_apply]

Premises used: Circle.smul_def, Real.fourierChar_apply, Real.fourierInv_eq