OAI/Geometry/RCD/Coordinates/TwoFrozenPairingVariation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A pairing derivative from both frozen scalar pairings

One Lipschitz-order increment and continuity of the other factor make the mixed increment negligible. Neither factor needs a vector derivative.

  1. theorem OAI.RegularPointCoordinates.hasDerivAt_inner_of_two_frozen line 16