OAI/Geometry/RCD/Coordinates/RadialFrameChange.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transporting a radial coefficient operator to the common frame

  1. theorem OAI.RegularPointCoordinates.radial_frame_change_bound line 14

    Source documentation

    A bounded change of frame preserves smallness of a radial operator's error from the identity, with the explicit two frame factors.

    theorem radial_frame_change_bound (P : E ≃L[ℝ] E) (A : E →L[ℝ] E) :
    ‖P.symm.toContinuousLinearMap * A * P.toContinuousLinearMap - 1‖ ≤
      ‖P.symm.toContinuousLinearMap‖ * ‖A - 1‖ * ‖P.toContinuousLinearMap‖ := by
…