OAI/Analysis/LipschitzHilbert/Trees/SourceAssignedTopSelector.lean

GitHub source file

24 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.SourceLabeledLattice.assignedTopLabel_first line 21
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopLabel line 25
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopLabel_injective line 28
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopItem_mem line 35
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopItem_assignment line 40
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_absoluteConstant line 46
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_raw line 49
  8. def OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopSelector line 55
  9. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_localMultiplicity line 59
  10. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_topGeometry line 73
  11. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_spectrum line 92
  12. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_alt_spectrum line 108
  13. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_active_separation line 129
  14. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_topGeometry line 143

    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

  15. def OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReferenceLabel line 181

    Source documentation

    The reference label still points to its unique original label.

    def assignedTopReferenceLabel (j : Fin N) (l : (Q).labels j) : P.labels j :=
…
  16. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_condition line 184
  17. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_absoluteConstant line 188
  18. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_physical_center line 190
  19. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_localMultiplicity line 195
  20. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_selector_support line 204
  21. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_spectrum line 215
  22. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_alt_spectrum line 228
  23. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_active_separation line 262
  24. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_physicalMultiplierCoefficient line 279