(S : UnboundedSelfAdjoint H) {y : ℝ → H} {y' : H} {t u : ℝ} (hy : HasDerivAt y y' u) : HasDerivAt (fun r : ℝ => S.stoneU (t - r) (y r - y u)) (S.stoneU (t

Initializing...

(S : UnboundedSelfAdjoint H) {y : ℝ → H} {y' : H} {t u : ℝ} (hy : HasDerivAt y y' u) : HasDerivAt (fun r : ℝ => S.stoneU (t - r) (y r - y u)) (S.stoneU (t - u) y') u · Prove2Me