OAI/Analysis/LipschitzHilbert/Estimates/ConstructedCovariantTop.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global top concentration for the actual covariant derivative. The original analyzing integrals are retained when synthesis is differentiated.

  1. theorem OAI.LipschitzHilbert.PlanarPacketFamily.constructed_covariant_top line 15