awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
⊢ IsBigO (E := ℝ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
have this : ∀ (x : ℝ),
  ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
    ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
Tactic: have : ∀ x : ℝ,
      ‖(f.comp (ContinuousMap.addRight x)).restrict K‖ ≤ ‖f.restrict (Icc (x - r) (x + r))‖ := by
    intro x
    rw [ContinuousMap.norm_le _ (norm_nonneg _)]
    rintro ⟨y, hy⟩
    refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, ?_⟩)
    · simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]
    · exact ⟨by linarith [(hr hy).1], by linarith [(hr hy).2]⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
⊢ IsBigO (E := ℝ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
have simp_rw : ∀
  (hf :
    (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
      IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)),
  (IsBigO (E := ℝ) (F := ℝ) atBot
      (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦
      |x| ^ (-b)) ∧
    IsBigO (E := ℝ) (F := ℝ) atTop
      (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
Tactic: simp_rw [cocompact_eq_atBot_atTop, isBigO_sup] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ (IsBigO (E := ℝ) (F := ℝ) atBot
      (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦
      |x| ^ (-b)) ∧
    IsBigO (E := ℝ) (F := ℝ) atTop
      (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
have left : IsBigO (E := ℝ) (F := ℝ) atBot (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖)
  fun (x : ℝ) ↦ |x| ^ (-b)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
left :
  IsBigO (E := ℝ) (F := ℝ) atBot
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ (IsBigO (E := ℝ) (F := ℝ) atBot
      (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦
      |x| ^ (-b)) ∧
    IsBigO (E := ℝ) (F := ℝ) atTop
      (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
have right : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖)
  fun (x : ℝ) ↦ |x| ^ (-b)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ IsBigO (E := ℝ) (F := ℝ) atBot
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
have left : ∀ (x : ℝ),
  ‖‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖‖ ≤
    ‖‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖‖
Tactic: refine (isBigO_of_le atBot ?_).trans (isBigO_norm_Icc_restrict_atBot hb hf.1 (-r) r)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ ∀ (x : ℝ),
    ‖‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖‖ ≤
      ‖‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖‖
have left : ∀ (x : ℝ),
  ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
    ‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖
Tactic: simp_rw [norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
have right : ∀ (x : ℝ),
  ‖‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖‖ ≤
    ‖‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖‖
Tactic: refine (isBigO_of_le atTop ?_).trans (isBigO_norm_Icc_restrict_atTop hb hf.2 (-r) r)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ ∀ (x : ℝ),
    ‖‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖‖ ≤
      ‖‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖‖
have right : ∀ (x : ℝ),
  ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
    ‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖
Tactic: simp_rw [norm_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
w : V
hw : w ≠ 0
⊢ ⟪i w, w⟫ = 1 / 2
have h : HPow.hPow (β := ℕ) ‖w‖ 2 ≠ 0
Tactic: rw [inner_smul_left, inner_self_eq_norm_sq_to_K, RCLike.ofReal_real_eq_id, id,
      RCLike.conj_to_real, ← div_div, div_mul_cancel₀]
-- 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
w : V
hw : w ≠ 0
⊢ HPow.hPow (β := ℕ) ‖w‖ 2 ≠ 0
have h : ¬HPow.hPow (β := ℕ) ‖w‖ 2 = 0
Tactic: rwa [Ne, sq_eq_zero_iff, norm_eq_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
w : V
hw : w ≠ 0
h : ¬HPow.hPow (β := ℕ) ‖w‖ 2 = 0
⊢ HPow.hPow (β := ℕ) ‖w‖ 2 ≠ 0
have h₁ : ¬‖w‖ = 0
Tactic: rwa [Ne, sq_eq_zero_iff, norm_eq_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
w : V
hw : w ≠ 0
h : ¬HPow.hPow (β := ℕ) ‖w‖ 2 = 0
h₁ : ¬‖w‖ = 0
⊢ HPow.hPow (β := ℕ) ‖w‖ 2 ≠ 0
have h₂ : ¬w = 0
Tactic: rwa [Ne, sq_eq_zero_iff, norm_eq_zero]
-- 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
w : V
hw : w ≠ 0
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w)))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
have hiw : ⟪i w, w⟫ = 1 / 2
Tactic: have hiw : ⟪i w, w⟫ = 1 / 2 := by
    rw [inner_smul_left, inner_self_eq_norm_sq_to_K, RCLike.ofReal_real_eq_id, id,
      RCLike.conj_to_real, ← div_div, div_mul_cancel₀]
    rwa [Ne, sq_eq_zero_iff, norm_eq_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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
⊢ Eq (α := (v : V) → E)
    (fun (v : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w))) fun (v : V) ↦
    (fun (x : V) ↦ -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x)) (v + i w)
have h : ∀ (v : V),
  HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w)) =
    (fun (x : V) ↦ -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x)) (v + i w)
Tactic: ext1 v
-- 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w)) =
    (fun (x : V) ↦ -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x)) (v + i w)
have h : cexp ((↑(2 * π * -⟪v, w⟫) : ℂ) * I) • f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w) =
  -((cexp ((↑(2 * π * -⟪v, w⟫) : ℂ) * I) * cexp ((↑(2 * π * -(1 / 2)) : ℂ) * I)) •
      f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w))
Tactic: simp_rw [inner_add_left, hiw, Circle.smul_def, Real.fourierChar_apply, neg_add, mul_add,
      ofReal_add, add_mul, exp_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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ cexp ((↑(2 * π * -⟪v, w⟫) : ℂ) * I) • f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w) =
    -((cexp ((↑(2 * π * -⟪v, w⟫) : ℂ) * I) * cexp ((↑(2 * π * -(1 / 2)) : ℂ) * I)) •
        f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w))
have match_scalars : cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * 1 =
  -(cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * cexp (2 * (↑π : ℂ) * -HDiv.hDiv (α := ℂ) 1 2 * I) * 1)
Tactic: match_scalars
-- 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ cexp (-((↑π : ℂ) * I)) = (-1)⁻¹
have rw : (cexp ((↑π : ℂ) * I))⁻¹ = (-1)⁻¹
Tactic: rw [exp_neg, exp_pi_mul_I]
-- 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
rw : (cexp ((↑π : ℂ) * I))⁻¹ = (-1)⁻¹
⊢ cexp (-((↑π : ℂ) * I)) = (-1)⁻¹
have rw₁ : Eq (α := ℂ) (-1)⁻¹ (-1)⁻¹
Tactic: rw [exp_neg, exp_pi_mul_I]
-- 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * 1 =
    -(cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * cexp (2 * (↑π : ℂ) * -HDiv.hDiv (α := ℂ) 1 2 * I) * 1)
have H : cexp (-((↑π : ℂ) * I)) = (-1)⁻¹
Tactic: have H : exp (- (π * I)) = (-1)⁻¹ := by rw [exp_neg, exp_pi_mul_I]
-- 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
H : cexp (-((↑π : ℂ) * I)) = (-1)⁻¹
⊢ cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * 1 =
    -(cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * cexp (2 * (↑π : ℂ) * -HDiv.hDiv (α := ℂ) 1 2 * I) * 1)
have a : cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * 1 + cexp (-2 * (↑π : ℂ) * (↑⟪v, w⟫ : ℂ) * I) * (-1)⁻¹ -
    (-(cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * cexp (2 * (↑π : ℂ) * -HDiv.hDiv (α := ℂ) 1 2 * I) * 1) +
      cexp (-2 * (↑π : ℂ) * (↑⟪v, w⟫ : ℂ) * I) * cexp (-((↑π : ℂ) * I))) =
  0
Tactic: linear_combination (norm := ring_nf) cexp (-2 * π * ⟪v, w⟫ * I) * H
-- 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w)))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
have this : Eq (α := (v : V) → E)
  (fun (v : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w))) fun (v : V) ↦
  (fun (x : V) ↦ -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x)) (v + i w)
Tactic: have :
    (fun v : V => 𝐞 (-⟪v, w⟫) • f (v + i w)) =
      fun v : V => (fun x : V => -(𝐞 (-⟪x, w⟫) • f x)) (v + i w) := by
    ext1 v
    simp_rw [inner_add_left, hiw, Circle.smul_def, Real.fourierChar_apply, neg_add, mul_add,
      ofReal_add, add_mul, exp_add]
    match_scalars
    have H : exp (- (π * I)) = (-1)⁻¹ := by rw [exp_neg, exp_pi_mul_I]
    linear_combination (norm := ring_nf) cexp (-2 * π * ⟪v, w⟫ * I) * 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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
this :
  Eq (α := (v : V) → E)
    (fun (v : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w))) fun (v : V) ↦
    (fun (x : V) ↦ -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x)) (v + i w)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w)))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
have rw : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ inst_3 (volume : Measure V) fun (x : V) ↦
    -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x))
  (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v))
Tactic: rw [this, integral_add_right_eq_self (fun (x : V) ↦ -(𝐞 (-⟪x, w⟫) • f x))
        ((fun w ↦ (1 / (2 * ‖w‖ ^ (2 : ℕ))) • w) 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
w : V
hw : w ≠ 0
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) =
    HSMul.hSMul (β := E) (1 / 2)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v - f (v + i w)))
have simp_rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) =
  HSMul.hSMul (β := E) (1 / 2)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v) -
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle)
          (f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)))
Tactic: simp_rw [smul_sub]
-- 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
w : V
hw : w ≠ 0
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) =
    HSMul.hSMul (β := E) (1 / 2)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v) -
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle)
            (f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)))
have rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) =
  HSMul.hSMul (β := E) (1 / 2 * 2)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) (f a))
Tactic: rw [integral_sub, fourierIntegral_half_period_translate hw, sub_eq_add_neg, neg_neg, ←
    two_smul ℂ _, ← @smul_assoc _ _ _ _ _ _ (IsScalarTower.left ℂ), smul_eq_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
w : V
hw : w ≠ 0
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) =
    HSMul.hSMul (β := E) (1 / 2 * 2)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪a, w⟫) : Circle) (f a))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) =
    HSMul.hSMul (β := E) (1 / 2)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v) -
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle)
            (f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w)))
have hf₁ : @Integrable.{u_1, u_2} E _ _ _ MeasureSpace.toMeasurableSpace
  (fun (v : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) volume
Tactic: rw [integral_sub, fourierIntegral_half_period_translate hw, sub_eq_add_neg, neg_neg, ←
    two_smul ℂ _, ← @smul_assoc _ _ _ _ _ _ (IsScalarTower.left ℂ), smul_eq_mul]