OAI/Analysis/LipschitzHilbert/Trees/SourcePhysicalOffchildGrouping.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original masked off-child packets give the exact off-child sum of their assigned physical top bands. This is the identification needed when applying the original-selector off-child estimate to a stopped path.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedPhysicalBands_eq line 24
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalOffchildAmplitude_top_bands line 43