OAI/NumberTheory/TwoPoint/Bounds/ShiftMatrixWords.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Expand finite shift matrices using step labels, without enumerating intermediate sites.

  1. def OAI.TwoPointCorrelations.shiftMatrix line 14
  2. def OAI.TwoPointCorrelations.retainedShiftWeight line 19
  3. lemma OAI.TwoPointCorrelations.retainedShiftWeight_nonzero line 25
  4. def OAI.TwoPointCorrelations.shiftWordEnd line 35
  5. def OAI.TwoPointCorrelations.shiftWordWeight line 39
  6. def OAI.TwoPointCorrelations.shiftWordTerm line 45
  7. lemma OAI.TwoPointCorrelations.sum_at_injective_site line 51
  8. lemma OAI.TwoPointCorrelations.shiftMatrix_action line 64
  9. lemma OAI.TwoPointCorrelations.shiftWordTerm_cons line 84
  10. theorem OAI.TwoPointCorrelations.shiftMatrix_pow_words line 95

    Source documentation

    Only the initial site and the step labels are summed. Intermediate sites are forced by the integer shifts and killed when they leave the finite domain.

    theorem shiftMatrix_pow_words (embed : V → S) (hinj : Function.Injective embed)
    (next : E → S → S) (weight : E → S → ℝ) (k : ℕ) (i j : V) :
    (shiftMatrix embed next weight ^ k) i j =
      ∑ w : Fin k → E, shiftWordTerm embed next weight (embed i) (embed j) w := by
…

    Mentions: OAI.TwoPointCorrelations.shiftMatrix, OAI.TwoPointCorrelations.shiftWordTerm

  11. theorem OAI.TwoPointCorrelations.shiftMatrix_power_closed_words line 113
  12. lemma OAI.TwoPointCorrelations.shiftWordWeight_support line 128
  13. lemma OAI.TwoPointCorrelations.sum_shiftWordTerm_pair line 145

    Source documentation

    The common endpoint is forced by the first word, and hence contributes no additional factor equal to the number of sites.

    lemma sum_shiftWordTerm_pair (embed : V → S) (hinj : Function.Injective embed)
    (next : E → S → S) (weight : E → S → ℝ) {k : ℕ} (i : V)
    (u v : Fin k → E) :
    (∑ j, shiftWordTerm embed next weight (embed i) (embed j) u *
      shiftWordTerm embed next weight (embed i) (embed j) v) =
      if shiftWordEnd next (embed i) u = shiftWordEnd next (embed i) v then
        shiftWordWeight embed next weight (embed i) u *
          shiftWordWeight embed next weight (embed i) v else 0 := by
…

    Mentions: OAI.TwoPointCorrelations.shiftWordTerm, OAI.TwoPointCorrelations.shiftWordEnd, OAI.TwoPointCorrelations.shiftWordWeight

  14. theorem OAI.TwoPointCorrelations.shiftMatrix_moment_forced_words line 180