OAI/Analysis/LipschitzHilbert/Trees/SourcePhysicalPathAssembly.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The measurable active path and every marked predictor are unchanged when the original physical packets are grouped into their assigned top and length bands. Both sides retain the original selector coefficients.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.assignedPhysicalBands line 24
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalActivePathValue_top_bands line 30
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalShiftedPathPrediction_top_bands line 53