Paper VI · Lean source
SchurFeshbach.lean
Inherited / related evidence Coverage and evidence
The edition relies on earlier or related formal evidence. That evidence is not a fresh full-edition replay.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
KomorebiPaperVI/SchurFeshbach.lean48 lines
Original source path
source/complete/original_snapshot/formalization/lean/KomorebiPaperVI/SchurFeshbach.leanSkip declarations and read code
1 import Mathlib.LinearAlgebra.Matrix.SchurComplement
2 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
3 import Mathlib.Tactic
4
5 /-! Author: Komorebi P. Literal retained blocks of the full matrix resolvent. -/
6 namespace KomorebiPaperVI.SchurFeshbach
7 open Matrix
8 variable {P Q : Type*} [Fintype P] [Fintype Q] [DecidableEq P] [DecidableEq Q]
9
10 noncomputable def schur (App : Matrix P P ℂ) (Apq : Matrix P Q ℂ)
11 (Aqp : Matrix Q P ℂ) (Aqq : Matrix Q Q ℂ) (z : ℂ) : Matrix P P ℂ :=
12 Matrix.scalar P z-App-Apq*(Matrix.scalar Q z-Aqq)⁻¹*Aqp
13
14 theorem resolvent_blocks (App : Matrix P P ℂ) (Apq : Matrix P Q ℂ)
15 (Aqp : Matrix Q P ℂ) (Aqq : Matrix Q Q ℂ) (z : ℂ) :
16 Matrix.scalar (P ⊕ Q) z-Matrix.fromBlocks App Apq Aqp Aqq =
17 Matrix.fromBlocks (Matrix.scalar P z-App) (-Apq) (-Aqp) (Matrix.scalar Q z-Aqq) := by
18 ext i j
19 cases i <;> cases j <;> simp [Matrix.fromBlocks,Matrix.scalar,Matrix.diagonal]
20
21 theorem projected_resolvent (App : Matrix P P ℂ) (Apq : Matrix P Q ℂ)
22 (Aqp : Matrix Q P ℂ) (Aqq : Matrix Q Q ℂ) (z : ℂ)
23 [Invertible (Matrix.scalar Q z-Aqq)]
24 [Invertible (Matrix.scalar (P ⊕ Q) z-Matrix.fromBlocks App Apq Aqp Aqq)] :
25 ((Matrix.scalar (P ⊕ Q) z-Matrix.fromBlocks App Apq Aqp Aqq)⁻¹).submatrix
26 Sum.inl Sum.inl = (schur App Apq Aqp Aqq z)⁻¹ := by
27 let D := Matrix.scalar Q z-Aqq
28 let A := Matrix.scalar P z-App
29 have he := resolvent_blocks App Apq Aqp Aqq z
30 let : Invertible (Matrix.fromBlocks A (-Apq) (-Aqp) D) := Invertible.copy ‹_› _ he.symm
31 let : Invertible (A-(-Apq)*⅟D*(-Aqp)) := Matrix.invertibleOfFromBlocks₂₂Invertible A (-Apq) (-Aqp) D
32 have hinv := Matrix.invOf_fromBlocks₂₂_eq A (-Apq) (-Aqp) D
33 have hs : A-(-Apq)*⅟D*(-Aqp)=schur App Apq Aqp Aqq z := by
34 simp only [Matrix.neg_mul,Matrix.mul_neg,neg_neg,Matrix.invOf_eq_nonsing_inv,schur,D,A]
35 rw [he,← Matrix.invOf_eq_nonsing_inv,hinv]
36 change ⅟(A-(-Apq)*⅟D*(-Aqp))=(schur App Apq Aqp Aqq z)⁻¹
37 rw [Matrix.invOf_eq_nonsing_inv]
38 congr 1
39
40 theorem schur_invertible (App : Matrix P P ℂ) (Apq : Matrix P Q ℂ)
41 (Aqp : Matrix Q P ℂ) (Aqq : Matrix Q Q ℂ) (z : ℂ)
42 [Invertible (Matrix.scalar Q z-Aqq)] :
43 IsUnit (Matrix.scalar (P ⊕ Q) z-Matrix.fromBlocks App Apq Aqp Aqq) ↔
44 IsUnit (schur App Apq Aqp Aqq z) := by
45 rw [resolvent_blocks, Matrix.isUnit_fromBlocks_iff_of_invertible₂₂]
46 simp only [Matrix.neg_mul,Matrix.mul_neg,neg_neg,Matrix.invOf_eq_nonsing_inv,schur]
47
48 end KomorebiPaperVI.SchurFeshbach
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: faa919ceab275eb4d593635337028a19ffcb238ac85cd660fe402935f44375c3
Back to Paper VI: Transfer Semigroups: Stochastic, Bayesian, Fractional, and PDE Realizations