OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialDuhamel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The difference formula for matrix exponentials

The scalar-time exponential derivative and the fundamental theorem of calculus give the noncommutative difference formula. This is the concrete step toward identifying the differential in the retained Dixmier input.

  1. theorem OAI.PolycyclicRecognition.hasDerivAt_exponential_bridge line 25
  2. theorem OAI.PolycyclicRecognition.exponential_sub_eq_integral line 44