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 : ‖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 : ℝ≥0∞).toReal < 2 * (↑B : ℝ)
have rw : (↑B : ℝ) < (↑B : ℝ) + (↑B : ℝ)
Tactic: rw [ENNReal.coe_toReal, two_mul]
-- 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
⊢ 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)
have 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)
Tactic: by_cases hfi : Integrable f
-- 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
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)
⊢ 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)
have 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)
Tactic: by_cases hfi : Integrable f
-- 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
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)
have 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
Tactic: convert! tendsto_const_nhds (x := (0 : E)) with w
-- 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
hfi : ¬@Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
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
have h : ¬@Integrable.{u_1, u_2} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (a : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) (f a)) volume
Tactic: apply integral_undef
-- 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
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)
have 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 <
      ε
Tactic: refine Metric.tendsto_nhds.mpr fun ε 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
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
ε : ℝ
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 <
      ε
have 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 <
      ε
Tactic: obtain ⟨g, hg_supp, hfg, hg_cont, -⟩ :=
    hfi.exists_hasCompactSupport_integral_sub_le (div_pos hε 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
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 <
      ε
have 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 <
    ε
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 => ?_)
-- 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
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
⊢ dist.{u_1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
      0 <
    ε
have 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‖ <
    ε
Tactic: rw [dist_eq_norm] at hI ⊢
Cleared hypotheses: hI
-- 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
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
have 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‖
Tactic: refine le_trans ?_ hfg
-- 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
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))‖ ≤
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖f x - g x‖
have simp_rw : norm.{u_1} (E := E)
    (@integral _ _ _ _ inst_3 (volume : Measure V) fun (a : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) ((f - g) a)) ≤
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ ‖(f - g) x‖
Tactic: simp_rw [← integral_sub ((Real.fourierIntegral_convergent_iff w).2 hfi)
      ((Real.fourierIntegral_convergent_iff w).2 (hg_cont.integrable_of_hasCompactSupport hg_supp)),
      ← smul_sub, ← Pi.sub_apply]
-- 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
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))
        0‖ <
    ε
have this : ‖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: have : ‖(∫ v, 𝐞 (-⟪v, w⟫) • f v) - ∫ v, 𝐞 (-⟪v, w⟫) • g v‖ ≤ ε / 2 := by
    refine le_trans ?_ hfg
    simp_rw [← integral_sub ((Real.fourierIntegral_convergent_iff w).2 hfi)
      ((Real.fourierIntegral_convergent_iff w).2 (hg_cont.integrable_of_hasCompactSupport hg_supp)),
      ← smul_sub, ← Pi.sub_apply]
    exact VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 _ (innerₗ V) (f - g) w
-- 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
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
this :
  ‖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
⊢ ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
        0‖ <
    ε
have this₁ : ‖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))‖ +
    ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
        0‖ <
  ε / 2 + ε / 2
Tactic: replace := add_lt_add_of_le_of_lt this hI
Cleared hypotheses: this
-- 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
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
this :
  ‖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))‖ +
      ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
          0‖ <
    ε / 2 + ε / 2
⊢ ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
        0‖ <
    ε
have this₁ : ‖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))‖ +
    ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
        0‖ <
  ε
Tactic: rw [add_halves] at this
Cleared hypotheses: 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
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
this :
  ‖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))‖ +
      ‖HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
          0‖ <
    ε
⊢ ‖HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
        0‖ <
    ε
have pos : ‖HSub.hSub (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
      0‖ =
  ‖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)) +
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (g v))
        0‖
Tactic: refine ((le_of_eq ?_).trans (norm_add_le _ _)).trans_lt this
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
⊢ Tendsto.{0, u_1} (β := E)
    (fun (w : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(v * w)) : Circle) (f v))
    (cocompact ℝ) (𝓝 0)
have simp_rw : Tendsto.{0, u_1} (β := E)
  (fun (w : ℝ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w * v)) : Circle) (f v))
  (cocompact ℝ) (𝓝 0)
Tactic: simp_rw [mul_comm]