awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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
refine :
  Summable (α := ℝ) fun (i : ℤ) ↦
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
        (e * f.comp (ContinuousMap.addRight (↑i : ℝ)))‖
⊢ 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)

Tactic:
refine (intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm ?_).symm

Premises used: intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm, Eq.symm
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 : ℤ) ↦
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
        (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖

Tactic:
hf ⟨uIcc 0 1, isCompact_uIcc⟩

Premises used: isCompact_uIcc, TopologicalSpace.Compacts.mk, OfNat.ofNat, Set.uIcc
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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
h :
  Eq (α := ℤ → ℝ)
    (fun (i : ℤ) ↦
      ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
          (e * f.comp (ContinuousMap.addRight (↑i : ℝ)))‖)
    fun (n : ℤ) ↦
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
        (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
⊢ Summable (α := ℝ) fun (i : ℤ) ↦
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
        (e * f.comp (ContinuousMap.addRight (↑i : ℝ)))‖

Tactic:
convert! hf ⟨uIcc 0 1, isCompact_uIcc⟩ using 1

Premises used: isCompact_uIcc, TopologicalSpace.Compacts.mk, OfNat.ofNat, Set.uIcc
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 (i : ℤ) ↦
      ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
          (e * f.comp (ContinuousMap.addRight (↑i : ℝ)))‖)
    fun (n : ℤ) ↦
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
        (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖

Tactic:
funext fun n => neK _ _

Premises used: Int.cast, ContinuousMap.comp, isCompact_uIcc, TopologicalSpace.Compacts.mk, funext, OfNat.ofNat, Set.uIcc, ContinuousMap.addRight
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 (i : ℤ) ↦
      ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
          (e * f.comp (ContinuousMap.addRight (↑i : ℝ)))‖)
    fun (n : ℤ) ↦
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
        (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖

Tactic:
exact funext fun n => neK _ _

Premises used: funext
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 :
  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)
⊢ 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)

Tactic:
simp only [mul_comp] at eadd ⊢

Premises used: ContinuousMap.mul_comp
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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.comp (ContinuousMap.addRight (↑n : ℝ)) * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)

Tactic:
simp_rw [eadd]
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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
suffices : @Integrable ℂ _ _ ℝ MeasureSpace.toMeasurableSpace (⇑(e * f) : (a : ℝ) → ℂ) volume
⊢ 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 : ℂ))

Tactic:
suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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
hf₁ :
  Summable (α := ℝ) fun (n : ℤ) ↦
    Norm.norm (E := C((↑(Icc 0 1) : Type), ℂ))
      (ContinuousMap.restrict (Icc 0 1) ((e * f).comp (ContinuousMap.addRight (↑n : ℝ))))
⊢ @Integrable ℂ _ _ ℝ MeasureSpace.toMeasurableSpace (⇑(e * f) : (a : ℝ) → ℂ) volume

Tactic:
apply integrable_of_summable_norm_Icc

Premises used: Real.integrable_of_summable_norm_Icc
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 : ℤ) ↦
    ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
        (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖

Tactic:
hf ⟨Icc 0 1, isCompact_Icc⟩

Premises used: CompactIccSpace.isCompact_Icc, TopologicalSpace.Compacts.mk, Set.Icc, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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
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' := ⋯ : Compacts ℝ } : Set ℝ)
        (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
⊢ Summable (α := ℝ) fun (n : ℤ) ↦
    Norm.norm (E := C((↑(Icc 0 1) : Type), ℂ))
      (ContinuousMap.restrict (Icc 0 1) ((e * f).comp (ContinuousMap.addRight (↑n : ℝ))))

Tactic:
convert! hf ⟨Icc 0 1, isCompact_Icc⟩ using 1

Premises used: CompactIccSpace.isCompact_Icc, TopologicalSpace.Compacts.mk, Set.Icc, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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
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' := ⋯ : Compacts ℝ } : Set ℝ)
        (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
⊢ 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 : ℝ)))‖

Tactic:
simp_rw [mul_comp] at eadd ⊢

Premises used: ContinuousMap.mul_comp
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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
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' := ⋯ : Compacts ℝ } : Set ℝ)
        (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
⊢ 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 : ℝ)))‖

Tactic:
simp_rw [eadd]
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 : ℝ)))‖

Tactic:
funext fun n => neK ⟨Icc 0 1, isCompact_Icc⟩ _

Premises used: Int.cast, ContinuousMap.comp, CompactIccSpace.isCompact_Icc, TopologicalSpace.Compacts.mk, funext, Set.Icc, OfNat.ofNat, ContinuousMap.addRight
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 : ℝ)))‖

Tactic:
exact funext fun n => neK ⟨Icc 0 1, isCompact_Icc⟩ _

Premises used: CompactIccSpace.isCompact_Icc, TopologicalSpace.Compacts.mk, funext, Set.Icc, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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
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 : ℂ))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) ((f : (a : ℝ) → ℂ) x : ℂ)) =
    𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑m : ℝ)

Tactic:
rw [fourier_real_eq_integral_exp_smul]

Premises used: Real.fourier_real_eq_integral_exp_smul
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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
e_f :
  ∀ (x : ℝ),
    HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) ((f : (a : ℝ) → ℂ) x : ℂ) =
      HSMul.hSMul (β := ℂ) (cexp ((↑(-2 * π * x * (↑m : ℝ)) : ℂ) * I)) ((f : (a : ℝ) → ℂ) x : ℂ)
⊢ 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:
congr 1 with x : 1
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 : ℝ
e_f :
  HMul.hMul (β := ℂ) (cexp (2 * (↑π : ℂ) * I * (↑(-m) : ℂ) * (↑x : ℂ) / (↑1 : ℂ))) ((f : (a : ℝ) → ℂ) x : ℂ) =
    HMul.hMul (β := ℂ) (cexp ((↑(-2 * π * x * (↑m : ℝ)) : ℂ) * I)) ((f : (a : ℝ) → ℂ) x : ℂ)
⊢ HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) ((f : (a : ℝ) → ℂ) x : ℂ) =
    HSMul.hSMul (β := ℂ) (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]

Premises used: fourier_coe_apply, ContinuousMap.comp_apply, ContinuousMap.coe_mk, smul_eq_mul, ContinuousMap.toFun_eq_coe
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 : ℝ
e_f : 2 * (↑π : ℂ) * I * (↑(-m) : ℂ) * (↑x : ℂ) / (↑1 : ℂ) = (↑(-2 * π * x * (↑m : ℝ)) : ℂ) * I
⊢ HMul.hMul (β := ℂ) (cexp (2 * (↑π : ℂ) * I * (↑(-m) : ℂ) * (↑x : ℂ) / (↑1 : ℂ))) ((f : (a : ℝ) → ℂ) x : ℂ) =
    HMul.hMul (β := ℂ) (cexp ((↑(-2 * π * x * (↑m : ℝ)) : ℂ) * I)) ((f : (a : ℝ) → ℂ) x : ℂ)

Tactic:
congr 2
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 : ℝ
e_f : 2 * (↑π : ℂ) * I * -(↑m : ℂ) * (↑x : ℂ) / 1 = -2 * (↑π : ℂ) * (↑x : ℂ) * (↑m : ℂ) * I
⊢ 2 * (↑π : ℂ) * I * (↑(-m) : ℂ) * (↑x : ℂ) / (↑1 : ℂ) = (↑(-2 * π * x * (↑m : ℝ)) : ℂ) * I

Tactic:
push_cast
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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

Tactic:
ring
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)

Tactic:
h_sum
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 := ⋯ }
h : ∀ (x : ℤ), fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ) x = 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑x : ℝ)
⊢ Summable (α := ℂ) (fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ))

Tactic:
convert! h_sum
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
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 := ⋯ }
x_1 : ℤ
⊢ fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ) x_1 = 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑x_1 : ℝ)

Tactic:
Real.fourierCoeff_tsum_comp_add h_norm _

Premises used: Real.fourierCoeff_tsum_comp_add, Quotient.liftOn', Function.Periodic.lift