SchurFeshbach.lean

1 module
2 
3 public import Mathlib.LinearAlgebra.Matrix.SchurComplement
4 public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
5 public import Mathlib.Tactic.NormNum
6 public import Mathlib.Basic.Complex.Basic
7 
8 public section
9 set_option autoImplicit false
10 
11 /-! Author: Komorebi P. Literal retained blocks of the full matrix resolvent. -/
12 namespace KomorebiPaperVII.SchurFeshbach
13 open Matrix
14 variable {P Q : Type*} [Fintype P] [Fintype Q] [DecidableEq P] [DecidableEq Q]
15 
16 noncomputable def schur (App : Matrix P P ℂ) (Apq : Matrix P Q ℂ)
17     (Aqp : Matrix Q P ℂ) (Aqq : Matrix Q Q ℂ) (z : ℂ) : Matrix P P ℂ :=
18   Matrix.scalar P z-App-Apq*(Matrix.scalar Q z-Aqq)⁻¹*Aqp
19 
20 theorem resolvent_blocks (App : Matrix P P ℂ) (Apq : Matrix P Q ℂ)
21     (Aqp : Matrix Q P ℂ) (Aqq : Matrix Q Q ℂ) (z : ℂ) :
22     Matrix.scalar (P ⊕ Q) z-Matrix.fromBlocks App Apq Aqp Aqq =
23       Matrix.fromBlocks (Matrix.scalar P z-App) (-Apq) (-Aqp) (Matrix.scalar Q z-Aqq) := by
24   ext i j
25   cases i <;> cases j <;> simp [Matrix.fromBlocks,Matrix.scalar,Matrix.diagonal]
26 
27 theorem projected_resolvent (App : Matrix P P ℂ) (Apq : Matrix P Q ℂ)
28     (Aqp : Matrix Q P ℂ) (Aqq : Matrix Q Q ℂ) (z : ℂ)
29     [Invertible (Matrix.scalar Q z-Aqq)]
30     [Invertible (Matrix.scalar (P ⊕ Q) z-Matrix.fromBlocks App Apq Aqp Aqq)] :
31     ((Matrix.scalar (P ⊕ Q) z-Matrix.fromBlocks App Apq Aqp Aqq)⁻¹).submatrix
32       Sum.inl Sum.inl = (schur App Apq Aqp Aqq z)⁻¹ := by
33   let D := Matrix.scalar Q z-Aqq
34   let A := Matrix.scalar P z-App
35   have he := resolvent_blocks App Apq Aqp Aqq z
36   let : Invertible (Matrix.fromBlocks A (-Apq) (-Aqp) D) := Invertible.copy ‹_› _ he.symm
37   let : Invertible (A-(-Apq)*⅟D*(-Aqp)) := Matrix.invertibleOfFromBlocks₂₂Invertible A (-Apq) (-Aqp) D
38   have hinv := Matrix.invOf_fromBlocks₂₂_eq A (-Apq) (-Aqp) D
39   have hs : A-(-Apq)*⅟D*(-Aqp)=schur App Apq Aqp Aqq z := by
40     simp only [Matrix.neg_mul,Matrix.mul_neg,neg_neg,Matrix.invOf_eq_nonsing_inv,schur,D,A]
41   rw [he,← Matrix.invOf_eq_nonsing_inv,hinv]
42   change ⅟(A-(-Apq)*⅟D*(-Aqp))=(schur App Apq Aqp Aqq z)⁻¹
43   rw [Matrix.invOf_eq_nonsing_inv]
44   congr 1
45 
46 theorem schur_invertible (App : Matrix P P ℂ) (Apq : Matrix P Q ℂ)
47     (Aqp : Matrix Q P ℂ) (Aqq : Matrix Q Q ℂ) (z : ℂ)
48     [Invertible (Matrix.scalar Q z-Aqq)] :
49     IsUnit (Matrix.scalar (P ⊕ Q) z-Matrix.fromBlocks App Apq Aqp Aqq) ↔
50       IsUnit (schur App Apq Aqp Aqq z) := by
51   rw [resolvent_blocks, Matrix.isUnit_fromBlocks_iff_of_invertible₂₂]
52   simp only [Matrix.neg_mul,Matrix.mul_neg,neg_neg,Matrix.invOf_eq_nonsing_inv,schur]
53 
54 end KomorebiPaperVII.SchurFeshbach
55 
56 namespace KomorebiPaperVII.SchurFeshbach
57 /-- Counterexample to inferring full invertibility from the eliminated block alone.
58 For z=0 and H=diag(0,-1), the eliminated resolvent block is 1, but z-H is singular. -/
59 theorem eliminated_invertible_full_singular :
60     IsUnit (1 : ℂ) ∧ ¬ IsUnit (!![0, 0; 0, 1] : Matrix (Fin 2) (Fin 2) ℂ) := by
61   constructor
62   · exact isUnit_one
63   · rw [Matrix.isUnit_iff_isUnit_det]
64     norm_num [Matrix.det_fin_two]
65 end KomorebiPaperVII.SchurFeshbach
66 
67 /-! Exported theorem axiom audit. -/
68 #print axioms KomorebiPaperVII.SchurFeshbach.resolvent_blocks
69 #print axioms KomorebiPaperVII.SchurFeshbach.projected_resolvent
70 #print axioms KomorebiPaperVII.SchurFeshbach.schur_invertible
71 #print axioms KomorebiPaperVII.SchurFeshbach.eliminated_invertible_full_singular

Back to source controls