Nonbacktracking.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Algebraic resolvent transfer for a nonbacktracking operator

This is the kernel argument in manuscript Lemma q:noncommuting. Each edge operator has its own resolvent; distinct edge operators are never commuted. The positivity and norm steps are separate from this algebraic transfer.

def OAI.TwoPointCorrelations.nonbacktracking line 27
Source documentation
The copy indexed by i receives all transitions except the one with the same index.
```
def nonbacktracking (B : ι → E →ₗ[ℂ] E) : (ι → E) →ₗ[ℂ] (ι → E) where
…
```

theorem OAI.TwoPointCorrelations.resolvent_transfer_injective line 38

Source documentation

R i is the inverse of 1 + u B i. These are the only inverse identities needed to transfer injectivity.

theorem resolvent_transfer_injective (B : ι → E →ₗ[ℂ] E) (u : ℂ)
    (R : ι → E →ₗ[ℂ] E)
    (hR : ∀ i v, R i v + u • B i (R i v) = v)
    (hinj : Function.Injective (fun z : ι → E => z - u • nonbacktracking B z)) :
    Function.Injective (fun v : E => v - ∑ i, u • B i (R i v)) := by
…

Mentions: OAI.TwoPointCorrelations.nonbacktracking