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
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}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : ((volume : Measure V) : (a : Set V) → ℝ≥0∞) A ≤ (↑B : ℝ≥0∞)
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / (↑B : ℝ)
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
this_1 : ‖1 / 2‖ = 2⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / (↑B : ℝ)
bdA2 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) ≤
    ε / (↑B : ℝ) * Measure.real (m := MeasureSpace.toMeasurableSpace) volume A
this :
  norm (E := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume A < 2 * (↑B : ℝ)

Tactic:
(ENNReal.toReal_mono ENNReal.coe_ne_top hB_vol).trans_lt ?_

Premises used: MeasureTheory.Measure.real, LE.le.trans_lt, ENNReal.toReal_mono, ENNReal.coe_ne_top
-- 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}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : ((volume : Measure V) : (a : Set V) → ℝ≥0∞) A ≤ (↑B : ℝ≥0∞)
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / (↑B : ℝ)
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
this_1 : ‖1 / 2‖ = 2⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / (↑B : ℝ)
bdA2 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) ≤
    ε / (↑B : ℝ) * Measure.real (m := MeasureSpace.toMeasurableSpace) volume A
this :
  norm (E := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖
refine : (↑B : ℝ≥0∞).toReal < 2 * (↑B : ℝ)
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume A < 2 * (↑B : ℝ)

Tactic:
refine (ENNReal.toReal_mono ENNReal.coe_ne_top hB_vol).trans_lt ?_

Premises used: LE.le.trans_lt, ENNReal.toReal_mono, ENNReal.coe_ne_top
-- 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}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : ((volume : Measure V) : (a : Set V) → ℝ≥0∞) A ≤ (↑B : ℝ≥0∞)
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / (↑B : ℝ)
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
this_1 : ‖1 / 2‖ = 2⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / (↑B : ℝ)
bdA2 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) ≤
    ε / (↑B : ℝ) * Measure.real (m := MeasureSpace.toMeasurableSpace) volume A
this :
  norm (E := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖
rw : (↑B : ℝ) < (↑B : ℝ) + (↑B : ℝ)
⊢ (↑B : ℝ≥0∞).toReal < 2 * (↑B : ℝ)

Tactic:
rw [ENNReal.coe_toReal, two_mul]

Premises used: ENNReal.coe_toReal, two_mul
-- 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}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : ((volume : Measure V) : (a : Set V) → ℝ≥0∞) A ≤ (↑B : ℝ≥0∞)
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / (↑B : ℝ)
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
this_1 : ‖1 / 2‖ = 2⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / (↑B : ℝ)
bdA2 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) ≤
    ε / (↑B : ℝ) * Measure.real (m := MeasureSpace.toMeasurableSpace) volume A
this :
  norm (E := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖
⊢ (↑B : ℝ) < (↑B : ℝ) + (↑B : ℝ)

Tactic:
lt_add_of_pos_left _ hB_pos

Premises used: lt_add_of_pos_left
-- 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}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : ((volume : Measure V) : (a : Set V) → ℝ≥0∞) A ≤ (↑B : ℝ≥0∞)
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / (↑B : ℝ)
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
this_1 : ‖1 / 2‖ = 2⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / (↑B : ℝ)
bdA2 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) ≤
    ε / (↑B : ℝ) * Measure.real (m := MeasureSpace.toMeasurableSpace) volume A
this :
  norm (E := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖
⊢ (↑B : ℝ) < (↑B : ℝ) + (↑B : ℝ)

Tactic:
exact lt_add_of_pos_left _ hB_pos

Premises used: lt_add_of_pos_left
-- 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
pos :
  ∀ (hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume),
    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)
neg :
  ∀ (hfi : ¬@Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume),
    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)
⊢ 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:
by_cases hfi : Integrable f

Premises used: MeasureTheory.Integrable
-- 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
⊢ Tendsto.{u_2, u_1} (β := E) (fun (x : V) ↦ 0) (cocompact V) (𝓝 0)

Tactic:
tendsto_const_nhds (x := (0 : E))

Premises used: tendsto_const_nhds
-- 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 :
  ∀ (w : V),
    Eq.{u_1 + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
      0
⊢ 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:
convert! tendsto_const_nhds (x := (0 : E)) with w

Premises used: tendsto_const_nhds
-- 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
w : V
h :
  ¬@Integrable.{u_1, u_2} E _ _ _ MeasureSpace.toMeasurableSpace
      (fun (a : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) (f a)) volume
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
    0

Tactic:
apply integral_undef

Premises used: MeasureTheory.integral_undef
-- 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
w : V
h h₁ h₂ h₃ : ¬@Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ ¬@Integrable.{u_1, u_2} E _ _ _ MeasureSpace.toMeasurableSpace
      (fun (a : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) (f a)) volume

Tactic:
rwa [Real.fourierIntegral_convergent_iff]

Premises used: 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
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ 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:
Metric.tendsto_nhds.mpr fun ε hε => ?_

Premises used: Iff.mpr, Metric.tendsto_nhds
-- 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
pos :
  ∀ (ε : ℝ) (hε : ε > 0),
    ∀ᶠ (x : V) in cocompact V,
      dist.{u_1} (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, x⟫) : Circle) (f v))
          0 <
        ε
⊢ 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 Metric.tendsto_nhds.mpr fun ε hε => ?_

Premises used: Iff.mpr, Metric.tendsto_nhds
-- 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
pos :
  ∀ (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),
    ∀ᶠ (x : V) in cocompact V,
      dist.{u_1} (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, x⟫) : Circle) (f v))
          0 <
        ε
⊢ ∀ᶠ (x : V) in cocompact V,
    dist.{u_1} (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, x⟫) : Circle) (f v))
        0 <
      ε

Tactic:
obtain ⟨g, hg_supp, hfg, hg_cont, -⟩ :=
    hfi.exists_hasCompactSupport_integral_sub_le (div_pos hε two_pos)

Premises used: two_pos, MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le, div_pos
-- 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
⊢ ∀ᶠ (x : V) in cocompact V,
    dist.{u_1} (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, x⟫) : Circle) (f v))
        0 <
      ε

Tactic:
((Metric.tendsto_nhds.mp
            (tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support hg_cont
              hg_supp))
          _ (div_pos hε two_pos)).mp
      (Eventually.of_forall fun w hI => ?_)

Premises used: tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support, Metric.tendsto_nhds, two_pos, Filter.Eventually.of_forall, Filter.Eventually.mp, Iff.mp, div_pos
-- 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
pos :
  ∀ (w : V)
    (hI :
      dist.{u_1} (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
          0 <
        ε / 2),
    dist.{u_1} (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
        0 <
      ε
⊢ ∀ᶠ (x : V) in cocompact V,
    dist.{u_1} (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, x⟫) : Circle) (f v))
        0 <
      ε

Tactic:
refine
    ((Metric.tendsto_nhds.mp
            (tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support hg_cont
              hg_supp))
          _ (div_pos hε two_pos)).mp
      (Eventually.of_forall fun w hI => ?_)

Premises used: tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support, Metric.tendsto_nhds, two_pos, Filter.Eventually.of_forall, Filter.Eventually.mp, Iff.mp, div_pos
-- 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 :
  dist.{u_1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
      0 <
    ε / 2
pos :
  ∀
    (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))
          0‖ <
      ε
⊢ dist.{u_1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
      0 <
    ε

Tactic:
rw [dist_eq_norm] at hI ⊢

Premises used: dist_eq_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
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:
le_trans ?_ hfg

Premises used: le_trans
-- 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
refine :
  ‖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‖
⊢ ‖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:
refine le_trans ?_ hfg

Premises used: le_trans