English
The inverse blocks satisfy specific equality relations with the original blocks under the partition.
Русский
Обратные блоки удовлетворяют определенным равенствам относительно исходных блоков в отношении разбиения.
LaTeX
$$$(M^{-1})_{pp} M_{pp} + (M^{-1})_{p\lnot p} M_{\lnot p p} = I$$$
Lean4
/-- The inverse of a block-triangular matrix is block-triangular. -/
theorem blockTriangular_inv_of_blockTriangular [LinearOrder α] [Invertible M] (hM : BlockTriangular M b) :
BlockTriangular M⁻¹ b :=
by
suffices ∀ hs : Finset α, univ.image b = hs → BlockTriangular M⁻¹ b by exact this _ rfl
intro s hs
induction s using Finset.strongInduction generalizing m with
| H s ih =>
subst hs
intro i j hij
haveI : Inhabited m := ⟨i⟩
let k := (univ.image b).max' (univ_nonempty.image _)
let b' := fun i : { a // b a < k } => b ↑i
let A := M.toBlock (fun i => b i < k) fun j => b j < k
obtain hbi | hi : b i = k ∨ _ := (le_max' _ (b i) <| mem_image_of_mem _ <| mem_univ _).eq_or_lt
· have : M⁻¹.toBlock (fun i => k ≤ b i) (fun i => b i < k) ⟨i, hbi.ge⟩ ⟨j, hbi ▸ hij⟩ = 0 := by
simp only [toBlock_inverse_eq_zero hM k, Matrix.zero_apply]
simp [this.symm]
haveI : Invertible A := hM.invertibleToBlock _
have hA : A.BlockTriangular b' := hM.submatrix
have hb' : image b' univ ⊂ image b univ :=
by
convert image_subtype_univ_ssubset_image_univ k b _ (fun a => a < k) (lt_irrefl _)
convert max'_mem (α := α) _ _
have hij' : b' ⟨j, hij.trans hi⟩ < b' ⟨i, hi⟩ := by simp_rw [b', hij]
simp [A, hM.inv_toBlock k, (ih (image b' univ) hb' hA rfl hij').symm]
