OAI/NumberTheory/TwoPoint/Bounds/ActualWordStateIdentity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact evaluation of the coefficient table on the integer sites of a word, including both endpoints of every retained departure.

  1. def OAI.TwoPointCorrelations.wordVertexSite line 13
  2. lemma OAI.TwoPointCorrelations.wordVertexSite_step line 17
  3. lemma OAI.TwoPointCorrelations.retainedWord_eq_state_product line 29
  4. def OAI.TwoPointCorrelations.wordCenteredBits line 48
  5. lemma OAI.TwoPointCorrelations.wordCenteredBits_apply line 54
  6. lemma OAI.TwoPointCorrelations.centeredWord_eq_state_bits line 63
  7. lemma OAI.TwoPointCorrelations.actualWordCoefficient_integer_identity line 81