OAI/Analysis/LipschitzHilbert/Packets/SourceSizeOnePacket.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A literal one-packet separated test controls each coefficient. The top direction is chosen inside its actual half-open angular cell.

  1. theorem OAI.LipschitzHilbert.interval_far_point line 12

    Also declared: OAI/Analysis/LipschitzHilbert/Packets/PacketDataSizeOnePacket.lean:12 (same declaration text).

  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_one_packet_size_direction line 26
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.coefficient_le_of_size_tests line 62