OAI/Analysis/LipschitzHilbert/Packets/PacketDataRecenteredReferenceConditions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original spectra, selectors and assigned packet geometry imply every local hypothesis of the selected-reference tail theorem after recentering. The selected packet set may have empty fibers and arbitrary finite support.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.recentered_reference_conditions line 17