English
The inverse of a block-triangular matrix M is block-triangular with respect to the same partition.
Русский
Обратная матрица блока-верхнетреугольной M сохраняет блочное разбиение индексов.
LaTeX
$$$M^{-1} \text{ is block-triangular with respect to } b$$$
Lean4
/-- A lower-left subblock of the inverse of a block-triangular matrix is zero. This is a first step
towards `BlockTriangular.inv_toBlock` below. -/
theorem toBlock_inverse_eq_zero [LinearOrder α] [Invertible M] (hM : BlockTriangular M b) (k : α) :
(M⁻¹.toBlock (fun i => k ≤ b i) fun i => b i < k) = 0 :=
by
let p i := b i < k
let q i := ¬b i < k
have h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0 :=
by
rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_disjoint]
rw [disjoint_iff_inf_le]
exact fun i h => h.1 h.2
have h_zero : M.toBlock q p = 0 := by
ext i j
simpa using hM (lt_of_lt_of_le j.2 <| le_of_not_gt i.2)
have h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0 := by simpa [h_zero] using h_sum
haveI : Invertible (M.toBlock p p) := hM.invertibleToBlock k
have : (fun i => k ≤ b i) = q := by
ext
exact not_lt.symm
rw [this, ← Matrix.zero_mul (M.toBlock p p)⁻¹, ← h_mul_eq_zero, mul_inv_cancel_right_of_invertible]
