OAI/Analysis/LipschitzHilbert/Packets/PacketDataUniformCrossReverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform reverse-disparity control of the distinct-profile form. All constants are chosen before the finite translated lattice.

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