OAI/NumberTheory/TwoPoint/Walks/RetainedActiveEdges.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Inactive tuple/padding pairs contribute zero. Giving them step zero lets the actual pair bound control every displacement in the block lemma.

  1. def OAI.TwoPointCorrelations.retainedPrimeStep line 15
  2. lemma OAI.TwoPointCorrelations.retainedPrimeEdge_inactive line 20
  3. lemma OAI.TwoPointCorrelations.retainedPrimeEdge_support_active line 29
  4. lemma OAI.TwoPointCorrelations.retainedPrimeStep_le line 41
  5. lemma OAI.TwoPointCorrelations.retainedPrimeEdge_active_step_eq line 54
  6. lemma OAI.TwoPointCorrelations.ambientLiouvilleBlockForm_active line 68
  7. lemma OAI.TwoPointCorrelations.canonicalTraceFamily_pair_eligible line 86