OAI/Analysis/LipschitzHilbert/Trees/SourceRecordedEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The strict stopping test gives a lower energy bound for every recorded top. This is the bound needed to sum its far-Gram estimate.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.recorded_energy_lower line 21
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.recorded_nonempty line 35
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.records_nodup line 46
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.selected_energy_eq_records line 57