OAI/Analysis/LipschitzHilbert/Packets/PacketDataSelectedQuadratic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Linear summation of the per-top quadratic estimate, using the actual stopping threshold for each recorded top.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.selected_far_linear line 23
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.selected_gram_energy_of_quadratic line 41