OAI/Analysis/LipschitzHilbert/Estimates/StrongOperatorDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The strong product rule needed for the sampling conjugation. A uniform operator bound replaces differentiability in operator norm.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.hasDerivAt_strong_operator_apply line 12