Smooth interpolation between symmetric operators

Two bounded symmetric operators Sm and Sp on a real inner product space are joined by a C¹ family of symmetric operators that equals Sm on (-∞, -R] and Sp on [R, ∞), is locally constant off [-R, R], and has norm at most ‖Sm‖ + ‖Sp - Sm‖ (TauCeti.exists_contDiff_isSymmetric_interpolation). The family interpolates through Real.smoothTransition.

theorem TauCeti.exists_contDiff_isSymmetric_interpolation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Sm Sp : E →L[ℝ] E} (hSm : (↑Sm).IsSymmetric) (hSp : (↑Sp).IsSymmetric) {R : ℝ} (hR : 0 < R) : ∃ (S : ℝ → E →L[ℝ] E), ContDiff ℝ 1 S ∧ (∀ (s : ℝ), (↑(S s)).IsSymmetric) ∧ (∀ s ≤ -R, S s = Sm) ∧ (∀ (s : ℝ), R ≤ s → S s = Sp) ∧ (∀ s ∉ Set.Icc (-R) R, deriv S s = 0) ∧ ∀ (s : ℝ), ‖S s‖ ≤ ‖Sm‖ + ‖Sp - Sm‖

A C¹ family of symmetric operators equal to Sm on (-∞, -R] and to Sp on [R, ∞), with norm at most ‖Sm‖ + ‖Sp - Sm‖. It interpolates through Real.smoothTransition.