The binomial size family e_d = q_d⁻¹

Corollary 7.10(a): q_d = w⁻¹ + Σ_{i<d} yⁱ u⁻¹ y⁻ⁱ and e_d = q_d⁻¹. With Δ = diag(w, y u y⁻¹, …, y^{d−1} u y^{−(d−1)}) and J the all-ones matrix, H = Δ + u J and L = H · diag(1, y, …, y^{d−1}). Over a division ring D (no commutativity) unless stated.

Main results

• rankOne_mul_inv, rankOneInv_mul (rank one): for Δ i ≠ 0, u ≠ 0 and q = u⁻¹ + Σ_i (Δ i)⁻¹ ≠ 0, H = diagonal Δ + u J has the two-sided inverse Hinv i j = δ_ij (Δ i)⁻¹ − (Δ i)⁻¹ q⁻¹ (Δ j)⁻¹. Both are the Woodbury identities Matrix.add_mul_mul_invOf_mul_eq_one and Matrix.add_mul_mul_invOf_mul_eq_one' (over a ring) with A = diagonal Δ, U a column of ones, C = [u], V a row of ones, so that ⅟C + V ⅟A U = q.
• rankOne_isUnit; inv_q_eq : q⁻¹ = u − u (Σ_{i,j} Hinv i j) u.
• conj_add_mul_pow (conjugation): (yⁱ u y⁻ⁱ + u) yⁱ = yⁱ u + u yⁱ, so L has entries linear in u, w, y.
• det_scalar_point (scalar point, commutative ring): det (diag(0, 1, …, 1) + J) = 1, via the Weinstein–Aronszajn identity Matrix.det_one_add_mul_comm with a rank-two factorization.
• idemBlock_isUnit (idempotent point, field): at U = 1 − E₀₀ (idemU_eq), W = 1 and Y the cyclic shift Y_{ab} = [a = b + 1] (cycShift_pow_apply: (Yᵏ)_{ab} = [a = b + k]), the block matrix with block (i, j) = U Yʲ + δ_ij (if i = 0 then W else Yⁱ U) is invertible for every size d = n + 1 ≥ 1. Proof: idemBlock_eq computes the entries, mulVec has trivial kernel.

Related

PhiCompression.phi_inv_woodbury is a scalar reading of the same Woodbury identity; ParabolicFamily has det (1 + J) = n + 1 via Matrix.det_one_add_replicateCol_mul_replicateRow.

Rank one: explicit inverse of diagonal Δ + u J

def ThreeAxes.BinomialSizeFamily.qSum {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] (Δ : ι → D) (u : D) : D

q = u⁻¹ + Σ_i (Δ i)⁻¹.

Equations

• ThreeAxes.BinomialSizeFamily.qSum Δ u = u⁻¹ + ∑ i : ι, (Δ i)⁻¹

def ThreeAxes.BinomialSizeFamily.rankOne {D : Type u_1} [DivisionRing D] {ι : Type u_2} [DecidableEq ι] (Δ : ι → D) (u : D) : Matrix ι ι D

H = diagonal Δ + u J.

Equations

• ThreeAxes.BinomialSizeFamily.rankOne Δ u = Matrix.diagonal Δ + Matrix.of fun (x x_1 : ι) => u

def ThreeAxes.BinomialSizeFamily.rankOneInv {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Δ : ι → D) (u : D) : Matrix ι ι D

The explicit inverse Hinv i j = δ_ij (Δ i)⁻¹ − (Δ i)⁻¹ q⁻¹ (Δ j)⁻¹.

Equations

• ThreeAxes.BinomialSizeFamily.rankOneInv Δ u = Matrix.of fun (i j : ι) => (if i = j then (Δ i)⁻¹ else 0) - (Δ i)⁻¹ * (ThreeAxes.BinomialSizeFamily.qSum Δ u)⁻¹ * (Δ j)⁻¹

theorem ThreeAxes.BinomialSizeFamily.rankOne_mul_inv {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Δ : ι → D) (u : D) (hΔ : ∀ (i : ι), Δ i ≠ 0) (hu : u ≠ 0) (hq : qSum Δ u ≠ 0) : rankOne Δ u * rankOneInv Δ u = 1

H * Hinv = 1: Mathlib's Matrix.add_mul_mul_invOf_mul_eq_one (Woodbury).

theorem ThreeAxes.BinomialSizeFamily.rankOneInv_mul {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Δ : ι → D) (u : D) (hΔ : ∀ (i : ι), Δ i ≠ 0) (hu : u ≠ 0) (hq : qSum Δ u ≠ 0) : rankOneInv Δ u * rankOne Δ u = 1

Hinv * H = 1: Mathlib's Matrix.add_mul_mul_invOf_mul_eq_one' (Woodbury).

theorem ThreeAxes.BinomialSizeFamily.rankOne_isUnit {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Δ : ι → D) (u : D) (hΔ : ∀ (i : ι), Δ i ≠ 0) (hu : u ≠ 0) (hq : qSum Δ u ≠ 0) : IsUnit (rankOne Δ u)

theorem ThreeAxes.BinomialSizeFamily.inv_q_eq {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Δ : ι → D) (u : D) (hu : u ≠ 0) (hq : qSum Δ u ≠ 0) : (qSum Δ u)⁻¹ = u - (u * ∑ i : ι, ∑ j : ι, rankOneInv Δ u i j) * u

q⁻¹ = u − u (Σ_{i,j} Hinv i j) u: e_d is a linear read-out of the inverse of H.

Conjugation

theorem ThreeAxes.BinomialSizeFamily.conj_add_mul_pow {D : Type u_1} [DivisionRing D] (y u : D) (hy : y ≠ 0) (i : ℕ) : (y ^ i * u * y⁻¹ ^ i + u) * y ^ i = y ^ i * u + u * y ^ i

(yⁱ u y⁻ⁱ + u) yⁱ = yⁱ u + u yⁱ: the columns of L = H · diag(1, y, …, y^{d−1}).

Scalar point

theorem ThreeAxes.BinomialSizeFamily.det_scalar_point {R : Type u_1} [CommRing R] (n : ℕ) : ((Matrix.diagonal fun (i : Fin (n + 1)) => if i = 0 then 0 else 1) + Matrix.of fun (x x_1 : Fin (n + 1)) => 1).det = 1

At the scalar point det (diag(0, 1, …, 1) + J) = 1, over any commutative ring.

Idempotent point

def ThreeAxes.BinomialSizeFamily.cycShift {K : Type u_1} [Field K] (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) K

The cyclic shift Y on K^{n+1}: Y_{ab} = [a = b + 1].

Equations

• ThreeAxes.BinomialSizeFamily.cycShift n = Matrix.of fun (a b : Fin (n + 1)) => if a = b + 1 then 1 else 0

def ThreeAxes.BinomialSizeFamily.idemU {K : Type u_1} [Field K] (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) K

U = 1 − E₀₀ (idemU_eq).

Equations

• ThreeAxes.BinomialSizeFamily.idemU n = Matrix.of fun (a b : Fin (n + 1)) => if a = b ∧ a ≠ 0 then 1 else 0

theorem ThreeAxes.BinomialSizeFamily.idemU_eq {K : Type u_1} [Field K] (n : ℕ) : idemU n = 1 - Matrix.single 0 0 1

theorem ThreeAxes.BinomialSizeFamily.cycShift_pow_apply {K : Type u_1} [Field K] (n k : ℕ) (a b : Fin (n + 1)) : (cycShift n ^ k) a b = if a = b + ↑k then 1 else 0

def ThreeAxes.BinomialSizeFamily.idemBlock {K : Type u_1} [Field K] (n : ℕ) : Matrix (Fin (n + 1) × Fin (n + 1)) (Fin (n + 1) × Fin (n + 1)) K

The (n+1) × (n+1) block matrix with block (i, j) equal to U Yʲ + δ_ij (if i = 0 then W else Yⁱ U), at W = 1, U = 1 − E₀₀, Y the cyclic shift.

Equations

• One or more equations did not get rendered due to their size.

def ThreeAxes.BinomialSizeFamily.idemBlockEntries {K : Type u_1} [Field K] (n : ℕ) : Matrix (Fin (n + 1) × Fin (n + 1)) (Fin (n + 1) × Fin (n + 1)) K

The entries of idemBlock.

Equations

• One or more equations did not get rendered due to their size.

theorem ThreeAxes.BinomialSizeFamily.idemBlock_eq {K : Type u_1} [Field K] (n : ℕ) : idemBlock n = idemBlockEntries n

theorem ThreeAxes.BinomialSizeFamily.idemBlockEntries_mulVec {K : Type u_1} [Field K] (n : ℕ) (v : Fin (n + 1) × Fin (n + 1) → K) (i a : Fin (n + 1)) : (idemBlockEntries n).mulVec v (i, a) = (if a ≠ 0 then ∑ j : Fin (n + 1), v (j, a - j) else 0) + if i = 0 then v (0, a) else if a ≠ i then v (i, a - i) else 0

theorem ThreeAxes.BinomialSizeFamily.idemBlock_isUnit {K : Type u_1} [Field K] (n : ℕ) : IsUnit (idemBlock n)

The block matrix at the idempotent point is invertible for every size n + 1 ≥ 1 (trivial kernel).