OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledRecenter.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Recenter a selected labelled lattice on its tree direction. Sites and profiles remain original, and the shear preserves physical packets.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.recenter line 15
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.recenter_cone_bounds line 27
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.recenter_length line 51
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.recenter_absoluteConstant line 54
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.recenter_actualX line 57
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.recenter_actualZ line 60
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.recenter_physicalPacket line 65
  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.recenter_fourier line 82