Tests, Derivations, Proofs

Triangular Matrix Inverse


rinv←{
  1=n←≢⍵:÷⍵
  m←⌈n÷2
  AI← ∇ A←(m,m)↑⍵
  DI← ∇ D←(m,m)↓⍵
  B ← (m,m-n)↑⍵
  BX← - AI x B x DI
  (AI,BX)⍪((⌊n÷2),-n)↑DI
}

x ← +.×





┌────┬────┐     ┌────┬────┐     ┌────┬────┐
│    │    │     │    │    │     │    │    │
│ I0 │ 0  │     │ A  │ B  │     │ AI │ BX │
│    │    │     │    │    │     │    │    │
├────┼────┤  =  ├────┼────┤  x  ├────┼────┤
│    │    │     │    │    │     │    │    │
│ 0  │ I1 │     │ 0  │ D  │     │ 0  │ DI │
│    │    │     │    │    │     │    │    │
└────┴────┘     └────┴────┘     └────┴────┘

`I0 = (A x AI) + (B x 0 )`		induction; 0 matrix
`0 = (A x BX) + (B x DI)`		see below
`0 = (0 x AI) + (D x 0 )`		0 matrix
`I1 = (0 x BX) + (D x DI)`		induction; 0 matrix

`(A x BX) + (B x DI)`
`(A x (- AI x B x DI)) + (B x DI)`		substituting for `BX`
`((A x AI) x - B x DI) + (B x DI)`		associativity
`(I x - B x DI) + (B x DI)`		induction
`(- B x DI) + (B x DI)`		identity matrix
`0`		matrix addition/subtraction