awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
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 + norm.{u_2} (E := V) (i w) ≤ ‖v‖
have refine : R + norm.{u_2} (E := V) (i w) ≤ R + 1
Tactic: refine le_trans ?_ hv.le
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
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 + norm.{u_2} (E := V) (i w) ≤ R + 1
have rw : 1 / 2 / ‖w‖ ≤ 1
Tactic: rw [add_le_add_iff_left, hw'_nm, ← div_div]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
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‖
⊢ 1 / 2 / ‖w‖ ≤ 1
have refine : 1 / 2 ≤ ‖w‖
Tactic: refine (div_le_one <| norm_pos_iff.mpr hw_ne).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
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‖
⊢ 1 / 2 ≤ ‖w‖
have refine : 0 ≤ 2 * δ
Tactic: refine le_trans (le_add_of_nonneg_right <| one_div_nonneg.mpr <| ?_) hw_bd
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (hypothesis)
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⁻¹
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
      ‖f a - f (a + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖) <
    2 * ε
have 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)‖)
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
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
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)‖)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
      ‖f a - f (a + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖) <
    2 * ε
have rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) < 2 * ε
Tactic: rw [int_A]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
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 : ℝ)
have simp_rw : ∀ v ∈ A, ‖f v - f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖ ≤ ε / (↑B : ℝ)
Tactic: simp_rw [norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (hypothesis)
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 + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖ ≤ ε / (↑B : ℝ)
have hδ2₁ : ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / (↑B : ℝ)
Tactic: simp_rw [dist_eq_norm] at hδ2
Cleared hypotheses: hδ2
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
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 : ℝ)
have refine : ∀ x ∈ A, ‖x - (x + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖ < δ
Tactic: refine fun x _ => (hδ2 ?_).le
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
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
⊢ ‖x - (x + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖ < δ
have rw : 1 / (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]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (hypothesis)
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⁻¹
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) <
    2 * ε
have bdA : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (hypothesis)
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 : ℝ)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) <
    2 * ε
have 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
Tactic: have bdA2 := norm_setIntegral_le_of_norm_le_const (hB_vol.trans_lt ENNReal.coe_lt_top) bdA
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (hypothesis)
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
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (v : V) ↦ ‖f v - f (v + i w)‖) <
    2 * ε
have 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)‖
Tactic: have : ‖_‖ = ∫ v : V in A, ‖f v - f (v + i w)‖ :=
    Real.norm_of_nonneg (setIntegral_nonneg mA fun x _ => norm_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (hypothesis)
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)‖) <
    2 * ε
have 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
Tactic: rw [this] at bdA2
Cleared hypotheses: bdA2, this
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
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 * ε
have refine : ε / (↑B : ℝ) * Measure.real (m := MeasureSpace.toMeasurableSpace) volume A < 2 * ε
Tactic: refine bdA2.trans_lt ?_
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
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 : ℝ) * Measure.real (m := MeasureSpace.toMeasurableSpace) volume A < 2 * ε
have rw : Measure.real (m := MeasureSpace.toMeasurableSpace) volume A < 2 * (↑B : ℝ)
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ε]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
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 : ℝ)
have refine : (↑B : ℝ≥0∞).toReal < 2 * (↑B : ℝ)
Tactic: refine (ENNReal.toReal_mono ENNReal.coe_ne_top hB_vol).trans_lt ?_