OAI/Analysis/LipschitzHilbert/Trees/SourceReferenceSelectorGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The physical selector centers are invariant under recentering. Restricting to the reference cone can only decrease their local count.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_physical_center line 20
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_localMultiplicity line 25
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_selector_support line 46