OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedTopSelector.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The assigned-top constructor preserves the original selectors, packet spectra, and local label count. Its geometry is supplied by the actual selected packets; the global longest-scale bound remains explicit.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopLabel_first line 20
  2. def OAI.LipschitzHilbert.PacketLatticeData.assignedTopLabel line 24
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopLabel_injective line 27
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopItem_mem line 34
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopItem_assignment line 39
  6. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_referenceEnvelopeConstant line 45
  7. def OAI.LipschitzHilbert.PacketLatticeData.assignedTopSelector line 48
  8. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_localMultiplicity line 52
  9. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_spectrum line 66
  10. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_alt_spectrum line 82
  11. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_active_separation line 103
  12. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_topGeometry line 117

    Source documentation

    The center estimate is expressed in the new top's physical shear coordinates. Restricting to the reference cone does not enlarge it.

    theorem assignedTopReference_topGeometry
    (oldSlope R cone w F : ℝ) (hw : 0 < w) (hcone : 0 ≤ cone) (hF : 0 ≤ F)
    (hwide : cone*w ≤ P.width) (hfrequency : ∀ k, |P.frequency k| ≤ F/w)
    (T : SlopeBox) (K : ℝ) (D : ℕ)
    (hlength : P.topLength ≤ K*T.length) (hwidth : P.width ≤ K*T.width)
    (horder : 3+2*(8*D+1) ≤ P.order) (hscale : P.scale = 4*(K*T.width))
    (hX : ∀ q ∈ packets, assigned q = top →
      |P.actualX q.1 q.2.1 q.2.2-T.x|+P.length q.1 ≤ K*T.length)
    (hZ : ∀ q ∈ packets, assigned q = top →
      |P.actualZ q.1 q.2.1 q.2.2+(oldSlope-T.slope)*P.actualX q.1 q.2.1 q.2.2-
        (T.y-T.slope*T.x)|+P.width ≤ K*T.width) :
    SourceLabeledTopGeometry
…

    Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SourceLabeledTopGeometry

  13. def OAI.LipschitzHilbert.PacketLatticeData.assignedTopReferenceLabel line 155

    Source documentation

    The reference label still points to its unique original label.

    def assignedTopReferenceLabel (j : Fin N) (l : (Q).labels j) : P.labels j :=
…
  14. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_condition line 158
  15. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_absoluteConstant line 162
  16. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_physical_center line 164
  17. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_localMultiplicity line 169
  18. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_selector_support line 178
  19. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_spectrum line 189
  20. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_alt_spectrum line 202
  21. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_active_separation line 236
  22. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_physicalMultiplierCoefficient line 253