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
rw : ‖1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₁ : norm (E := ℝ) 1 / ‖2 * HPow.hPow (β := ℕ) ‖w‖ 2‖ * ‖w‖ = 1 / (2 * ‖w‖)
⊢ norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
have rw₂ : norm (E := ℝ) 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
Tactic: rw [norm_smul, norm_div, Real.norm_of_nonneg (mul_nonneg two_pos.le <| sq_nonneg _), norm_one,
      sq, ← div_div, ← div_div, ← div_div, div_mul_cancel₀ _ (norm_eq_zero.not.mpr hw_ne)]
-- 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
rw : ‖1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₁ : norm (E := ℝ) 1 / ‖2 * HPow.hPow (β := ℕ) ‖w‖ 2‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₂ : norm (E := ℝ) 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
⊢ norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
have rw₃ : 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
Tactic: rw [norm_smul, norm_div, Real.norm_of_nonneg (mul_nonneg two_pos.le <| sq_nonneg _), norm_one,
      sq, ← div_div, ← div_div, ← div_div, div_mul_cancel₀ _ (norm_eq_zero.not.mpr hw_ne)]
-- 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
rw : ‖1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₁ : norm (E := ℝ) 1 / ‖2 * HPow.hPow (β := ℕ) ‖w‖ 2‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₂ : norm (E := ℝ) 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
rw₃ : 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
⊢ norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
have rw₄ : 1 / (2 * (‖w‖ * ‖w‖)) * ‖w‖ = 1 / (2 * ‖w‖)
Tactic: rw [norm_smul, norm_div, Real.norm_of_nonneg (mul_nonneg two_pos.le <| sq_nonneg _), norm_one,
      sq, ← div_div, ← div_div, ← div_div, div_mul_cancel₀ _ (norm_eq_zero.not.mpr hw_ne)]
-- 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
rw : ‖1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₁ : norm (E := ℝ) 1 / ‖2 * HPow.hPow (β := ℕ) ‖w‖ 2‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₂ : norm (E := ℝ) 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
rw₃ : 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
rw₄ : 1 / (2 * (‖w‖ * ‖w‖)) * ‖w‖ = 1 / (2 * ‖w‖)
⊢ norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
have rw₅ : 1 / 2 / (‖w‖ * ‖w‖) * ‖w‖ = 1 / (2 * ‖w‖)
Tactic: rw [norm_smul, norm_div, Real.norm_of_nonneg (mul_nonneg two_pos.le <| sq_nonneg _), norm_one,
      sq, ← div_div, ← div_div, ← div_div, div_mul_cancel₀ _ (norm_eq_zero.not.mpr hw_ne)]
-- 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
rw : ‖1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₁ : norm (E := ℝ) 1 / ‖2 * HPow.hPow (β := ℕ) ‖w‖ 2‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₂ : norm (E := ℝ) 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
rw₃ : 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
rw₄ : 1 / (2 * (‖w‖ * ‖w‖)) * ‖w‖ = 1 / (2 * ‖w‖)
rw₅ : 1 / 2 / (‖w‖ * ‖w‖) * ‖w‖ = 1 / (2 * ‖w‖)
⊢ norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
have rw₆ : 1 / 2 / ‖w‖ / ‖w‖ * ‖w‖ = 1 / (2 * ‖w‖)
Tactic: rw [norm_smul, norm_div, Real.norm_of_nonneg (mul_nonneg two_pos.le <| sq_nonneg _), norm_one,
      sq, ← div_div, ← div_div, ← div_div, div_mul_cancel₀ _ (norm_eq_zero.not.mpr hw_ne)]
-- 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
rw : ‖1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₁ : norm (E := ℝ) 1 / ‖2 * HPow.hPow (β := ℕ) ‖w‖ 2‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₂ : norm (E := ℝ) 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
rw₃ : 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
rw₄ : 1 / (2 * (‖w‖ * ‖w‖)) * ‖w‖ = 1 / (2 * ‖w‖)
rw₅ : 1 / 2 / (‖w‖ * ‖w‖) * ‖w‖ = 1 / (2 * ‖w‖)
rw₆ : 1 / 2 / ‖w‖ / ‖w‖ * ‖w‖ = 1 / (2 * ‖w‖)
⊢ norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
have rw₇ : 1 / 2 / ‖w‖ / ‖w‖ * ‖w‖ = 1 / 2 / ‖w‖
Tactic: rw [norm_smul, norm_div, Real.norm_of_nonneg (mul_nonneg two_pos.le <| sq_nonneg _), norm_one,
      sq, ← div_div, ← div_div, ← div_div, div_mul_cancel₀ _ (norm_eq_zero.not.mpr hw_ne)]
-- 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
rw : ‖1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₁ : norm (E := ℝ) 1 / ‖2 * HPow.hPow (β := ℕ) ‖w‖ 2‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₂ : norm (E := ℝ) 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
rw₃ : 1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2) * ‖w‖ = 1 / (2 * ‖w‖)
rw₄ : 1 / (2 * (‖w‖ * ‖w‖)) * ‖w‖ = 1 / (2 * ‖w‖)
rw₅ : 1 / 2 / (‖w‖ * ‖w‖) * ‖w‖ = 1 / (2 * ‖w‖)
rw₆ : 1 / 2 / ‖w‖ / ‖w‖ * ‖w‖ = 1 / (2 * ‖w‖)
rw₇ : 1 / 2 / ‖w‖ / ‖w‖ * ‖w‖ = 1 / 2 / ‖w‖
⊢ norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
have rw₈ : 1 / 2 / ‖w‖ = 1 / 2 / ‖w‖
Tactic: rw [norm_smul, norm_div, Real.norm_of_nonneg (mul_nonneg two_pos.le <| sq_nonneg _), norm_one,
      sq, ← div_div, ← div_div, ← div_div, div_mul_cancel₀ _ (norm_eq_zero.not.mpr hw_ne)]
-- 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
⊢ norm.{u_1} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) <
    ε
have hw'_nm : norm.{u_2} (E := V) (i w) = 1 / (2 * ‖w‖)
Tactic: have hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖) := by
    rw [norm_smul, norm_div, Real.norm_of_nonneg (mul_nonneg two_pos.le <| sq_nonneg _), norm_one,
      sq, ← div_div, ← div_div, ← div_div, div_mul_cancel₀ _ (norm_eq_zero.not.mpr hw_ne)]
-- 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‖)
⊢ norm.{u_1} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) <
    ε
have this : ‖1 / 2‖ = 2⁻¹
Tactic: have : ‖(1 / 2 : ℂ)‖ = 2⁻¹ := by simp
-- 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⁻¹
⊢ norm.{u_1} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) <
    ε
have rw : norm.{u_1} (E := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v - f (v + i w))) <
  2 * ε
Tactic: rw [fourierIntegral_eq_half_sub_half_period_translate hw_ne
      (hf1.integrable_of_hasCompactSupport hf2),
    norm_smul, this, inv_mul_eq_div, div_lt_iff₀' two_pos]
-- 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⁻¹
⊢ norm.{u_1} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v - f (v + i w))) <
    2 * ε
have refine : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
    ‖HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) (f a - f (a + i w))‖) <
  2 * ε
Tactic: refine lt_of_le_of_lt (norm_integral_le_integral_norm _) ?_
-- 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⁻¹
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
      ‖HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) (f a - f (a + i w))‖) <
    2 * ε
have simp_rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
    ‖f a - f (a + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)‖) <
  2 * ε
Tactic: simp_rw [Circle.norm_smul]
-- 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⁻¹
⊢ 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)‖)
have refine : ∀ (v : V) (hv : v ∉ A), ‖f v - f (v + i w)‖ = 0
Tactic: refine (setIntegral_eq_integral_of_forall_compl_eq_zero fun v hv => ?_).symm
-- 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 : V
hv : v ∉ {v : V | ‖v‖ ≤ R + 1}
⊢ ‖f v - f (v + i w)‖ = 0
have hv₁ : R + 1 < ‖v‖
Tactic: simp only [mem_setOf, not_le] at hv
Cleared hypotheses: hv
-- 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‖
⊢ ‖f v - f (v + i w)‖ = 0
have rw : R ≤ ‖v + i w‖
Tactic: rw [hR_bd v _, hR_bd (v + i w) _, sub_zero, norm_zero]
-- 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‖
rw : R ≤ ‖v + i w‖
⊢ ‖f v - f (v + i w)‖ = 0
have rw₁ : R ≤ ‖v‖
Tactic: rw [hR_bd v _, hR_bd (v + i w) _, sub_zero, norm_zero]
-- 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 ≤ ‖v + i w‖
have rw : R ≤ ‖v - -i w‖
Tactic: rw [← sub_neg_eq_add]
-- 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 ≤ ‖v - -i w‖
have refine : R ≤ ‖v‖ - norm.{u_2} (E := V) (-i w)
Tactic: refine le_trans ?_ (norm_sub_norm_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 ≤ ‖v‖ - norm.{u_2} (E := V) (-i w)
have rw : R + norm.{u_2} (E := V) (i w) ≤ ‖v‖
Tactic: rw [le_sub_iff_add_le, norm_neg]