OAI/Analysis/LipschitzHilbert/Trees/SourceInhabitedLabels.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Removing labels with no items preserves every packet and every source band. Only genuinely populated assigned fibers enter label counts.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedLabels line 17
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedOriginalLabel line 20
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedLabel_nonempty line 23
  4. def OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily line 26
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_length line 53
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_actualX line 54
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_actualZ line 56
  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_rowSlope line 58
  9. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_constant line 60
  10. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_absoluteConstant line 61
  11. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_label_card line 62
  12. def OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedItemsEquiv line 65
  13. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_inhabited line 72
  14. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_raw line 82
  15. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_physicalPacket line 86
  16. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_physicalMultiplierCoefficient line 91
  17. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_rawBand line 98
  18. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_rawInterval line 107
  19. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedLabels_card_le line 115
  20. def OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedAlternate line 123
  21. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedAlternate_bound line 127
  22. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_withProfile line 134
  23. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_physicalMaskedBand line 140