OAI/Analysis/LipschitzHilbert/Phase/SourceSignedAngularGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Angular margins discharge the direction hypotheses of signed selected-box separation, for both passes of the stopping procedure.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.selected_top_direction_bound_signed line 18
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.selected_boxes_disjoint_of_margin_signed line 36

    Source documentation

    The geometric separation now needs only the packet-cell margins and the two packet slope bounds; it does not assume the later top's direction.

    theorem selected_boxes_disjoint_of_margin_signed
    (h : P.SizeStoppingRun negative w cb tau sigma epsilon A cell grid c initial tops remaining)
    (hw : 0<w) (hwW : w≤P.width) (hcb : 0<cb)
    (t K CZero : ℝ) (hK : 0≤K) (hCZero : 0<CZero)
    (hconstants : (1+cb/4)/CZero≤cb/4)
    (hA : 2*K*(1+(1+cb/4))+1/2≤A)
    (p p' : SlopeBox × Finset P.PacketIndex)
    (hp : p∈P.sizeSelectionRecords negative w cb A cell grid initial tops)
    (hp' : p'∈P.sizeSelectionRecords negative w cb A cell grid initial tops)
    (q q' : P.PacketIndex) (hq : q∈p.2) (hq' : q'∈p'.2)
    (hlen : P.length q.1≤P.length q'.1)
    (hfar : CZero*P.length q.1≤P.length q'.1)
…

    Mentions: OAI.LipschitzHilbert.SlopeBox