OAI/NumberTheory/TwoPoint/Bounds/IntegerShiftWords.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.signedIntegerWeight line 14
2. lemma OAI.TwoPointCorrelations.forward_edge_as_shift line 24
3. lemma OAI.TwoPointCorrelations.backward_edge_as_shift line 42
4. lemma OAI.TwoPointCorrelations.signedIntegerWeight_nonzero line 61
5. lemma OAI.TwoPointCorrelations.integerEdgeMatrix_signed_shifts line 83
6. def OAI.TwoPointCorrelations.integerShiftNext line 100
7. def OAI.TwoPointCorrelations.integerShiftWeight line 104
8. theorem OAI.TwoPointCorrelations.block_integer_matrix_eq_shift line 116

   Source documentation

   The step index is the actual tuple label, padding divisor and sign. The finite state records the preceding tuple and the integer site.

   theorem block_integer_matrix_eq_shift
       (site : V → ℤ) (Q : Finset ℕ) (tuple : D → ℕ)
       (u : ℕ → ℝ) (eligible : D → ℕ → Prop) (g : ℤ → ℝ) (center : D → ℤ → ℝ)
       (L K : ℝ) (extra : D → ℤ → Prop) (h : ℕ) (gate : D → ℤ → ℤ → Prop) :
       blockNonbacktrackingMatrix (fun d i j =>
         if gate d (site i) (site j) then
           integerEdgeMatrix site Q u (eligible d) g (center d) L K (extra d) h (tuple d) i j
         else 0) =
       shiftMatrix (fun x : D × V => (x.1, site x.2)) (integerShiftNext Q tuple h)
         (integerShiftWeight Q tuple u eligible g center L K extra h gate) := by
   …

   Mentions: OAI.TwoPointCorrelations.blockNonbacktrackingMatrix, OAI.TwoPointCorrelations.integerEdgeMatrix, OAI.TwoPointCorrelations.shiftMatrix, OAI.TwoPointCorrelations.integerShiftNext, OAI.TwoPointCorrelations.integerShiftWeight