OAI/Analysis/LipschitzHilbert/Packets/PacketDataUniformReverseDisparity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The supported reverse estimate with constants independent of the finite lattice. All geometric dependence is exposed in reverseModelCost.

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