OAI/NumberTheory/TwoPoint/Walks/TupleRankFiberSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sum the actual high-rank column while retaining reciprocal weights outside it.

  1. theorem OAI.TwoPointCorrelations.same_column_patterns_high_rank_sum line 13