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 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R ≤ ‖v‖

Tactic:
exact (le_add_of_nonneg_right zero_le_one).trans hv.le

Premises used: LT.lt.le, zero_le_one, le_add_of_nonneg_right, LE.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
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 / 2‖ = 2⁻¹
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume 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)‖)

Tactic:
have int_A : ∫ v : V, ‖f v - f (v + i w)‖ = ∫ v in A, ‖f v - f (v + i w)‖ := by
    refine (setIntegral_eq_integral_of_forall_compl_eq_zero fun v hv => ?_).symm
    dsimp only [A] at hv
    simp only [mem_setOf, not_le] at hv
    rw [hR_bd v _, hR_bd (v + i w) _, sub_zero, norm_zero]
    · rw [← sub_neg_eq_add]
      refine le_trans ?_ (norm_sub_norm_le _ _)
      rw [le_sub_iff_add_le, norm_neg]
      refine le_trans ?_ hv.le
      rw [add_le_add_iff_left, hw'_nm, ← div_div]
      refine (div_le_one <| norm_pos_iff.mpr hw_ne).mpr ?_
      refine le_trans (le_add_of_nonneg_right <| one_div_nonneg.mpr <| ?_) hw_bd
      exact (mul_pos (zero_lt_two' ℝ) hδ1).le
    · exact (le_add_of_nonneg_right zero_le_one).trans hv.le
-- 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 / 2‖ = 2⁻¹
int_A :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume 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 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) <
    2 * ε
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
      ‖f a - f (a + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖) <
    2 * ε

Tactic:
rw [int_A]
-- 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 / 2‖ = 2⁻¹
simp_rw : ∀ v ∈ A, ‖f v - f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖ ≤ ε / (↑B : ℝ)
⊢ ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / (↑B : ℝ)

Tactic:
simp_rw [norm_norm]

Premises used: norm_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}
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 / 2‖ = 2⁻¹
⊢ ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / (↑B : ℝ)

Tactic:
simp_rw [dist_eq_norm] at hδ2

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
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
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 / 2‖ = 2⁻¹
hδ2 : ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / (↑B : ℝ)
⊢ ∀ v ∈ A, ‖f v - f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖ ≤ ε / (↑B : ℝ)

Tactic:
fun x _ => (hδ2 ?_).le

Premises used: LT.lt.le
-- 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
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 / 2‖ = 2⁻¹
hδ2 : ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / (↑B : ℝ)
refine : ∀ x ∈ A, ‖x - (x + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖ < δ
⊢ ∀ v ∈ A, ‖f v - f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖ ≤ ε / (↑B : ℝ)

Tactic:
refine fun x _ => (hδ2 ?_).le

Premises used: LT.lt.le
-- 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
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 / 2‖ = 2⁻¹
hδ2 : ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / (↑B : ℝ)
x : V
h : x ∈ A
rw : 1 / (2 * δ) < ‖w‖
⊢ ‖x - (x + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖ < δ

Tactic:
rw [sub_add_cancel_left, norm_neg, hw'_nm, ← div_div, div_lt_iff₀ (norm_pos_iff.mpr hw_ne), ←
      div_lt_iff₀' hδ1, div_div]

Premises used: Iff.mpr, norm_pos_iff, sub_add_cancel_left, div_lt_iff₀, div_lt_iff₀', norm_neg, div_div
-- 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
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 / 2‖ = 2⁻¹
hδ2 : ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / (↑B : ℝ)
x : V
h : x ∈ A
⊢ 1 / (2 * δ) < ‖w‖

Tactic:
(lt_add_of_pos_left _ one_half_pos).trans_le hw_bd

Premises used: LT.lt.trans_le, 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
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 / 2‖ = 2⁻¹
hδ2 : ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / (↑B : ℝ)
x : V
h : x ∈ A
⊢ 1 / (2 * δ) < ‖w‖

Tactic:
exact (lt_add_of_pos_left _ one_half_pos).trans_le hw_bd

Premises used: LT.lt.trans_le, 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 / 2‖ = 2⁻¹
⊢ ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / (↑B : ℝ)

Tactic:
have bdA : ∀ v : V, v ∈ A → ‖‖f v - f (v + i w)‖‖ ≤ ε / B := by
    simp_rw [norm_norm]
    simp_rw [dist_eq_norm] at hδ2
    refine fun x _ => (hδ2 ?_).le
    rw [sub_add_cancel_left, norm_neg, hw'_nm, ← div_div, div_lt_iff₀ (norm_pos_iff.mpr hw_ne), ←
      div_lt_iff₀' hδ1, div_div]
    exact (lt_add_of_pos_left _ one_half_pos).trans_le hw_bd
-- 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 / 2‖ = 2⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / (↑B : ℝ)
⊢ norm (E := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (x : V) ↦ ‖f x - f (x + i w)‖) ≤
    ε / (↑B : ℝ) * Measure.real (m := MeasureSpace.toMeasurableSpace) volume A

Tactic:
have bdA2 := norm_setIntegral_le_of_norm_le_const (hB_vol.trans_lt ENNReal.coe_lt_top) bdA
-- 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 / 2‖ = 2⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / (↑B : ℝ)
bdA2 :
  norm (E := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (x : V) ↦ ‖f x - f (x + i w)‖) ≤
    ε / (↑B : ℝ) * Measure.real (m := MeasureSpace.toMeasurableSpace) volume A
⊢ 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)‖

Tactic:
have : ‖_‖ = ∫ v : V in A, ‖f v - f (v + i w)‖ :=
    Real.norm_of_nonneg (setIntegral_nonneg mA fun x _ => norm_nonneg _)
-- 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 :
  norm (E := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (x : V) ↦ ‖f x - f (x + 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)‖
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) ≤
    ε / (↑B : ℝ) * Measure.real (m := MeasureSpace.toMeasurableSpace) volume A

Tactic:
rw [this] at bdA2
-- 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 :
  norm (E := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (x : V) ↦ ‖f x - f (x + 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)‖
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
⊢ 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)‖

Tactic:
rw [this] at bdA2
-- 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)‖
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) <
    2 * ε

Tactic:
bdA2.trans_lt ?_

Premises used: 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
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 : ℝ) * Measure.real (m := MeasureSpace.toMeasurableSpace) volume A < 2 * ε
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) <
    2 * ε

Tactic:
refine bdA2.trans_lt ?_

Premises used: 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
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 : Measure.real (m := MeasureSpace.toMeasurableSpace) volume A < 2 * (↑B : ℝ)
⊢ ε / (↑B : ℝ) * Measure.real (m := MeasureSpace.toMeasurableSpace) volume A < 2 * ε

Tactic:
rw [div_mul_eq_mul_div, div_lt_iff₀ (NNReal.coe_pos.mpr hB_pos), mul_comm (2 : ℝ), mul_assoc,
    mul_lt_mul_iff_right₀ hε]

Premises used: Iff.mpr, mul_assoc, div_mul_eq_mul_div, div_lt_iff₀, mul_lt_mul_iff_right₀, mul_comm, NNReal.coe_pos, OfNat.ofNat