English
For a block-triangular matrix M and any k in the index, the sum of the products of the corresponding blocks of M^{-1} and M equals the identity block, yielding a block-level decomposition of I.
Русский
Для блочно-верхнетреугольной матрицы M и любого k сумма произведений соответствующих блоков M^{-1} и M равна единичному блоку, что даёт блочное разложение единицы.
LaTeX
$$$\big(M^{-1}_{pp}\,M_{pp}\big) + \big(M^{-1}_{p\lnot p}\,M_{\lnot p p}\big) = I$$$
Lean4
theorem toBlock_inverse_mul_toBlock_eq_one [LinearOrder α] [Invertible M] (hM : BlockTriangular M b) (k : α) :
((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1 :=
by
let p i := b i < k
have h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 1 := by
rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
have h_zero : M.toBlock (fun i => ¬p i) p = 0 := by
ext i j
simpa using hM (lt_of_lt_of_le j.2 (le_of_not_gt i.2))
simpa [h_zero] using h_sum
