OAI/Analysis/LipschitzHilbert/Geometry/PacketDataTwoSidedSelection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Positive followed by negative selection leaves every separated size test below its threshold. Both runs retain their original geometry.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.signed_indicator_bound line 18
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.unsignedSizeTestEnergy_le line 30
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_two_sided_size_selection line 48