OAI/Analysis/LipschitzHilbert/Estimates/ConstructedTopNeighborhood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual integral-defined top packet sum, on the physical plane, has a common exceptional set for all intervals and vertical shifts.

  1. theorem OAI.LipschitzHilbert.PlanarPacketFamily.constructed_top_neighborhood line 14