OAI/Analysis/LipschitzHilbert/Packets/PacketDataUniformBoundedSize.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The bounded-input constant is chosen before the packet lattice, its translation, and its finite collection. Its remaining dependence is explicit.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_uniform_bounded_unsigned_size line 14