OAI/NumberTheory/TwoPoint/Walks/BlockEdgeForm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite directed matrix form is the overlapping edge-block sum used in the prefix comparison, with no residual multiplicity assumption.

  1. theorem OAI.TwoPointCorrelations.directed_block_form_eq line 13
  2. theorem OAI.TwoPointCorrelations.directed_block_form_prefix_error line 41