Compression of φ_r over a division ring

For d : ι → K with every d i ≠ 0, α ω : ι → K and d₂ ≠ 0, w, let φ = Σ_i α_i d_i⁻¹ ω_i + w d₂⁻¹ (in the paper φ_r = Σ_τ α_τ d_τ⁻¹ ω_τ + α₂ d₂⁻¹ ω₂ with ω₂ = 1, α₂ = w). Over an arbitrary division ring K (no commutativity):

Main results

• fromBlocks_schur_mul, fromBlocks_schur_mul': two-sided block inverse of fromBlocks A B C (S + C A⁻¹ B) from two-sided inverses of the pivot A and of the Schur complement S, over any ring.
• phiMatrix, phiMatrixInv (Remark 8.2): M = [[diag d, −ω d₂], [α, w]] and its explicit inverse; the Schur complement of diag d is φ d₂ (phiMatrix_schur). phiMatrix_mul_inv, phiMatrixInv_mul: both products are 1; phiMatrix_isUnit; phi_inv_eq_corner: φ⁻¹ = d₂ (M⁻¹)_{∞∞}.
• phi_inv_woodbury (Remark 8.2, second compression): for S = diag d + ω (d₂ w⁻¹) α and a right inverse T of S, φ⁻¹ = c − c (α T ω) c with c = d₂ w⁻¹.
• inv_mul_conj (Corollary 7.10(c)): m₀ ℓ⁻¹ m₁ = (m₀ ℓ m₀⁻¹)⁻¹ (m₀ m₁).
• harmonic_compression_inv (Remark 7.11(iii)): the case r = 0 of InverseIdentities.compression_inv.

Matrix inverses are given explicitly and checked on both sides; Matrix.inv needs a commutative ring.

Related

Over a commutative ring the block inverse is Mathlib's Matrix.invOf_fromBlocks₁₁_eq (with Invertible instances), and phi_inv_woodbury is a scalar reading of the Woodbury identity Matrix.invOf_add_mul_mul' (over a ring, with Invertible instances).

Two-sided block inverse with pivot in the upper-left block

theorem ThreeAxes.PhiCompression.fromBlocks_schur_mul {R : Type u_1} [Ring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A Ai : Matrix m m R) (B : Matrix m n R) (C : Matrix n m R) (S Si : Matrix n n R) (hA : A * Ai = 1) (hS : S * Si = 1) : Matrix.fromBlocks A B C (S + C * Ai * B) * Matrix.fromBlocks (Ai + Ai * B * Si * C * Ai) (-(Ai * B * Si)) (-(Si * C * Ai)) Si = 1

Block inverse of fromBlocks A B C (S + C A⁻¹ B), right product, over any ring.

theorem ThreeAxes.PhiCompression.fromBlocks_schur_mul' {R : Type u_1} [Ring R] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A Ai : Matrix m m R) (B : Matrix m n R) (C : Matrix n m R) (S Si : Matrix n n R) (hA : Ai * A = 1) (hS : Si * S = 1) : Matrix.fromBlocks (Ai + Ai * B * Si * C * Ai) (-(Ai * B * Si)) (-(Si * C * Ai)) Si * Matrix.fromBlocks A B C (S + C * Ai * B) = 1

Block inverse of fromBlocks A B C (S + C A⁻¹ B), left product, over any ring.

Remark 8.2: first compression

def ThreeAxes.PhiCompression.phi {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Fintype ι] (d α ω : ι → K) (d₂ w : K) : K

φ = Σ_i α_i d_i⁻¹ ω_i + w d₂⁻¹.

Equations

• ThreeAxes.PhiCompression.phi d α ω d₂ w = ∑ i : ι, α i * (d i)⁻¹ * ω i + w * d₂⁻¹

def ThreeAxes.PhiCompression.phiMatrix {K : Type u_1} [DivisionRing K] {ι : Type u_2} [DecidableEq ι] (d α ω : ι → K) (d₂ w : K) : Matrix (ι ⊕ Unit) (ι ⊕ Unit) K

M = [[diag d, −ω d₂], [α, w]], border indexed by Unit (Remark 8.2).

Equations

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

noncomputable def ThreeAxes.PhiCompression.phiMatrixInv {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → K) (d₂ w : K) : Matrix (ι ⊕ Unit) (ι ⊕ Unit) K

The explicit inverse of phiMatrix: block inverse through the Schur complement φ d₂ of diag d.

Equations

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

theorem ThreeAxes.PhiCompression.phiMatrix_schur {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → K) (d₂ w : K) (h₂ : d₂ ≠ 0) : (Matrix.of fun (x x_1 : Unit) => w) = (Matrix.of fun (x x_1 : Unit) => phi d α ω d₂ w * d₂) + ((Matrix.of fun (x : Unit) (j : ι) => α j) * Matrix.diagonal fun (i : ι) => (d i)⁻¹) * Matrix.of fun (i : ι) (x : Unit) => -(ω i * d₂)

The Schur complement of diag d in phiMatrix is φ d₂.

theorem ThreeAxes.PhiCompression.diagonal_mul_diagonal_inv {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d : ι → K) (hd : ∀ (i : ι), d i ≠ 0) : (Matrix.diagonal d * Matrix.diagonal fun (i : ι) => (d i)⁻¹) = 1

theorem ThreeAxes.PhiCompression.diagonal_inv_mul_diagonal {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d : ι → K) (hd : ∀ (i : ι), d i ≠ 0) : (Matrix.diagonal fun (i : ι) => (d i)⁻¹) * Matrix.diagonal d = 1

theorem ThreeAxes.PhiCompression.phiMatrix_mul_inv {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → K) (d₂ w : K) (hd : ∀ (i : ι), d i ≠ 0) (h₂ : d₂ ≠ 0) (hφ : phi d α ω d₂ w ≠ 0) : phiMatrix d α ω d₂ w * phiMatrixInv d α ω d₂ w = 1

theorem ThreeAxes.PhiCompression.phiMatrixInv_mul {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → K) (d₂ w : K) (hd : ∀ (i : ι), d i ≠ 0) (h₂ : d₂ ≠ 0) (hφ : phi d α ω d₂ w ≠ 0) : phiMatrixInv d α ω d₂ w * phiMatrix d α ω d₂ w = 1

theorem ThreeAxes.PhiCompression.phiMatrix_isUnit {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → K) (d₂ w : K) (hd : ∀ (i : ι), d i ≠ 0) (h₂ : d₂ ≠ 0) (hφ : phi d α ω d₂ w ≠ 0) : IsUnit (phiMatrix d α ω d₂ w)

theorem ThreeAxes.PhiCompression.phiMatrixInv_corner {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → K) (d₂ w : K) : phiMatrixInv d α ω d₂ w (Sum.inr ()) (Sum.inr ()) = d₂⁻¹ * (phi d α ω d₂ w)⁻¹

The border corner of phiMatrixInv is d₂⁻¹ φ⁻¹.

theorem ThreeAxes.PhiCompression.phi_inv_eq_corner {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → K) (d₂ w : K) (hd : ∀ (i : ι), d i ≠ 0) (h₂ : d₂ ≠ 0) (hφ : phi d α ω d₂ w ≠ 0) : ∃ (N : Matrix (ι ⊕ Unit) (ι ⊕ Unit) K), phiMatrix d α ω d₂ w * N = 1 ∧ N * phiMatrix d α ω d₂ w = 1 ∧ N (Sum.inr ()) (Sum.inr ()) = d₂⁻¹ * (phi d α ω d₂ w)⁻¹ ∧ (phi d α ω d₂ w)⁻¹ = d₂ * N (Sum.inr ()) (Sum.inr ())

Remark 8.2. If φ = Σ_i α_i d_i⁻¹ ω_i + w d₂⁻¹ ≠ 0, then M = [[diag d, −ω d₂], [α, w]] has a two-sided inverse N, and φ⁻¹ = d₂ N_{∞∞}.

Remark 8.2: second compression (Woodbury)

theorem ThreeAxes.PhiCompression.phi_inv_woodbury {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → K) (d₂ w : K) (hd : ∀ (i : ι), d i ≠ 0) (h₂ : d₂ ≠ 0) (hw : w ≠ 0) (T : Matrix ι ι K) (hST : (Matrix.diagonal d + Matrix.of fun (i j : ι) => ω i * d₂ * w⁻¹ * α j) * T = 1) : (phi d α ω d₂ w)⁻¹ = d₂ * w⁻¹ - (d₂ * w⁻¹ * ∑ i : ι, ∑ j : ι, α i * T i j * ω j) * d₂ * w⁻¹

Remark 8.2, second compression. With c = d₂ w⁻¹ and S = diag d + ω c α (S_ij = d_i δ_ij + ω_i d₂ w⁻¹ α_j), if S T = 1 then φ⁻¹ = c − c (Σ_{i,j} α_i T_ij ω_j) c. No hypothesis φ ≠ 0 is needed: it follows from S T = 1.

Corollary 7.10(c)

theorem ThreeAxes.PhiCompression.inv_mul_conj {K : Type u_1} [DivisionRing K] (m₀ ℓ m₁ : K) (h₀ : m₀ ≠ 0) : m₀ * ℓ⁻¹ * m₁ = (m₀ * ℓ * m₀⁻¹)⁻¹ * (m₀ * m₁)

Corollary 7.10(c). m₀ ℓ⁻¹ m₁ = (m₀ ℓ m₀⁻¹)⁻¹ (m₀ m₁) for m₀ ≠ 0.

Remark 7.11(iii): the harmonic case r = 0

theorem ThreeAxes.PhiCompression.compressionMatrix_zero {K : Type u_1} [DivisionRing K] {ι : Type u_2} [DecidableEq ι] (d₁ d₂ : K) (d : ι → K) : InverseIdentities.compressionMatrix d₁ d₂ 0 d = Matrix.fromBlocks (Matrix.of fun (x x_1 : Fin 1) => d₁ + d₂) (Matrix.of fun (x : Fin 1) (x_1 : ι) => d₁) (Matrix.of fun (x : ι) (x_1 : Fin 1) => -d₂) (Matrix.diagonal d)

theorem ThreeAxes.PhiCompression.harmonic_compression_inv {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d₁ d₂ : K) (d : ι → K) (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) (hd : ∀ (i : ι), d i ≠ 0) (hf : d₁⁻¹ + d₂⁻¹ + ∑ i : ι, (d i)⁻¹ ≠ 0) [Invertible (InverseIdentities.compressionMatrix d₁ d₂ 0 d)] : d₂ * ⅟(InverseIdentities.compressionMatrix d₁ d₂ 0 d) (Sum.inl 0) (Sum.inl 0) * d₁ = (d₁⁻¹ + d₂⁻¹ + ∑ i : ι, (d i)⁻¹)⁻¹

Remark 7.11(iii). The case r = 0 of InverseIdentities.compression_inv: (d₁⁻¹ + d₂⁻¹ + Σ dᵢ⁻¹)⁻¹ = d₂ (M⁻¹)₁₁ d₁ for M = [[d₁ + d₂, d₁ 𝟙ᵀ], [−𝟙 d₂, diag d]] (compressionMatrix_zero).