AddCircle.liftIco_convolution_liftIco

theorem liftIco_convolution_liftIco (hf : f.Periodic T) (hg : g.Periodic T) :    liftIco T a f ⋆[L] liftIco T a g = liftIco T a fun x ↦ ∫ y in a..a+T, L (f y) (g (x - y)) := by  refine funext (fun q ↦ QuotientAddGroup.induction_on q (fun x ↦ ?_))  have : Periodic (fun x ↦ ∫ y in a..a+T, L (f y) (g (x-y))) T := by    intro; refine integral_congr (fun _ _ ↦ ?_); rw [add_sub_right_comm, hg]  rw [convolution, ← AddCircle.intervalIntegral_preimage T a, liftIco_coe_apply_of_periodic a this]  refine integral_congr (fun y _ ↦ ?_)  rw [AddCircle.liftIco_coe_apply_of_periodic a hf, ← AddCircle.liftIco_coe_apply_of_periodic a hg]  rfl