OAI/NumberTheory/TwoPoint/Walks/ProhibitedWeightSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positivity, crude size and retained divisibility of the actual departure weights.

  1. lemma OAI.TwoPointCorrelations.retainedEdgeDeparture_le_crude line 13
  2. theorem OAI.TwoPointCorrelations.retained_word_le_crude line 25
  3. theorem OAI.TwoPointCorrelations.retained_word_padding_divisibility line 40
  4. theorem OAI.TwoPointCorrelations.lifted_retained_word_padding_tests line 57