MatrixClosedWords.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Signed closed-word expansion of the actual matrix power moment.

def OAI.TwoPointCorrelations.matrixPathWeight line 20
def OAI.TwoPointCorrelations.matrixPathEnd line 24
def OAI.TwoPointCorrelations.matrixPathTerm line 28
def OAI.TwoPointCorrelations.matrixPathVertices line 31
lemma OAI.TwoPointCorrelations.matrixPathEnd_eq_last line 34
lemma OAI.TwoPointCorrelations.matrixPathTerm_ne_zero line 44
lemma OAI.TwoPointCorrelations.matrixPathWeight_chain line 53
lemma OAI.TwoPointCorrelations.sum_fin_cons line 67
lemma OAI.TwoPointCorrelations.matrixPathTerm_cons line 74
theorem OAI.TwoPointCorrelations.matrix_pow_path_sum line 80
Source documentation
Every power entry is an exact signed sum over its successive states.
```
theorem matrix_pow_path_sum (A : Matrix V V ℝ) (k : ℕ) (x y : V) :
    (A ^ k) x y = ∑ v : Fin k → V, matrixPathTerm A x y v := by
…
```
Mentions: OAI.TwoPointCorrelations.matrixPathTerm
def OAI.TwoPointCorrelations.matrixFrobeniusSq line 90
lemma OAI.TwoPointCorrelations.matrixFrobeniusSq_nonneg line 93
theorem OAI.TwoPointCorrelations.matrix_power_closed_words line 98
Source documentation
Squaring joins two paths with the same endpoints. No absolute values are taken in this identity, which is the step needed before centering.
```
theorem matrix_power_closed_words (A : Matrix V V ℝ) (k : ℕ) :
    matrixFrobeniusSq (A ^ k) =
      ∑ x, ∑ y, ∑ u : Fin k → V, ∑ v : Fin k → V,
        matrixPathTerm A x y u * matrixPathTerm A x y v := by
…
```
Mentions: OAI.TwoPointCorrelations.matrixFrobeniusSq, OAI.TwoPointCorrelations.matrixPathTerm
theorem OAI.TwoPointCorrelations.average_matrix_power_le_closed_words line 112
Source documentation
Move the finite-law average through the full signed expansion. The triangle inequality is applied to each word expectation only afterwards.
```
theorem average_matrix_power_le_closed_words {Ω : Type*} [Fintype Ω]
    (μ : FiniteLaw Ω) (A : Ω → Matrix V V ℝ) (k : ℕ) :
    μ.average (fun ω => matrixFrobeniusSq (A ω ^ k)) ≤
      ∑ x, ∑ y, ∑ u : Fin k → V, ∑ v : Fin k → V,
        |μ.average (fun ω => matrixPathTerm (A ω) x y u * matrixPathTerm (A ω) x y v)| := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.matrixFrobeniusSq, OAI.TwoPointCorrelations.matrixPathTerm
def OAI.TwoPointCorrelations.blockNonbacktrackingMatrix line 143
Source documentation
The manuscript's concrete block matrix H[d,d'] = 1[d≠d'] A[d'].
```
def blockNonbacktrackingMatrix (A : D → Matrix V V ℝ) : Matrix (D × V) (D × V) ℝ :=
…
```
lemma OAI.TwoPointCorrelations.blockNonbacktrackingMatrix_ne_zero line 146
lemma OAI.TwoPointCorrelations.block_path_copy_chain line 156

theorem OAI.TwoPointCorrelations.closed_copy_halves_chain line 168

Source documentation

The two halves of a nonzero closed-word term are nonbacktracking. There is deliberately no condition across the two joins.

theorem closed_copy_halves_chain (A : D → Matrix V V ℝ) {k : ℕ}
    (x y : D × V) (u v : Fin k → D × V)
    (hu : matrixPathTerm (blockNonbacktrackingMatrix A) x y u ≠ 0)
    (hv : matrixPathTerm (blockNonbacktrackingMatrix A) x y v ≠ 0) :
    ((List.ofFn u).map Prod.fst).IsChain (fun a b => a ≠ b) ∧
      (((List.ofFn v).map Prod.fst).reverse).IsChain (fun a b => a ≠ b) := by
…

Mentions: OAI.TwoPointCorrelations.matrixPathTerm, OAI.TwoPointCorrelations.blockNonbacktrackingMatrix