OAI/Analysis/LipschitzHilbert/Geometry/SourceSelectionRecords.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Paired tops and their actual recorded test packets. Chronological nondeletion is a conclusion of the finite stopping run.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.sizeSelectionRecords line 16
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sizeSelectionRecords_packets line 24
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sizeSelectionRecords_tops line 33
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sizeSelectionRecords_subset line 41
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.records_geometry line 56
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.records_order line 76

    Source documentation

    A later recorded packet lies outside every earlier enlarged deletion box whenever its scale and angular cell make it eligible for deletion.

    theorem records_order
    (h : P.SizeStoppingRun negative w cb tau sigma epsilon A cell grid c initial tops remaining) :
    (P.sizeSelectionRecords negative w cb A cell grid initial tops).Pairwise
      (fun p p' => sizeDirection negative p.1.slope<sizeDirection negative p'.1.slope+epsilon ∧
        ∀ q∈p'.2, ¬(P.length q.1≤p.1.length ∧
          (P.actualX q.1 q.2.1 q.2.2,P.actualZ q.1 q.2.1 q.2.2)∈densitySpatialBox p.1 A ∧
          p.1.slope∈scaledAngularCell (w/P.topLength) grid q.1.val (cell q.1 q.2.1))) := by
…

    Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.sizeDirection, OAI.LipschitzHilbert.densitySpatialBox, OAI.LipschitzHilbert.scaledAngularCell