OAI/Analysis/LipschitzHilbert/Phase/PacketDataSelectionAngularGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.PacketLatticeData.angular_cell_distance line 15
2. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.selected_top_direction_bound line 34
3. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.selected_boxes_disjoint_of_margin line 52

   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
       (h : P.SizeStoppingRun false 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 false w cb A cell grid initial tops)
       (hp' : p'∈P.sizeSelectionRecords false 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