OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledActiveSpectrum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The active narrow reference annuli follow from the original two-dimensional packet spectrum. The selector's lower angular separation is used only on labels that occur in the frozen main sum. All three covariant jets inherit these annuli, including alternate synthesis profiles on the same physical geometry.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.raw_fourier_cutoffs_at line 20
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceSelf_active_raw_cutoffs line 53
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceSelf_active_alt_raw_cutoffs line 76
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_narrow_main_square_spectral_tail line 99
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_narrow_centered_masked_variation_spectral_tail line 150