OAI/Analysis/LipschitzHilbert/Packets/PacketReferenceSpectrum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The unrestricted family passes its original spectra to every local reference lattice without enlarging either frequency strip.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_slope line 17
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_spectrum_at line 23
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_bin_at line 41
  4. def OAI.LipschitzHilbert.PacketLatticeData.referenceSelector line 56

    Source documentation

    The local family carries the original selector as a function of the physical direction. Only its label type changes.

    def referenceSelector (b : ∀ j, P.labels j → κ → ℝ → ℂ) :
    ∀ j, (Q).labels j → κ → ℝ → ℂ :=
…
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceSelector_support line 60