OAI/Analysis/LipschitzHilbert/Phase/FiniteDiagonalHighL1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The positive-disparity gain for the actual finite diagonal band. Only the fixed low scales needed for bounded slope labels are excluded.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.exists_finite_diagonal_high_l1 line 16