OAI/NumberTheory/TwoPoint/Walks/RetainedBlockIdentity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual projected block form is the sum of its ambient directed edges. The identity includes every vertex deletion, so overlapping blocks can be compared directly with a prefix of the retained correlation.

  1. lemma OAI.TwoPointCorrelations.sum_gated_edges line 16
  2. def OAI.TwoPointCorrelations.retainedPrimeEdge line 39
  3. lemma OAI.TwoPointCorrelations.retainedPrimeEdge_support line 51
  4. theorem OAI.TwoPointCorrelations.primeBlockCompression_retained_identity line 63
  5. theorem OAI.TwoPointCorrelations.primeBlockCompression_retained_blocks line 112