OAI/Geometry/RCD/Sobolev/ComposedGammaPairingVariation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Variation of a weighted nonlinear gradient square

Only the original Sobolev path and the L² weight are differentiated.

  1. theorem OAI.RegularPointCoordinates.composed_gamma_pairing_hasDerivAt line 18