Star operations on derivatives #
This file contains the usual formulas (and existence assertions) for the FrΓ©chet derivative of the
star operation. For detailed documentation of the FrΓ©chet derivative, see the module docstring of
Analysis/Calculus/FDeriv/Basic.lean
.
Most of the results in this file only apply when the field that the derivative is respect to has a
trivial star operation; which as should be expected rules out π = β
. The exceptions are
HasFDerivAt.star_star
and DifferentiableAt.star_star
, showing that star β f β star
is
differentiable when f
is (and giving a formula for its derivative).
If f
has derivative f'
at z
, then star β f β star
has derivative starL β f' β starL
at star z
.
If f
is differentiable at z
, then star β f β star
is differentiable at star z
.