OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledComparableEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The comparable-scale contribution for the actual labeled packet family. Both the scale window and angular multiplicity are uniform.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalScaleComponent line 16
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalScaleComponent_vector line 21
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalScaleComponent_energy line 30
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_comparable_gram_energy line 40