OAI/Geometry/RCD/Coordinates/CovectorCommutator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.covector_commutator_norm_le line 14

   Source documentation

   The affine Sobolev identity acts on covectors, so its commutator has this reversed order. The same near-identity absorption controls B.

   theorem covector_commutator_norm_le (A B : E →L[ℝ] E)
       (hA : ‖A - 1‖ ≤ 1 / 4) {η : ℝ}
       (herror : ‖A * B - B * (A - 1)‖ ≤ η) : ‖B‖ ≤ 2 * η := by
   …