OAI/NumberTheory/TwoPoint/Walks/RetainedLiouvilleEdges.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A literal retained edge coefficient after testing. The vertex masks are ambient predicates, so the coefficient is independent of the block.

  1. def OAI.TwoPointCorrelations.retainedLiouvilleScalar line 12
  2. def OAI.TwoPointCorrelations.retainedLiouvilleEdge line 15
  3. lemma OAI.TwoPointCorrelations.retainedLiouvilleScalar_star line 23
  4. theorem OAI.TwoPointCorrelations.retainedLiouvilleEdge_test line 28