OAI/Analysis/LipschitzHilbert/Phase/FiniteDiagonalReverseL1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform reverse-disparity estimate for the actual finite diagonal band form. Slope labels, plateaus, compact symbols, and profile budgets are all constructed inside the proof. The scalar width W=w is included.

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