OAI/Analysis/LipschitzHilbert/Geometry/SourceTwoSidedSizeSelection.lean

GitHub source file

4 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. def OAI.LipschitzHilbert.SourceLabeledLattice.unsignedSizeTestEnergy line 17
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.signed_indicator_bound line 26
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.unsignedSizeTestEnergy_le line 38
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_two_sided_size_selection line 56