OAI/Analysis/LipschitzHilbert/Phase/FiniteDiagonalBasicL1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform basic 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_basic_l1 line 16