(S : E →L[ℂ] E) (hS : ∀ w : E, ‖S w‖ ≤ ‖w‖) (n : ℕ) (v : E) : ‖(S ^ n) v‖ ≤ ‖v‖

Initializing...

(S : E →L[ℂ] E) (hS : ∀ w : E, ‖S w‖ ≤ ‖w‖) (n : ℕ) (v : E) : ‖(S ^ n) v‖ ≤ ‖v‖ · Prove2Me