OAI/Analysis/LipschitzHilbert/Packets/PacketDataSelectedArea.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Charge the actual selected top areas to the L2 norm of the test function, using the proved selected synthesis estimate.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.selected_top_area_bound line 18