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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
rw : (cexp ((↑π : ℂ) * I))⁻¹ = (-1)⁻¹
rw₁ rw₂ : Eq (α := ℂ) (-1)⁻¹ (-1)⁻¹
⊢ cexp (-((↑π : ℂ) * I)) = (-1)⁻¹

Tactic:
rw [exp_neg, exp_pi_mul_I]

Premises used: Complex.exp_neg, Complex.exp_pi_mul_I
-- 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ cexp (-((↑π : ℂ) * I)) = (-1)⁻¹

Tactic:
have H : exp (- (π * I)) = (-1)⁻¹ := by rw [exp_neg, exp_pi_mul_I]
-- 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
H : cexp (-((↑π : ℂ) * I)) = (-1)⁻¹
⊢ cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * 1 + cexp (-2 * (↑π : ℂ) * (↑⟪v, w⟫ : ℂ) * I) * (-1)⁻¹ -
      (-(cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * cexp (2 * (↑π : ℂ) * -HDiv.hDiv (α := ℂ) 1 2 * I) * 1) +
        cexp (-2 * (↑π : ℂ) * (↑⟪v, w⟫ : ℂ) * I) * cexp (-((↑π : ℂ) * I))) =
    0

Tactic:
ring_nf
-- 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
H : cexp (-((↑π : ℂ) * I)) = (-1)⁻¹
a :
  cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * 1 + cexp (-2 * (↑π : ℂ) * (↑⟪v, w⟫ : ℂ) * I) * (-1)⁻¹ -
      (-(cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * cexp (2 * (↑π : ℂ) * -HDiv.hDiv (α := ℂ) 1 2 * I) * 1) +
        cexp (-2 * (↑π : ℂ) * (↑⟪v, w⟫ : ℂ) * I) * cexp (-((↑π : ℂ) * I))) =
    0
⊢ cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * 1 =
    -(cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * cexp (2 * (↑π : ℂ) * -HDiv.hDiv (α := ℂ) 1 2 * I) * 1)

Tactic:
linear_combination (norm := ring_nf) cexp (-2 * π * ⟪v, w⟫ * I) * H

Premises used: Real, Real.pi, HMul.hMul, Inner.inner, Complex.ofReal, Complex.exp, OfNat.ofNat, Neg.neg, Complex.I
-- 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
⊢ Eq (α := (v : V) → E)
    (fun (v : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w))) fun (v : V) ↦
    (fun (x : V) ↦ -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x)) (v + i w)

Tactic:
have :
    (fun v : V => 𝐞 (-⟪v, w⟫) • f (v + i w)) =
      fun v : V => (fun x : V => -(𝐞 (-⟪x, w⟫) • f x)) (v + i w) := by
    ext1 v
    simp_rw [inner_add_left, hiw, Circle.smul_def, Real.fourierChar_apply, neg_add, mul_add,
      ofReal_add, add_mul, exp_add]
    match_scalars
    have H : exp (- (π * I)) = (-1)⁻¹ := by rw [exp_neg, exp_pi_mul_I]
    linear_combination (norm := ring_nf) cexp (-2 * π * ⟪v, w⟫ * I) * H
-- 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
this :
  Eq (α := (v : V) → E)
    (fun (v : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w))) fun (v : V) ↦
    (fun (x : V) ↦ -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x)) (v + i w)
rw :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ inst_3 (volume : Measure V) fun (x : V) ↦
      -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w)))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))

Tactic:
rw [this, integral_add_right_eq_self (fun (x : V) ↦ -(𝐞 (-⟪x, w⟫) • f x))
        ((fun w ↦ (1 / (2 * ‖w‖ ^ (2 : ℕ))) • w) w)]

Premises used: Norm.norm, Real, HMul.hMul, MeasureTheory.integral_add_right_eq_self, Inner.inner, Real.fourierChar, HDiv.hDiv, HPow.hPow, HSMul.hSMul, OfNat.ofNat, DFunLike.coe, Neg.neg
-- 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
this :
  Eq (α := (v : V) → E)
    (fun (v : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w))) fun (v : V) ↦
    (fun (x : V) ↦ -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x)) (v + i w)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ inst_3 (volume : Measure V) fun (x : V) ↦
      -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))

Tactic:
simp only [integral_neg]

Premises used: MeasureTheory.integral_neg
-- 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
w : V
hw : w ≠ 0
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) =
    HSMul.hSMul (β := E) (1 / 2)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v) -
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle)
            (f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) =
    HSMul.hSMul (β := E) (1 / 2)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v - f (v + i w)))

Tactic:
simp_rw [smul_sub]

Premises used: smul_sub
-- 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
w : V
hw : w ≠ 0
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) =
    HSMul.hSMul (β := E) (1 / 2 * 2)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) (f a))
hf₁ :
  @Integrable.{u_1, u_2} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) volume
hg :
  @Integrable.{u_1, u_2} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle)
        (f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)))
    volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) =
    HSMul.hSMul (β := E) (1 / 2)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v) -
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle)
            (f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)))

Tactic:
rw [integral_sub, fourierIntegral_half_period_translate hw, sub_eq_add_neg, neg_neg, ←
    two_smul ℂ _, ← @smul_assoc _ _ _ _ _ _ (IsScalarTower.left ℂ), smul_eq_mul]

Premises used: smul_assoc, sub_eq_add_neg, two_smul, neg_neg, MeasureTheory.integral_sub, fourierIntegral_half_period_translate, smul_eq_mul, Complex
-- 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
w : V
hw : w ≠ 0
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) =
    HSMul.hSMul (β := E) (1 / 2 * 2)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) (f a))

Tactic:
simp
-- 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
w : V
hw : w ≠ 0
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ @Integrable.{u_1, u_2} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) volume

Tactic:
(Real.fourierIntegral_convergent_iff w).2 hf

Premises used: Iff.mpr, Real.fourierIntegral_convergent_iff
-- 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
w : V
hw : w ≠ 0
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ @Integrable.{u_1, u_2} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle)
        (f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)))
    volume

Tactic:
(Real.fourierIntegral_convergent_iff w).2 (hf.comp_add_right _)

Premises used: Iff.mpr, Real.fourierIntegral_convergent_iff, MeasureTheory.Integrable.comp_add_right
-- 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
w : V
hw : w ≠ 0
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ @Integrable.{u_1, u_2} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) volume

Tactic:
exacts [(Real.fourierIntegral_convergent_iff w).2 hf,
    (Real.fourierIntegral_convergent_iff w).2 (hf.comp_add_right _)]

Premises used: Iff.mpr, Real.fourierIntegral_convergent_iff, MeasureTheory.Integrable.comp_add_right
-- 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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : V) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
    (cocompact V) (𝓝 0)

Tactic:
NormedAddGroup.tendsto_nhds_zero.mpr fun ε hε => ?_

Premises used: Iff.mpr, NormedAddGroup.tendsto_nhds_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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
refine :
  ∀ (ε : ℝ) (hε : ε > 0),
    ∀ᶠ (x : V) in cocompact V,
      norm.{u_1} (E := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, x⟫) : Circle) (f v)) <
        ε
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : V) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
    (cocompact V) (𝓝 0)

Tactic:
refine NormedAddGroup.tendsto_nhds_zero.mpr fun ε hε => ?_

Premises used: Iff.mpr, NormedAddGroup.tendsto_nhds_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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
this :
  ∃ (T : ℝ),
    ∀ (w : V),
      T ≤ ‖w‖ →
        norm.{u_1} (E := E)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) <
          ε
simp_rw :
  ∃ (a : ℝ),
    ∀ b ≥ a,
      ∀ (a : V),
        ‖a‖ = b →
          norm.{u_1} (E := E)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
                HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, a⟫) : Circle) (f v)) <
            ε
⊢ ∀ᶠ (x : V) in cocompact V,
    norm.{u_1} (E := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, x⟫) : Circle) (f v)) <
      ε

Tactic:
simp_rw [← comap_dist_left_atTop_eq_cocompact (0 : V), eventually_comap, eventually_atTop,
      dist_eq_norm', sub_zero]

Premises used: comap_dist_left_atTop_eq_cocompact, sub_zero, dist_eq_norm', Filter.eventually_comap, Filter.eventually_atTop, OfNat.ofNat
-- 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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
this :
  ∃ (T : ℝ),
    ∀ (w : V),
      T ≤ ‖w‖ →
        norm.{u_1} (E := E)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) <
          ε
⊢ ∃ (a : ℝ),
    ∀ b ≥ a,
      ∀ (a : V),
        ‖a‖ = b →
          norm.{u_1} (E := E)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
                HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, a⟫) : Circle) (f v)) <
            ε

Tactic:
let ⟨T, hT⟩ := this
      ⟨T, fun b hb v hv => hT v (hv.symm ▸ hb)⟩

Premises used: _private.0.tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support.match_2, Exists, Eq.rec, Exists.intro, Eq.symm
-- 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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
this :
  ∃ (T : ℝ),
    ∀ (w : V),
      T ≤ ‖w‖ →
        norm.{u_1} (E := E)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) <
          ε
⊢ ∃ (a : ℝ),
    ∀ b ≥ a,
      ∀ (a : V),
        ‖a‖ = b →
          norm.{u_1} (E := E)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
                HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, a⟫) : Circle) (f v)) <
            ε

Tactic:
exact
      let ⟨T, hT⟩ := this
      ⟨T, fun b hb v hv => hT v (hv.symm ▸ hb)⟩
-- 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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
suffices :
  ∃ (T : ℝ),
    ∀ (w : V),
      T ≤ ‖w‖ →
        norm.{u_1} (E := E)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) <
          ε
⊢ ∀ᶠ (x : V) in cocompact V,
    norm.{u_1} (E := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, x⟫) : Circle) (f v)) <
      ε

Tactic:
suffices ∃ T : ℝ, ∀ w : V, T ≤ ‖w‖ → ‖∫ v : V, 𝐞 (-⟪v, w⟫) • f v‖ < ε by
    simp_rw [← comap_dist_left_atTop_eq_cocompact (0 : V), eventually_comap, eventually_atTop,
      dist_eq_norm', sub_zero]
    exact
      let ⟨T, hT⟩ := this
      ⟨T, fun b hb v hv => hT v (hv.symm ▸ hb)⟩
-- 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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
⊢ ∃ (R : ℝ), 0 < R ∧ ∀ (x : V), R ≤ ‖x‖ → f x = 0

Tactic:
hf2.exists_pos_le_norm

Premises used: HasCompactSupport.exists_pos_le_norm
-- 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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
obtain :
  ∀ (R : ℝ) (hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0),
    ∃ (T : ℝ),
      ∀ (w : V),
        T ≤ ‖w‖ →
          norm.{u_1} (E := E)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
                HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) <
            ε
⊢ ∃ (T : ℝ),
    ∀ (w : V),
      T ≤ ‖w‖ →
        norm.{u_1} (E := E)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) <
          ε

Tactic:
obtain ⟨R, -, hR_bd⟩ : ∃ R : ℝ, 0 < R ∧ ∀ x : V, R ≤ ‖x‖ → f x = 0 := hf2.exists_pos_le_norm

Premises used: HasCompactSupport.exists_pos_le_norm
-- 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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v : V | ‖v‖ ≤ R + 1}
this : A = Metric.closedBall 0 (R + 1)
rw : MeasurableSet.{u_2} (α := V) (Metric.closedBall 0 (R + 1))
⊢ MeasurableSet A

Tactic:
rw [this]
-- 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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v : V | ‖v‖ ≤ R + 1}
this : A = Metric.closedBall 0 (R + 1)
⊢ MeasurableSet.{u_2} (α := V) (Metric.closedBall 0 (R + 1))

Tactic:
Metric.isClosed_closedBall.measurableSet

Premises used: Metric.isClosed_closedBall, IsClosed.measurableSet
-- 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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v : V | ‖v‖ ≤ R + 1}
this : A = Metric.closedBall 0 (R + 1)
⊢ MeasurableSet.{u_2} (α := V) (Metric.closedBall 0 (R + 1))

Tactic:
exact Metric.isClosed_closedBall.measurableSet

Premises used: Metric.isClosed_closedBall, IsClosed.measurableSet
-- 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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v : V | ‖v‖ ≤ R + 1}
suffices : A = Metric.closedBall 0 (R + 1)
⊢ MeasurableSet A

Tactic:
suffices A = Metric.closedBall (0 : V) (R + 1) by
      rw [this]
      exact Metric.isClosed_closedBall.measurableSet