OAI/Analysis/LipschitzHilbert/Trees/SourceOrdinarySizeStopping.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual finite signed size-selection loop. Test directions are chosen near the extremum; all tiles in the enlarged top are deleted.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.sizeDeletePackets line 15
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sizeTestPackets_subset_delete line 21
  3. inductive OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun line 31
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_size_stopping_run line 47
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.remaining_subset line 78
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.terminal_good line 85
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.length_le_card line 92