OAI/Analysis/CircleDomains/Selection/RealTestLevelData.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The selected real tests supply the actual level graphs and their square-summable incidence weights for the next positive-law application.

  1. def OAI.CircleDomainRigidity.realTestLevelData line 22
  2. def OAI.CircleDomainRigidity.realTestLevelData.previous line 32
  3. theorem OAI.CircleDomainRigidity.realTestLevelData.weight_finite line 35
  4. theorem OAI.CircleDomainRigidity.realTestLevelData.marked_weights line 44
  5. theorem OAI.CircleDomainRigidity.realTestLevelData.point_bound line 54
  6. theorem OAI.CircleDomainRigidity.realTestLevelData.unique_free_trace line 77
  7. theorem OAI.CircleDomainRigidity.realTestLevelData.level_relation line 106
  8. theorem OAI.CircleDomainRigidity.realTestLevelData.compatibility line 112
  9. theorem OAI.CircleDomainRigidity.OrderedLevelNullCompatibility.mono line 131