OAI/Analysis/LipschitzHilbert/Packets/PacketDataDeletionForest.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The full trees removed by the size-selection loop, including the nonseparated packets deleted with each recorded top.

  1. def OAI.LipschitzHilbert.PacketLatticeData.sizeDeletionRecords line 16
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.sizeDeletionRecords_tops line 22
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.sizeDeletionRecords_subset line 29
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.sizeDeletionRecords_disjoint line 40
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.deletion_forest_covers line 61
  6. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.deletion_forest_nonempty line 74
  7. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.deletion_forest_geometry line 87
  8. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.deletion_forest_sum line 104
  9. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.deletion_forest_area line 121
  10. theorem OAI.LipschitzHilbert.PacketLatticeData.two_size_deletion_forest_sum line 131