OAI/Analysis/LipschitzHilbert/Estimates/HilbertEndpointCases.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The complementary endpoint cases: no very-short segment when the inner endpoint is already large, and no packet segment for wide bands.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertMiddleLong_bound line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertShortLong_bound line 36