awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 μ
⊢ 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))
    μ
have 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
Tactic: apply (fourierIntegral_convergent_iff he _ _).2 hf
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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)
    ((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)
have 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)
Tactic: rw [fourierIntegral, ContinuousMultilinearMap.integral_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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)
⊢ 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)
have φ_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))
  μ
Tactic: rw [fourierIntegral, ContinuousMultilinearMap.integral_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 μ
⊢ 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))
    μ
have 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
Tactic: apply (fourierIntegral_convergent_iff he _ _).2 hf
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ 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 ∂μ
have 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 ∂μ)
Tactic: simp_rw [VectorFourier.fourierIntegral, Circle.smul_def, Real.fourierChar_apply, mul_neg,
    neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 ∂μ)
⊢ 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 ∂μ
have 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 ∂μ)
Tactic: simp_rw [VectorFourier.fourierIntegral, Circle.smul_def, Real.fourierChar_apply, mul_neg,
    neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 ∂μ)
⊢ 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 ∂μ
have 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 ∂μ)
Tactic: simp_rw [VectorFourier.fourierIntegral, Circle.smul_def, Real.fourierChar_apply, mul_neg,
    neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 ∂μ)
⊢ 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 ∂μ
have 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 ∂μ)
Tactic: simp_rw [VectorFourier.fourierIntegral, Circle.smul_def, Real.fourierChar_apply, mul_neg,
    neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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) ↦
      Complex.exp ((↑(-2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v
have 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)
Tactic: simp_rw [fourier_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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)
⊢ 𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(-2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v
have 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)
Tactic: simp_rw [fourier_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
have 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)
Tactic: simp_rw [fourier_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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)
⊢ 𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(-2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v
have 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)
Tactic: simp_rw [fourier_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ 𝓕 f₁ x = 𝓕 f₂ x
have 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)
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ 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)
have 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)
Tactic: filter_upwards [hf] with _ hf'
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ 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)
have 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)
Tactic: rw [hf']