OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledActiveReference.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The narrow main reference family retains only labels active at the frozen direction. Inactive labels contribute exactly zero, so neither the square nor the masked variation needs spectral assumptions there.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveLabels line 18
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveOriginalLabel line 21
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveLabel_nonzero line 24
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveLabels_card_le line 30
  5. def OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveFamily line 34
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveFamily_constant line 61
  7. def OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveSelector line 63
  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveFamily_physicalPacket line 66
  9. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveFamily_positiveEnvelope line 71
  10. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveFamily_raw line 76
  11. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveFamily_alt_raw line 81
  12. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveFamily_frozenCoefficient line 91
  13. def OAI.LipschitzHilbert.SourceLabeledLattice.frozenActiveLabelsEquiv line 98
  14. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_frozenActive_of_zero line 106
  15. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainScale_eq_frozenActive line 128
  16. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainSquare_eq_frozenActive line 139
  17. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedBand_eq_frozenActive line 146
  18. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedVariation_eq_frozenActive line 170