OAI/Analysis/LipschitzHilbert/Packets/TopPacketWindow.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Actual top-weighted line packets. The window records only geometry and the fixed packet decay order, and introduces no concentration input.

  1. structure OAI.LipschitzHilbert.TopPacketWindow line 16
  2. def OAI.LipschitzHilbert.TopPacketWindow.constant line 37
  3. theorem OAI.LipschitzHilbert.TopPacketWindow.constant_pos line 39
  4. theorem OAI.LipschitzHilbert.TopPacketWindow.constant_ge line 43
  5. def OAI.LipschitzHilbert.TopPacketWindow.family line 51
  6. theorem OAI.LipschitzHilbert.TopPacketWindow.family_budget line 71
  7. theorem OAI.LipschitzHilbert.TopPacketWindow.family_packets line 74
  8. theorem OAI.LipschitzHilbert.TopPacketWindow.family_variation line 79