The lower bound by the matrices U_d

periodic-mesh-calculations.tex: "For a finite graph with adjacency matrix M, define integer matrices U_0 = I, U_1 = M, U_{d+1} = M U_d - U_{d-1}. If U_0, …, U_N are entrywise nonnegative, then (dim_k e_i Π(Δ)_N e_j)_{ij} ≥ U_N. … If K(t) records the kernels of the leftmost maps, … (I - tM + t²I) H(t) = I + K(t), H(t) = (∑ U_d t^d)(I + K(t)). The coefficients of K are nonnegative."

We record the coefficientwise form: a sequence of vectors h_d with κ_d = h_d - M h_{d-1} + h_{d-2} ≥ 0 satisfies h_N = ∑_{e ≤ N} U_{N-e} κ_e, hence h_N ≥ U_N h_0 when U_0, …, U_N ≥ 0.

def MultiplicativeBasisDeformations.UBound.U {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℤ) : ℕ → Matrix ι ι ℤ

U_0 = I, U_1 = M, U_{d+2} = M U_{d+1} - U_d.

def MultiplicativeBasisDeformations.UBound.κ {ι : Type u_1} [Fintype ι] (M : Matrix ι ι ℤ) (h : ℕ → ι → ℤ) : ℕ → ι → ℤ

The defects κ_d = h_d - M h_{d-1} + h_{d-2}.

def MultiplicativeBasisDeformations.UBound.S {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℤ) (h : ℕ → ι → ℤ) (N : ℕ) : ι → ℤ

S_N = ∑_{e ≤ N} U_{N-e} κ_e.

theorem MultiplicativeBasisDeformations.UBound.S_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℤ) (h : ℕ → ι → ℤ) (N : ℕ) : S M h N = h N

theorem MultiplicativeBasisDeformations.UBound.mulVec_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι ℤ} (hA : ∀ (i j : ι), 0 ≤ A i j) {v : ι → ℤ} (hv : ∀ (i : ι), 0 ≤ v i) (i : ι) : 0 ≤ A.mulVec v i

theorem MultiplicativeBasisDeformations.UBound.le_of_U {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℤ) (h : ℕ → ι → ℤ) (j : ι) (N : ℕ) (hU : ∀ d ≤ N, ∀ (a b : ι), 0 ≤ U M d a b) (hκ : ∀ (d : ℕ), 1 ≤ d → d ≤ N → ∀ (i : ι), 0 ≤ κ M h d i) (h0 : ∀ (i : ι), (if i = j then 1 else 0) ≤ h 0 i) (i : ι) : U M N i j ≤ h N i

The U bound.