OAI/NumberTheory/TwoPoint/Bounds/ActualPaddingProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Identify recursive padding weights with the literal product at the numerical departures.

  1. theorem OAI.TwoPointCorrelations.paddingWordWeight_eq_prod_sites line 13
  2. lemma OAI.TwoPointCorrelations.wordDisplacement_take_succ line 40
  3. theorem OAI.TwoPointCorrelations.paddingWordWeight_eq_departure_product line 45
  4. theorem OAI.TwoPointCorrelations.retainedColumnPaddingWeight_eq_departure_product line 64