OAI/NumberTheory/TwoPoint/Walks/ProhibitedWeightIndependence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The retained departure weight is independent of tuple-prime residue draws. Only the padding-prime residues enter its divisibility, density and cutoff data.

  1. lemma OAI.TwoPointCorrelations.squarefree_divisor_congr line 13
  2. lemma OAI.TwoPointCorrelations.paddingDensity_eq_of_prime_residues line 25
  3. lemma OAI.TwoPointCorrelations.retainedEdgeDeparture_eq_of_prime_residues line 37
  4. theorem OAI.TwoPointCorrelations.retained_word_eq_of_prime_residues line 64
  5. theorem OAI.TwoPointCorrelations.lifted_retained_word_independent_tuple line 82