OAI/Analysis/LipschitzHilbert/Packets/PacketDataRecordedEnergy.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.PacketLatticeData.SizeStoppingRun.recorded_energy_lower line 21
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.recorded_nonempty line 35
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.records_nodup line 46
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.selected_energy_eq_records line 57