Commutativeness of Linear Operator Series

Stream: mathlib4

[Fengyang Wang]

Updated to minimal working environment (Resolved!)

 import mathlib

open scoped Topology
open Metric Set Filter ContinuousLinearMap
open BigOperators

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]

lemma tsum_apply_op {X : E →L[ℝ] E} {x : E} :
    (∑' n, X ^ (n + N)) x = ∑' n, (X ^ (n + N)) x := by
    -- Use the HasSum characterization directly
    sorry

Thanks for any help

[Kevin Buzzard]

Can you edit your message to make it a #mwe so it's easier for people to answer?

[Fengyang Wang]

Kevin Buzzard said:

Can you edit your message to make it a #mwe so it's easier for people to answer?

This is a good idea. I will update this post shortly.