OAI/GroupTheory/PolycyclicRecognition/Algebra/ReweightedFrameBracket.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.lieBracket_reweighted_frame line 16

   Source documentation

   At a point where both frames are the identity, the correction to the bracket is precisely the antisymmetric part of the changing frame.

   theorem lieBracket_reweighted_frame
       {F R : E → E →L[ℝ] E} {dF dR : E →L[ℝ] E →L[ℝ] E} {x : E}
       (hF : HasFDerivAt F dF x) (hR : HasFDerivAt R dR x)
       (hF₀ : F x = ContinuousLinearMap.id ℝ E)
       (hR₀ : R x = ContinuousLinearMap.id ℝ E) (v w : E) :
       lieBracket ℝ (fun y => F y (R y v)) (fun y => F y (R y w)) x =
         lieBracket ℝ (fun y => F y v) (fun y => F y w) x + dR v w - dR w v := by
   …