awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖f x - g x‖) ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI :
  ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
        0‖ <
    ε / 2
simp_rw :
  norm.{u_1} (E := E)
      (@integral _ _ _ _ inst_3 (volume : Measure V) fun (a : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) ((f - g) a)) ≤
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖(f - g) x‖
⊢ ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))‖ ≤
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖f x - g x‖

Tactic:
simp_rw [← integral_sub ((Real.fourierIntegral_convergent_iff w).2 hfi)
      ((Real.fourierIntegral_convergent_iff w).2 (hg_cont.integrable_of_hasCompactSupport hg_supp)),
      ← smul_sub, ← Pi.sub_apply]

Premises used: Iff.mpr, Continuous.integrable_of_hasCompactSupport, MeasureTheory.integral_sub, smul_sub, Real.fourierIntegral_convergent_iff, Pi.sub_apply
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖f x - g x‖) ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI :
  ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
        0‖ <
    ε / 2
⊢ norm.{u_1} (E := E)
      (@integral _ _ _ _ inst_3 (volume : Measure V) fun (a : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) ((f - g) a)) ≤
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖(f - g) x‖

Tactic:
VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 _ (innerₗ V) (f - g) w

Premises used: Real.fourierChar, HSub.hSub, VectorFourier.fourierIntegral, VectorFourier.norm_fourierIntegral_le_integral_norm, innerₗ
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖f x - g x‖) ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI :
  ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
        0‖ <
    ε / 2
⊢ norm.{u_1} (E := E)
      (@integral _ _ _ _ inst_3 (volume : Measure V) fun (a : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) ((f - g) a)) ≤
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖(f - g) x‖

Tactic:
exact VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 _ (innerₗ V) (f - g) w

Premises used: Real.fourierChar, HSub.hSub, VectorFourier.norm_fourierIntegral_le_integral_norm, innerₗ
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖f x - g x‖) ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI :
  ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
        0‖ <
    ε / 2
⊢ ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))‖ ≤
    ε / 2

Tactic:
have : ‖(∫ v, 𝐞 (-⟪v, w⟫) • f v) - ∫ v, 𝐞 (-⟪v, w⟫) • g v‖ ≤ ε / 2 := by
    refine le_trans ?_ hfg
    simp_rw [← integral_sub ((Real.fourierIntegral_convergent_iff w).2 hfi)
      ((Real.fourierIntegral_convergent_iff w).2 (hg_cont.integrable_of_hasCompactSupport hg_supp)),
      ← smul_sub, ← Pi.sub_apply]
    exact VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 _ (innerₗ V) (f - g) w
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖f x - g x‖) ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI :
  ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
        0‖ <
    ε / 2
this :
  ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))‖ ≤
    ε / 2
⊢ ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))‖ +
      ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
          0‖ <
    ε / 2 + ε / 2

Tactic:
replace := add_lt_add_of_le_of_lt this hI
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖f x - g x‖) ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI :
  ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
        0‖ <
    ε / 2
this :
  ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))‖ +
      ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
          0‖ <
    ε / 2 + ε / 2
⊢ ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))‖ +
      ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
          0‖ <
    ε

Tactic:
rw [add_halves] at this

Premises used: add_halves
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖f x - g x‖) ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI :
  ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
        0‖ <
    ε / 2
this :
  ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))‖ +
      ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
          0‖ <
    ε
⊢ ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
        0‖ <
    ε

Tactic:
((le_of_eq ?_).trans (norm_add_le _ _)).trans_lt this

Premises used: norm_add_le, LE.le.trans, le_of_eq, LE.le.trans_lt
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖f x - g x‖) ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI :
  ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
        0‖ <
    ε / 2
this :
  ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))‖ +
      ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
          0‖ <
    ε
pos :
  ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
        0‖ =
    ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v)) +
        HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
          0‖
⊢ ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
        0‖ <
    ε

Tactic:
refine ((le_of_eq ?_).trans (norm_add_le _ _)).trans_lt this

Premises used: norm_add_le, LE.le.trans, le_of_eq, LE.le.trans_lt
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖f x - g x‖) ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI :
  ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
        0‖ <
    ε / 2
this :
  ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))‖ +
      ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
          0‖ <
    ε
⊢ ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
        0‖ =
    ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v)) +
        HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
          0‖

Tactic:
simp only [sub_zero, sub_add_cancel]

Premises used: sub_zero, sub_add_cancel
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
simp_rw :
  Tendsto.{0, u_1} (β := E)
    (fun (w : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w * v)) : Circle) (f v))
    (cocompact ℝ) (𝓝 0)
⊢ Tendsto.{0, u_1} (β := E)
    (fun (w : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(v * w)) : Circle) (f v))
    (cocompact ℝ) (𝓝 0)

Tactic:
simp_rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
⊢ Tendsto.{0, u_1} (β := E)
    (fun (w : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w * v)) : Circle) (f v))
    (cocompact ℝ) (𝓝 0)

Tactic:
tendsto_integral_exp_inner_smul_cocompact f

Premises used: tendsto_integral_exp_inner_smul_cocompact
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
⊢ Tendsto.{0, u_1} (β := E)
    (fun (w : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w * v)) : Circle) (f v))
    (cocompact ℝ) (𝓝 0)

Tactic:
exact tendsto_integral_exp_inner_smul_cocompact f

Premises used: tendsto_integral_exp_inner_smul_cocompact
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
⊢ Tendsto (𝓕 f) (cocompact ℝ) (𝓝 0)

Tactic:
tendsto_integral_exp_inner_smul_cocompact f

Premises used: VectorFourier.fourierIntegral, tendsto_integral_exp_inner_smul_cocompact
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
rw :
  Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      ∫ (v : V),
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle)
          (f v) ∂HSMul.hSMul (β := Measure V) (μ.addHaarScalarFactor volume) (volume : Measure V))
    (cocompact (StrongDual ℝ V)) (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      ∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
rw [μ.isAddLeftInvariant_eq_smul volume]

Premises used: MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.isAddLeftInvariant_eq_smul
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
simp_rw :
  Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      HSMul.hSMul (β := E) (μ.addHaarScalarFactor volume)
        (@integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v)))
    (cocompact (StrongDual ℝ V)) (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      ∫ (v : V),
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle)
          (f v) ∂HSMul.hSMul (β := Measure V) (μ.addHaarScalarFactor volume) (volume : Measure V))
    (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
simp_rw [integral_smul_nnreal_measure]

Premises used: MeasureTheory.integral_smul_nnreal_measure
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
rw :
  Tendsto
    (fun (w : StrongDual ℝ V) ↦
      HSMul.hSMul (β := E) (μ.addHaarScalarFactor volume)
        (@integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v)))
    (cocompact (StrongDual ℝ V)) (𝓝 (HSMul.hSMul (β := E) (μ.addHaarScalarFactor volume) 0))
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      HSMul.hSMul (β := E) (μ.addHaarScalarFactor volume)
        (@integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v)))
    (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
rw [← (smul_zero _ : Measure.addHaarScalarFactor μ volume • (0 : E) = 0)]

Premises used: smul_zero
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
hf :
  Tendsto.{u_2, u_1} (β := E)
    (fun (x : StrongDual ℝ V) ↦
      @integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(x : (a : V) → ℝ) v) : Circle) (f v))
    (cocompact (StrongDual ℝ V)) (𝓝 0)
⊢ Tendsto
    (fun (w : StrongDual ℝ V) ↦
      HSMul.hSMul (β := E) (μ.addHaarScalarFactor volume)
        (@integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v)))
    (cocompact (StrongDual ℝ V)) (𝓝 (HSMul.hSMul (β := E) (μ.addHaarScalarFactor volume) 0))

Tactic:
apply Tendsto.const_smul

Premises used: Filter.Tendsto.const_smul