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
simp_rw :
  HSMul.hSMul (β := ℂ) (1 / 1)
      (∫ (x : ℝ) in 0..HAdd.hAdd (α := ℝ) 0 1,
        HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          (Periodic.lift (f :=
            (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯
            (↑x : ℝ ⧸ AddSubgroup.zmultiples 1))) =
    ∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
⊢ 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 : ℂ)
have simp_rw₁ : HSMul.hSMul (α := ℝ) (β := ℂ) 1
    (∫ (x : ℝ) in 0..HAdd.hAdd (α := ℝ) 0 1,
      HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ))
          sorry (↑x : ℝ ⧸ AddSubgroup.zmultiples 1))) =
  ∫ (x : ℝ) in 0..1,
    HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
Tactic: 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]
-- 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
simp_rw :
  HSMul.hSMul (β := ℂ) (1 / 1)
      (∫ (x : ℝ) in 0..HAdd.hAdd (α := ℝ) 0 1,
        HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          (Periodic.lift (f :=
            (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯
            (↑x : ℝ ⧸ AddSubgroup.zmultiples 1))) =
    ∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
simp_rw₁ :
  HSMul.hSMul (α := ℝ) (β := ℂ) 1
      (∫ (x : ℝ) in 0..HAdd.hAdd (α := ℝ) 0 1,
        HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          (Periodic.lift (f :=
            (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯
            (↑x : ℝ ⧸ AddSubgroup.zmultiples 1))) =
    ∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
⊢ 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 : ℂ)
have simp_rw₂ : Eq (α := ℂ)
  (∫ (x : ℝ) in 0..HAdd.hAdd (α := ℝ) 0 1,
    HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) sorry
        (↑x : ℝ ⧸ AddSubgroup.zmultiples 1)))
  (∫ (x : ℝ) in 0..1,
    HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
Tactic: 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]
-- 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
simp_rw :
  HSMul.hSMul (β := ℂ) (1 / 1)
      (∫ (x : ℝ) in 0..HAdd.hAdd (α := ℝ) 0 1,
        HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          (Periodic.lift (f :=
            (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯
            (↑x : ℝ ⧸ AddSubgroup.zmultiples 1))) =
    ∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
simp_rw₁ :
  HSMul.hSMul (α := ℝ) (β := ℂ) 1
      (∫ (x : ℝ) in 0..HAdd.hAdd (α := ℝ) 0 1,
        HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          (Periodic.lift (f :=
            (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯
            (↑x : ℝ ⧸ AddSubgroup.zmultiples 1))) =
    ∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
simp_rw₂ :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..HAdd.hAdd (α := ℝ) 0 1,
      HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ))
          ⋯ (↑x : ℝ ⧸ AddSubgroup.zmultiples 1)))
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
⊢ 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 : ℂ)
have simp_rw₃ : Eq (α := ℂ)
  (∫ (x : ℝ) in 0..1,
    HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) sorry
        (↑x : ℝ ⧸ AddSubgroup.zmultiples 1)))
  (∫ (x : ℝ) in 0..1,
    HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
Tactic: 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]
-- 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 (α := ℂ)
    (∫ (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)
have simp_rw : Eq (α := ℂ)
  (∫ (x : ℝ) in 0..1,
    HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
  (∫ (x : ℝ) in 0..1,
    ∑' (n : ℤ),
      HMul.hMul (α := (a : ℝ) → ℂ) (β := (a : ℝ) → ℂ) (⇑e : (a : ℝ) → ℂ)
        (⇑(f.comp (ContinuousMap.addRight (↑n : ℝ))) : (a : ℝ) → ℂ) x)
Tactic: simp_rw [coe_mul, Pi.mul_apply,
        ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]
-- 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
simp_rw :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
    (∫ (x : ℝ) in 0..1,
      ∑' (n : ℤ),
        HMul.hMul (α := (a : ℝ) → ℂ) (β := (a : ℝ) → ℂ) (⇑e : (a : ℝ) → ℂ)
          (⇑(f.comp (ContinuousMap.addRight (↑n : ℝ))) : (a : ℝ) → ℂ) x)
⊢ 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)
have simp_rw₁ : Eq (α := ℂ)
  (∫ (x : ℝ) in 0..1,
    HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
  (∫ (x : ℝ) in 0..1,
    ∑' (n : ℤ),
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
Tactic: simp_rw [coe_mul, Pi.mul_apply,
        ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]
-- 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
simp_rw :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
    (∫ (x : ℝ) in 0..1,
      ∑' (n : ℤ),
        HMul.hMul (α := (a : ℝ) → ℂ) (β := (a : ℝ) → ℂ) (⇑e : (a : ℝ) → ℂ)
          (⇑(f.comp (ContinuousMap.addRight (↑n : ℝ))) : (a : ℝ) → ℂ) x)
simp_rw₁ :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
    (∫ (x : ℝ) in 0..1,
      ∑' (n : ℤ),
        HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
          ((f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
⊢ 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)
have simp_rw₂ : Eq (α := ℂ)
  (∫ (x : ℝ) in 0..1,
    HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
      (∑' (i : ℤ), (f.comp (ContinuousMap.addRight (↑i : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
  (∫ (x : ℝ) in 0..1,
    ∑' (n : ℤ),
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
Tactic: simp_rw [coe_mul, Pi.mul_apply,
        ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]
-- 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 (α := ℂ) (∫ (x : ℝ) in 0..1, ∑' (n : ℤ), (e * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
    (∑' (n : ℤ), ∫ (x : ℝ) in 0..1, (e * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
have refine : Summable (α := ℝ) fun (i : ℤ) ↦
  ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := sorry : Compacts ℝ } : Set ℝ)
      (e * f.comp (ContinuousMap.addRight (↑i : ℝ)))‖
Tactic: refine (intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm ?_).symm
-- 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
⊢ Summable (α := ℝ) fun (i : ℤ) ↦
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
        (e * f.comp (ContinuousMap.addRight (↑i : ℝ)))‖
have h : Eq (α := ℤ → ℝ)
  (fun (i : ℤ) ↦
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := sorry : Compacts ℝ } : Set ℝ)
        (e * f.comp (ContinuousMap.addRight (↑i : ℝ)))‖)
  fun (n : ℤ) ↦
  ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := sorry : Compacts ℝ } : Set ℝ)
      (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
Tactic: convert! hf ⟨uIcc 0 1, isCompact_uIcc⟩ using 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
⊢ Eq (α := ℂ) (∑' (n : ℤ), ∫ (x : ℝ) in 0..1, (e * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
    (∑' (n : ℤ), ∫ (x : ℝ) in 0..1, ((e * f).comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
have simp : Eq (α := ℂ) (∑' (n : ℤ), ∫ (x : ℝ) in 0..1, (e * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
  (∑' (n : ℤ),
    ∫ (x : ℝ) in 0..1,
      (e.comp (ContinuousMap.addRight (↑n : ℝ)) * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
Tactic: simp only [mul_comp] at eadd ⊢
-- 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 (α := ℂ) (∑' (n : ℤ), ∫ (x : ℝ) in 0..1, ((e * f).comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) ((f : (a : ℝ) → ℂ) x : ℂ))
have suffices : @Integrable ℂ _ _ ℝ MeasureSpace.toMeasurableSpace (⇑(e * f) : (a : ℝ) → ℂ) volume
Tactic: suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq
-- 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
⊢ @Integrable ℂ _ _ ℝ MeasureSpace.toMeasurableSpace (⇑(e * f) : (a : ℝ) → ℂ) volume
have hf₁ : Summable (α := ℝ) fun (n : ℤ) ↦
  Norm.norm (E := C((↑(Icc 0 1) : Type), ℂ))
    (ContinuousMap.restrict (Icc 0 1) ((e * f).comp (ContinuousMap.addRight (↑n : ℝ))))
Tactic: apply integrable_of_summable_norm_Icc
-- 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
⊢ Summable (α := ℝ) fun (n : ℤ) ↦
    Norm.norm (E := C((↑(Icc 0 1) : Type), ℂ))
      (ContinuousMap.restrict (Icc 0 1) ((e * f).comp (ContinuousMap.addRight (↑n : ℝ))))
have h : Eq (α := ℤ → ℝ)
  (fun (n : ℤ) ↦
    Norm.norm (E := C((↑(Icc 0 1) : Type), ℂ))
      (ContinuousMap.restrict (Icc 0 1) ((e * f).comp (ContinuousMap.addRight (↑n : ℝ)))))
  fun (n : ℤ) ↦
  ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := sorry : Compacts ℝ } : Set ℝ)
      (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
Tactic: convert! hf ⟨Icc 0 1, isCompact_Icc⟩ using 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
⊢ Eq (α := ℤ → ℝ)
    (fun (n : ℤ) ↦
      Norm.norm (E := C((↑(Icc 0 1) : Type), ℂ))
        (ContinuousMap.restrict (Icc 0 1) ((e * f).comp (ContinuousMap.addRight (↑n : ℝ)))))
    fun (n : ℤ) ↦
    ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
        (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
have h : Eq (α := ℤ → ℝ)
  (fun (n : ℤ) ↦
    Norm.norm (E := C((↑(Icc 0 1) : Type), ℂ))
      (ContinuousMap.restrict (Icc 0 1)
        (e.comp (ContinuousMap.addRight (↑n : ℝ)) * f.comp (ContinuousMap.addRight (↑n : ℝ)))))
  fun (n : ℤ) ↦
  ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := sorry : Compacts ℝ } : Set ℝ)
      (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
Tactic: simp_rw [mul_comp] at eadd ⊢
-- 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 (α := ℤ → ℝ)
    (fun (n : ℤ) ↦
      Norm.norm (E := C((↑(Icc 0 1) : Type), ℂ))
        (ContinuousMap.restrict (Icc 0 1)
          (e.comp (ContinuousMap.addRight (↑n : ℝ)) * f.comp (ContinuousMap.addRight (↑n : ℝ)))))
    fun (n : ℤ) ↦
    ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
        (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
have h : Eq (α := ℤ → ℝ)
  (fun (n : ℤ) ↦
    Norm.norm (E := C((↑(Icc 0 1) : Type), ℂ))
      (ContinuousMap.restrict (Icc 0 1) (e * f.comp (ContinuousMap.addRight (↑n : ℝ)))))
  fun (n : ℤ) ↦
  ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := sorry : Compacts ℝ } : Set ℝ)
      (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
Tactic: simp_rw [eadd]
-- 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
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) ((f : (a : ℝ) → ℂ) x : ℂ)) =
    𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑m : ℝ)
have rw : 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 : ℂ))
Tactic: rw [fourier_real_eq_integral_exp_smul]