OAI/Analysis/LipschitzHilbert/Packets/PacketDataReferenceBand.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recentring an entire already-selected top family preserves its physical length bands. Only the literal short-cone membership is needed.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_physicalMaskedBand_all line 16