OAI/Analysis/LipschitzHilbert/Trees/SourceReferenceRestriction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The fixed reference collection is a literal restriction of the original labels. Its new reference coordinates keep every selected profile, integer site and physical packet unchanged.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.referenceLabels line 18
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.referenceOriginalLabel line 24
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceLabel_bounds line 28
  4. def OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily line 44

    Source documentation

    Only labels in the fixed short reference cone remain. All spatial items in those labels retain the original lattice and profile.

    def referenceFamily (oldSlope newSlope referenceLength cone w F : ℝ)
    (hw : 0 < w) (hcone : 0 ≤ cone) (hF : 0 ≤ F) (hwide : cone*w ≤ P.width)
    (hfrequency : ∀ k, |P.frequency k| ≤ F/w) : SourceLabeledLattice N κ Label Item where
…

    Mentions: OAI.LipschitzHilbert.SourceLabeledLattice

  5. abbrev OAI.LipschitzHilbert.SourceLabeledLattice.RefLabel line 94
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_length line 96
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_actualX line 100
  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_actualZ line 105
  9. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_physicalPacket line 113
  10. theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceFamily_spectrum line 145