OAI/Analysis/LipschitzHilbert/Packets/PacketDataPartial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Physical scale partial sums and their continuous interval maximum for unrestricted packet data.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.continuous_interval_max line 14
  2. def OAI.LipschitzHilbert.PacketLatticeData.physicalTreePartial line 30
  3. def OAI.LipschitzHilbert.PacketLatticeData.physicalTreeMaximal line 37
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.physicalTreePartial_continuous line 41
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.physicalTreeMaximal_continuous line 56