OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialDuhamelDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The differential of the noncommutative exponential

The difference formula and continuity of integrals on a compact interval identify the derivative along each line. Analyticity then identifies the actual Frechet differential; no inverse-exponential theorem is assumed.

  1. theorem OAI.PolycyclicRecognition.hasDerivAt_exp_add_smul_zero line 24
  2. theorem OAI.PolycyclicRecognition.fderiv_exp_eq_integral line 55