OAI/Analysis/LipschitzHilbert/Packets/PacketDataFiniteSizeBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every finite packet collection has a finite initial unsigned size. This starts the threshold algorithm without an additional size premise.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.unsignedSizeTestEnergy_le_coefficient_sum line 14
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_finite_unsigned_size_bound line 31