OAI/Analysis/LipschitzHilbert/Estimates/ConstructedTopFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sum the actual top-packet exceptions. The conclusion is uniform in the number of tops, packet scales, and Hilbert dimension.

  1. theorem OAI.LipschitzHilbert.PlanarPacketFamily.constructed_top_family line 13