SourceCovariantTop.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A common exceptional set for all actual covariant top derivatives, with a fixed polynomial threshold at the manuscript's scales.

theorem OAI.LipschitzHilbert.PlanarPacketFamily.source_covariant_top line 14