OAI/Analysis/LipschitzHilbert/Packets/PacketLatticeData.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The finite packet family before choosing a reference direction. There is no small-shear condition on its slopes. That condition is proved only for the labels retained in a short reference cone.

  1. structure OAI.LipschitzHilbert.PacketLatticeData line 12
  2. def OAI.LipschitzHilbert.PacketLatticeData.length line 42
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.length_pos line 44
  4. def OAI.LipschitzHilbert.PacketLatticeData.actualX line 47
  5. def OAI.LipschitzHilbert.PacketLatticeData.actualZ line 50
  6. def OAI.LipschitzHilbert.PacketLatticeData.physicalPacket line 54
  7. def OAI.LipschitzHilbert.PacketLatticeData.referenceLabels line 60
  8. def OAI.LipschitzHilbert.PacketLatticeData.referenceOriginalLabel line 66
  9. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceLabel_bounds line 70
  10. def OAI.LipschitzHilbert.PacketLatticeData.referenceFamily line 86

    Source documentation

    The reference lattice derives both dimensionless bounds from its cone. No bound on the slopes of the original packet family is used.

    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

  11. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_length line 141
  12. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_actualX line 143
  13. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_actualZ line 148
  14. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_physicalPacket line 157