OAI/Analysis/LipschitzHilbert/Trees/SourcePhysicalSquareTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The positive main square has a tail on every original physical interval, with the exact reference coordinate change and no interval scale in its constants.

  1. theorem OAI.LipschitzHilbert.SourceLatticePacket.physical_reference_square_tail line 16