OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledActiveCardTail.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Only frozen-active labels need slots in the main reference tail. Their cardinality follows from the original local slope multiplicity, uniformly over the number of vector coordinates and inactive labels.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveLabels_card_local line 19
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenActive_referenceLabels_card_le line 39
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveLabels_card_source line 46
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_active_narrow_main_square_spectral_tail line 60
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_active_narrow_centered_masked_variation_spectral_tail line 108