Theorem: Matrix.IsHermitian.fromBlocks₁₁ (CvxLean/Lib/Math/SchurComplement.lean)

State before:
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
⊢ (A.fromBlocks B B.conjTranspose D).IsHermitian ↔ (D - B.conjTranspose * A⁻¹ * B).IsHermitian
Tactic:
have hBAB : (Bᴴ * A⁻¹ * B).IsHermitian := by
  apply isHermitian_conjTranspose_mul_mul
  apply hA.inv
State after:
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ (A.fromBlocks B B.conjTranspose D).IsHermitian ↔ (D - B.conjTranspose * A⁻¹ * B).IsHermitian

State before:
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ (A.fromBlocks B B.conjTranspose D).IsHermitian ↔ (D - B.conjTranspose * A⁻¹ * B).IsHermitian
Tactic:
rw [isHermitian_fromBlocks_iff]
State after:
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ B.conjTranspose = B.conjTranspose ∧ B.conjTranspose.conjTranspose = B ∧ D.IsHermitian ↔
    (D - B.conjTranspose * A⁻¹ * B).IsHermitian

State before:
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ B.conjTranspose = B.conjTranspose ∧ B.conjTranspose.conjTranspose = B ∧ D.IsHermitian ↔
    (D - B.conjTranspose * A⁻¹ * B).IsHermitian
Tactic:
constructor
State after:
case mp
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ B.conjTranspose = B.conjTranspose ∧ B.conjTranspose.conjTranspose = B ∧ D.IsHermitian →
    (D - B.conjTranspose * A⁻¹ * B).IsHermitian

case mpr
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ (D - B.conjTranspose * A⁻¹ * B).IsHermitian →
    A.IsHermitian ∧ B.conjTranspose = B.conjTranspose ∧ B.conjTranspose.conjTranspose = B ∧ D.IsHermitian

State before:
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
⊢ (B.conjTranspose * A⁻¹ * B).IsHermitian
Tactic:
apply isHermitian_conjTranspose_mul_mul
State after:
case hA
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
⊢ A⁻¹.IsHermitian

State before:
case hA
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
⊢ A⁻¹.IsHermitian
Tactic:
apply hA.inv
State after:
no goals

State before:
case mp
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ B.conjTranspose = B.conjTranspose ∧ B.conjTranspose.conjTranspose = B ∧ D.IsHermitian →
    (D - B.conjTranspose * A⁻¹ * B).IsHermitian
Tactic:
intro h
State after:
case mp
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
h : A.IsHermitian ∧ B.conjTranspose = B.conjTranspose ∧ B.conjTranspose.conjTranspose = B ∧ D.IsHermitian
⊢ (D - B.conjTranspose * A⁻¹ * B).IsHermitian

State before:
case mp
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
h : A.IsHermitian ∧ B.conjTranspose = B.conjTranspose ∧ B.conjTranspose.conjTranspose = B ∧ D.IsHermitian
⊢ (D - B.conjTranspose * A⁻¹ * B).IsHermitian
Tactic:
apply IsHermitian.sub h.2.2.2 hBAB
State after:
no goals

State before:
case mpr
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ (D - B.conjTranspose * A⁻¹ * B).IsHermitian →
    A.IsHermitian ∧ B.conjTranspose = B.conjTranspose ∧ B.conjTranspose.conjTranspose = B ∧ D.IsHermitian
Tactic:
intro h
State after:
case mpr
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
h : (D - B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ B.conjTranspose = B.conjTranspose ∧ B.conjTranspose.conjTranspose = B ∧ D.IsHermitian

State before:
case mpr
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
h : (D - B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ B.conjTranspose = B.conjTranspose ∧ B.conjTranspose.conjTranspose = B ∧ D.IsHermitian
Tactic:
refine' ⟨hA, rfl, conjTranspose_conjTranspose B, _⟩
State after:
case mpr
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
h : (D - B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ D.IsHermitian

State before:
case mpr
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
h : (D - B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ D.IsHermitian
Tactic:
rw [← sub_add_cancel D]
State after:
case mpr
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
h : (D - B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ (D - ?mpr + ?mpr).IsHermitian

case mpr
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
h : (D - B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ Matrix n n 𝕜

State before:
case mpr
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
h : (D - B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ (D - ?mpr + ?mpr).IsHermitian

case mpr
n : Type u_3
m : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.IsHermitian
hBAB : (B.conjTranspose * A⁻¹ * B).IsHermitian
h : (D - B.conjTranspose * A⁻¹ * B).IsHermitian
⊢ Matrix n n 𝕜
Tactic:
apply IsHermitian.add h hBAB
State after:
no goals