awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight (↑n : ℝ)) = e
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) ((f : (a : ℝ) → ℂ) x : ℂ))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (β := ℂ) (cexp ((↑(-2 * π * v * (↑m : ℝ)) : ℂ) * I)) ((f : (a : ℝ) → ℂ) v : ℂ))
have e_f : ∀ (x : ℝ),
  HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) ((f : (a : ℝ) → ℂ) x : ℂ) =
    HSMul.hSMul (β := ℂ) (cexp ((↑(-2 * π * x * (↑m : ℝ)) : ℂ) * I)) ((f : (a : ℝ) → ℂ) x : ℂ)
Tactic: congr 1 with x : 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight (↑n : ℝ)) = e
x : ℝ
⊢ HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) ((f : (a : ℝ) → ℂ) x : ℂ) =
    HSMul.hSMul (β := ℂ) (cexp ((↑(-2 * π * x * (↑m : ℝ)) : ℂ) * I)) ((f : (a : ℝ) → ℂ) x : ℂ)
have e_f : HMul.hMul (β := ℂ) (cexp (2 * (↑π : ℂ) * I * (↑(-m) : ℂ) * (↑x : ℂ) / (↑1 : ℂ))) ((f : (a : ℝ) → ℂ) x : ℂ) =
  HMul.hMul (β := ℂ) (cexp ((↑(-2 * π * x * (↑m : ℝ)) : ℂ) * I)) ((f : (a : ℝ) → ℂ) x : ℂ)
Tactic: rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight (↑n : ℝ)) = e
x : ℝ
⊢ HMul.hMul (β := ℂ) (cexp (2 * (↑π : ℂ) * I * (↑(-m) : ℂ) * (↑x : ℂ) / (↑1 : ℂ))) ((f : (a : ℝ) → ℂ) x : ℂ) =
    HMul.hMul (β := ℂ) (cexp ((↑(-2 * π * x * (↑m : ℝ)) : ℂ) * I)) ((f : (a : ℝ) → ℂ) x : ℂ)
have e_f : 2 * (↑π : ℂ) * I * (↑(-m) : ℂ) * (↑x : ℂ) / (↑1 : ℂ) = (↑(-2 * π * x * (↑m : ℝ)) : ℂ) * I
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight (↑n : ℝ)) = e
x : ℝ
⊢ 2 * (↑π : ℂ) * I * (↑(-m) : ℂ) * (↑x : ℂ) / (↑1 : ℂ) = (↑(-2 * π * x * (↑m : ℝ)) : ℂ) * I
have e_f : 2 * (↑π : ℂ) * I * -(↑m : ℂ) * (↑x : ℂ) / 1 = -2 * (↑π : ℂ) * (↑x : ℂ) * (↑m : ℂ) * I
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight (↑n : ℝ)) = e
⊢ fourierCoeff (T := 1)
      (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯)
      m =
    𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑m : ℝ)
have fourierCoeff : fourierCoeff (T := 1)
    (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) sorry)
    m =
  ∫ (x : ℝ) in 0..1,
    HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
Tactic: calc
    fourierCoeff (Periodic.lift <| f.periodic_tsum_comp_add_zsmul 1) m =
        ∫ x in (0 : ℝ)..1, e x * (∑' n : ℤ, f.comp (ContinuousMap.addRight n)) x := by
      simp_rw [fourierCoeff_eq_intervalIntegral _ m 0, div_one, one_smul, zero_add, e, comp_apply,
        coe_mk, Periodic.lift_coe, zsmul_one, smul_eq_mul]
    -- Transform sum in C(ℝ, ℂ) evaluated at x into pointwise sum of values.
    _ = ∫ x in (0 : ℝ)..1, ∑' n : ℤ, (e * f.comp (ContinuousMap.addRight n)) x := by
      simp_rw [coe_mul, Pi.mul_apply,
        ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]
    -- Swap sum and integral.
    _ = ∑' n : ℤ, ∫ x in (0 : ℝ)..1, (e * f.comp (ContinuousMap.addRight n)) x := by
      refine (intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm ?_).symm
      convert! hf ⟨uIcc 0 1, isCompact_uIcc⟩ using 1
      exact funext fun n => neK _ _
    _ = ∑' n : ℤ, ∫ x in (0 : ℝ)..1, (e * f).comp (ContinuousMap.addRight n) x := by
      simp only [mul_comp] at eadd ⊢
      simp_rw [eadd]
    -- Rearrange sum of interval integrals into an integral over `ℝ`.
    _ = ∫ x, e x * f x := by
      suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq
      apply integrable_of_summable_norm_Icc
      convert! hf ⟨Icc 0 1, isCompact_Icc⟩ using 1
      simp_rw [mul_comp] at eadd ⊢
      simp_rw [eadd]
      exact funext fun n => neK ⟨Icc 0 1, isCompact_Icc⟩ _
    -- Minor tidying to finish
    _ = 𝓕 (f : ℝ → ℂ) m := by
      rw [fourier_real_eq_integral_exp_smul]
      congr 1 with x : 1
      rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
      congr 2
      push_cast
      ring
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight (↑n : ℝ)) = e
fourierCoeff :
  _root_.fourierCoeff (T := 1)
      (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯)
      m =
    ∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
⊢ _root_.fourierCoeff (T := 1)
      (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯)
      m =
    𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑m : ℝ)
have fourierCoeff₁ : Eq (α := ℂ)
  (∫ (x : ℝ) in 0..1,
    HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
  (∫ (x : ℝ) in 0..1, ∑' (n : ℤ), (e * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
Tactic: calc
    fourierCoeff (Periodic.lift <| f.periodic_tsum_comp_add_zsmul 1) m =
        ∫ x in (0 : ℝ)..1, e x * (∑' n : ℤ, f.comp (ContinuousMap.addRight n)) x := by
      simp_rw [fourierCoeff_eq_intervalIntegral _ m 0, div_one, one_smul, zero_add, e, comp_apply,
        coe_mk, Periodic.lift_coe, zsmul_one, smul_eq_mul]
    -- Transform sum in C(ℝ, ℂ) evaluated at x into pointwise sum of values.
    _ = ∫ x in (0 : ℝ)..1, ∑' n : ℤ, (e * f.comp (ContinuousMap.addRight n)) x := by
      simp_rw [coe_mul, Pi.mul_apply,
        ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]
    -- Swap sum and integral.
    _ = ∑' n : ℤ, ∫ x in (0 : ℝ)..1, (e * f.comp (ContinuousMap.addRight n)) x := by
      refine (intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm ?_).symm
      convert! hf ⟨uIcc 0 1, isCompact_uIcc⟩ using 1
      exact funext fun n => neK _ _
    _ = ∑' n : ℤ, ∫ x in (0 : ℝ)..1, (e * f).comp (ContinuousMap.addRight n) x := by
      simp only [mul_comp] at eadd ⊢
      simp_rw [eadd]
    -- Rearrange sum of interval integrals into an integral over `ℝ`.
    _ = ∫ x, e x * f x := by
      suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq
      apply integrable_of_summable_norm_Icc
      convert! hf ⟨Icc 0 1, isCompact_Icc⟩ using 1
      simp_rw [mul_comp] at eadd ⊢
      simp_rw [eadd]
      exact funext fun n => neK ⟨Icc 0 1, isCompact_Icc⟩ _
    -- Minor tidying to finish
    _ = 𝓕 (f : ℝ → ℂ) m := by
      rw [fourier_real_eq_integral_exp_smul]
      congr 1 with x : 1
      rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
      congr 2
      push_cast
      ring
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
h_sum : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)
x : ℝ
F : C(UnitAddCircle, ℂ) :=
  {
    toFun :=
      Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
    continuous_toFun := ⋯ }
⊢ Summable (α := ℂ) (fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ))
have h : ∀ (x : ℤ), fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ) x = 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑x : ℝ)
Tactic: convert! h_sum
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (hypothesis)
Goal:
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
h_sum : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)
x : ℝ
F : C(UnitAddCircle, ℂ) :=
  {
    toFun :=
      Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
    continuous_toFun := ⋯ }
⊢ Eq (α := ℂ) (∑' (n : ℤ), (f : (a : ℝ) → ℂ) (x + (↑n : ℝ)))
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ))
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
have this : Summable (α := ℂ) (fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ))
Tactic: have : Summable (fourierCoeff F) := by
    convert! h_sum
    exact Real.fourierCoeff_tsum_comp_add h_norm _
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
h_sum : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)
x : ℝ
F : C(UnitAddCircle, ℂ) :=
  {
    toFun :=
      Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
    continuous_toFun := ⋯ }
this : Summable (α := ℂ) (fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ))
⊢ Eq (α := ℂ) (∑' (n : ℤ), (f : (a : ℝ) → ℂ) (x + (↑n : ℝ)))
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ))
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
have h : Eq (α := ℂ) (∑' (n : ℤ), (f : (a : ℝ) → ℂ) (x + (↑n : ℝ)) : ℂ)
  ((F : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
Tactic: convert! (has_pointwise_sum_fourier_series_of_summable this x).tsum_eq.symm using 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
h_sum : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)
x : ℝ
F : C(UnitAddCircle, ℂ) :=
  {
    toFun :=
      Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
    continuous_toFun := ⋯ }
this : Summable (α := ℂ) (fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ))
h :
  Eq (α := ℂ) (∑' (n : ℤ), (f : (a : ℝ) → ℂ) (x + (↑n : ℝ)) : ℂ)
    ((F : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
⊢ Eq (α := ℂ) (∑' (n : ℤ), (f : (a : ℝ) → ℂ) (x + (↑n : ℝ)))
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ))
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
have h₁ : Eq (α := ℂ)
  (∑' (n : ℤ),
    HMul.hMul (β := ℂ) (𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ))
      ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
  (∑' (b : ℤ),
    HSMul.hSMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑F : (a : AddCircle 1) → ℂ) b)
      ((fourier b : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
Tactic: convert! (has_pointwise_sum_fourier_series_of_summable this x).tsum_eq.symm using 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
h_sum : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)
x : ℝ
F : C(UnitAddCircle, ℂ) :=
  {
    toFun :=
      Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
    continuous_toFun := ⋯ }
this : Summable (α := ℂ) (fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ))
⊢ Eq (α := ℂ)
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ))
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (∑' (b : ℤ),
      HSMul.hSMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑F : (a : AddCircle 1) → ℂ) b)
        ((fourier b : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
have h : Eq (α := ℂ)
  (∑' (n : ℤ),
    HMul.hMul (β := ℂ)
      (fourierCoeff (T := 1)
        (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ))
          sorry)
        n)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
  (∑' (b : ℤ),
    HSMul.hSMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑F : (a : AddCircle 1) → ℂ) b)
      ((fourier b : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
Tactic: simp_rw [← Real.fourierCoeff_tsum_comp_add h_norm, smul_eq_mul, F, coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
h_sum : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)
x : ℝ
F : C(UnitAddCircle, ℂ) :=
  {
    toFun :=
      Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
    continuous_toFun := ⋯ }
this : Summable (α := ℂ) (fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ))
h :
  Eq (α := ℂ)
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ)
        (fourierCoeff (T := 1)
          (Periodic.lift (f :=
            (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯)
          n)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (∑' (b : ℤ),
      HSMul.hSMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑F : (a : AddCircle 1) → ℂ) b)
        ((fourier b : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
⊢ Eq (α := ℂ)
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ))
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (∑' (b : ℤ),
      HSMul.hSMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑F : (a : AddCircle 1) → ℂ) b)
        ((fourier b : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
have h₁ : Eq (α := ℂ)
  (∑' (n : ℤ),
    HMul.hMul (β := ℂ)
      (fourierCoeff (T := 1)
        (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ))
          sorry)
        n)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
  (∑' (b : ℤ),
    HMul.hMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑F : (a : AddCircle 1) → ℂ) b : ℂ)
      ((fourier b : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
Tactic: simp_rw [← Real.fourierCoeff_tsum_comp_add h_norm, smul_eq_mul, F, coe_mk]
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x : ℝ
hx : max 0 (-2 * R) < x
y : ℝ
hy : x + R ≤ y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
have rw : ∀ (hx : 0 < x ∧ -2 * R < x) (y : ℝ) (hy : x + R ≤ y), y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
Tactic: rw [max_lt_iff] at hx
Cleared hypotheses: hx, y, hy
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
have hx1 : 0 < x
Tactic: obtain ⟨hx1, hx2⟩ := hx
Cleared hypotheses: hx
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
have hx2 : -2 * R < x
Tactic: obtain ⟨hx1, hx2⟩ := hx
Cleared hypotheses: hx
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
have rw : y ^ (-b) ≤ (1 / 2 * x) ^ (-b)
Tactic: rw [← mul_rpow]
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
rw : y ^ (-b) ≤ (1 / 2 * x) ^ (-b)
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
have hx : 0 ≤ 1 / 2
Tactic: rw [← mul_rpow]
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
rw : y ^ (-b) ≤ (1 / 2 * x) ^ (-b)
hx : 0 ≤ 1 / 2
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
have hy₁ : 0 ≤ x
Tactic: rw [← mul_rpow]
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ y ^ (-b) ≤ (1 / 2 * x) ^ (-b)
have hx : 0 < 1 / 2 * x
Tactic: apply rpow_le_rpow_of_nonpos
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
hx : 0 < 1 / 2 * x
⊢ y ^ (-b) ≤ (1 / 2 * x) ^ (-b)
have hxy : 1 / 2 * x ≤ y
Tactic: apply rpow_le_rpow_of_nonpos
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
hx : 0 < 1 / 2 * x
hxy : 1 / 2 * x ≤ y
⊢ y ^ (-b) ≤ (1 / 2 * x) ^ (-b)
have hz : -b ≤ 0
Tactic: apply rpow_le_rpow_of_nonpos
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 < 1 / 2 * x
have linarith : 1 / 2 * x ≤ 0 → 2 / 2 = 1
Tactic: linarith
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
linarith : 1 / 2 * x ≤ 0 → 2 / 2 = 1
⊢ 0 < 1 / 2 * x
have linarith₁ : 1 / 2 * x ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
linarith : 1 / 2 * x ≤ 0 → 2 / 2 = 1
linarith₁ : 1 / 2 * x ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 < 1 / 2 * x
have linarith₂ : 1 / 2 * x ≤ 0 → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
linarith : 1 / 2 * x ≤ 0 → 2 / 2 = 1
linarith₁ : 1 / 2 * x ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 * x ≤ 0 → HMul.hMul (α := ℝ) 2 1 = 2
⊢ 0 < 1 / 2 * x
have linarith₃ : 1 / 2 * x ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
linarith : 1 / 2 * x ≤ 0 → 2 / 2 = 1
linarith₁ : 1 / 2 * x ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 * x ≤ 0 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 1 / 2 * x ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < 1 / 2 * x
have linarith₄ : 1 / 2 * x ≤ 0 → 0 - x + (HMul.hMul (α := ℝ) 1 1 * (1 * x) - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 1 / 2 * x ≤ y
have linarith : y < 1 / 2 * x → 2 / 2 = 1
Tactic: linarith