internlm/Lean-Github huggingface dataset:
Theorem: Matrix.toSquareBlock_inv_mul_toSquareBlock_eq_one
Proof state before:
case neg
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i = k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 1
i : { a // p a }
j : { a // (fun i => ¬p i) a }
l : { a // p a }
hj : ¬b ↑j ≤ k
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
have hj := lt_of_not_ge hj
Proof state after:
case neg
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i = k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 1
i : { a // p a }
j : { a // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : ¬b ↑j ≤ k
hj : k < b ↑j
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
Theorem: Matrix.toSquareBlock_inv_mul_toSquareBlock_eq_one
Proof state before:
case neg
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i = k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 1
i : { a // p a }
j : { a // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : ¬b ↑j ≤ k
hj : k < b ↑j
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
apply mul_eq_zero_of_right
Proof state after:
case neg.h
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i = k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 1
i : { a // p a }
j : { a // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : ¬b ↑j ≤ k
hj : k < b ↑j
⊢ M.toBlock (fun i => ¬p i) p j l = 0
Theorem: Matrix.toSquareBlock_inv_mul_toSquareBlock_eq_one
Proof state before:
case neg.h
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i = k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 1
i : { a // p a }
j : { a // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : ¬b ↑j ≤ k
hj : k < b ↑j
⊢ M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
simpa using hM (lt_of_eq_of_lt l.2 hj)
Proof state after:
no goals
Theorem: Matrix.toSquareBlock_inv_mul_toSquareBlock_eq_one
Proof state before:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i = k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 1
h_zero :
  ∀ (i : { a // p a }) (j : { a // (fun i => ¬p i) a }) (l : { a // p a }),
    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
⊢ (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 0
Tactic:
ext i l
Proof state after:
case a
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i = k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 1
h_zero :
  ∀ (i : { a // p a }) (j : { a // (fun i => ¬p i) a }) (l : { a // p a }),
    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
i l : { a // p a }
⊢ ((M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p) i l = 0 i l
Theorem: Matrix.toSquareBlock_inv_mul_toSquareBlock_eq_one
Proof state before:
case a
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i = k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 1
h_zero :
  ∀ (i : { a // p a }) (j : { a // (fun i => ¬p i) a }) (l : { a // p a }),
    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
i l : { a // p a }
⊢ ((M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p) i l = 0 i l
Tactic:
apply sum_eq_zero (λ j _ => h_zero i j l)
Proof state after:
no goals
Theorem: Matrix.schur_complement_eq₁₁
Proof state before:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible A
hA : A.IsHermitian
⊢ star (x ⊕ᵥ y) ᵥ* A.fromBlocks B B.conjTranspose D ⬝ᵥ (x ⊕ᵥ y) =
    star (x + (A⁻¹ * B).mulVec y) ᵥ* A ⬝ᵥ (x + (A⁻¹ * B).mulVec y) + star y ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ y
Tactic:
simp [Function.star_sum_elim, fromBlocks_mulVec, vecMul_fromBlocks, add_vecMul,
  dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, vecMul_mulVec, hA.eq,
  conjTranspose_nonsing_inv, star_mulVec]
Proof state after:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible A
hA : A.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* A ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x +
        (star x ᵥ* B ⬝ᵥ y + star y ᵥ* (B.conjTranspose * (A⁻¹ * B)) ⬝ᵥ y) +
      (star y ᵥ* D ⬝ᵥ y - star y ᵥ* (B.conjTranspose * (A⁻¹ * B)) ⬝ᵥ y)
Theorem: Matrix.schur_complement_eq₁₁
Proof state before:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible A
hA : A.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* A ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x +
        (star x ᵥ* B ⬝ᵥ y + star y ᵥ* (B.conjTranspose * (A⁻¹ * B)) ⬝ᵥ y) +
      (star y ᵥ* D ⬝ᵥ y - star y ᵥ* (B.conjTranspose * (A⁻¹ * B)) ⬝ᵥ y)
Tactic:
abel
Proof state after:
no goals
Theorem: Matrix.schur_complement_eq₂₂
Proof state before:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible D
hD : D.IsHermitian
⊢ star (x ⊕ᵥ y) ᵥ* A.fromBlocks B B.conjTranspose D ⬝ᵥ (x ⊕ᵥ y) =
    star ((D⁻¹ * B.conjTranspose).mulVec x + y) ᵥ* D ⬝ᵥ ((D⁻¹ * B.conjTranspose).mulVec x + y) +
      star x ᵥ* (A - B * D⁻¹ * B.conjTranspose) ⬝ᵥ x
Tactic:
simp [Function.star_sum_elim, fromBlocks_mulVec, vecMul_fromBlocks, add_vecMul,
  dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, vecMul_mulVec, hD.eq,
  conjTranspose_nonsing_inv, star_mulVec]
Proof state after:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible D
hD : D.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* (B * (D⁻¹ * B.conjTranspose)) ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x +
        (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) +
      (star x ᵥ* A ⬝ᵥ x - star x ᵥ* (B * (D⁻¹ * B.conjTranspose)) ⬝ᵥ x)
Theorem: Matrix.schur_complement_eq₂₂
Proof state before:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible D
hD : D.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* (B * (D⁻¹ * B.conjTranspose)) ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x +
        (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) +
      (star x ᵥ* A ⬝ᵥ x - star x ᵥ* (B * (D⁻¹ * B.conjTranspose)) ⬝ᵥ x)
Tactic:
abel
Proof state after:
no goals
Theorem: Matrix.IsHermitian.fromBlocks₁₁
Proof 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
Proof 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
Theorem: Matrix.IsHermitian.fromBlocks₁₁
Proof 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]
Proof 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
Theorem: Matrix.IsHermitian.fromBlocks₁₁
Proof 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
Proof 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
Theorem: Matrix.IsHermitian.fromBlocks₁₁
Proof 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
Proof 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
Theorem: Matrix.IsHermitian.fromBlocks₁₁
Proof 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
Proof state after:
no goals
Theorem: Matrix.IsHermitian.fromBlocks₁₁
Proof 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
Proof 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
Theorem: Matrix.IsHermitian.fromBlocks₁₁
Proof 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
Proof state after:
no goals
Theorem: Matrix.IsHermitian.fromBlocks₁₁
Proof 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
Proof 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
Theorem: Matrix.IsHermitian.fromBlocks₁₁
Proof 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, _⟩
Proof 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
Theorem: Matrix.IsHermitian.fromBlocks₁₁
Proof 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]
Proof 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 𝕜
Theorem: Matrix.IsHermitian.fromBlocks₁₁
Proof 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
Proof state after:
no goals
Theorem: Matrix.IsHermitian.fromBlocks₂₂
Proof state before:
n : Type u_1
m : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.IsHermitian
⊢ (A.fromBlocks B B.conjTranspose D).IsHermitian ↔ (A - B * D⁻¹ * B.conjTranspose).IsHermitian
Tactic:
rw [← isHermitian_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply,
  fromBlocks_submatrix_sum_swap_sum_swap]
Proof state after:
n : Type u_1
m : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.IsHermitian
⊢ (D.fromBlocks B.conjTranspose B A).IsHermitian ↔ (A - B * D⁻¹ * B.conjTranspose).IsHermitian
Theorem: Matrix.IsHermitian.fromBlocks₂₂
Proof state before:
n : Type u_1
m : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.IsHermitian
⊢ (D.fromBlocks B.conjTranspose B A).IsHermitian ↔ (A - B * D⁻¹ * B.conjTranspose).IsHermitian
Tactic:
convert IsHermitian.fromBlocks₁₁ _ _ hD <;> rw [conjTranspose_conjTranspose]
Proof state after:
no goals
Theorem: Matrix.PosSemidef.fromBlocks₁₁
Proof state before:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
⊢ (A.fromBlocks B B.conjTranspose D).PosSemidef ↔ (D - B.conjTranspose * A⁻¹ * B).PosSemidef
Tactic:
rw [PosSemidef, IsHermitian.fromBlocks₁₁ _ _ hA.1]
Proof state after:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
⊢ ((D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
      ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x) ↔
    (D - B.conjTranspose * A⁻¹ * B).PosSemidef
Theorem: Matrix.PosSemidef.fromBlocks₁₁
Proof state before:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
⊢ ((D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
      ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x) ↔
    (D - B.conjTranspose * A⁻¹ * B).PosSemidef
Tactic:
constructor
Proof state after:
case mp
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
⊢ ((D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
      ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x) →
    (D - B.conjTranspose * A⁻¹ * B).PosSemidef

case mpr
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
⊢ (D - B.conjTranspose * A⁻¹ * B).PosSemidef →
    (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
      ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
Theorem: Matrix.PosSemidef.fromBlocks₁₁
Proof state before:
case mp
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
⊢ ((D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
      ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x) →
    (D - B.conjTranspose * A⁻¹ * B).PosSemidef

case mpr
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
⊢ (D - B.conjTranspose * A⁻¹ * B).PosSemidef →
    (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
      ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
Tactic:
{ intro h; refine' ⟨h.1, _⟩; intro x
  have := h.2 (- ((A⁻¹ * B).mulVec x) ⊕ᵥ x)
  rw [dotProduct_mulVec, schur_complement_eq₁₁ B D _ _ hA.1, neg_add_self,
    dotProduct_zero, zero_add] at this
  rw [dotProduct_mulVec]; exact this }
Proof state after:
case mpr
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
⊢ (D - B.conjTranspose * A⁻¹ * B).PosSemidef →
    (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
      ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
Theorem: Matrix.PosSemidef.fromBlocks₁₁
Proof state before:
case mpr
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : A.PosDef
inst✝ : Invertible A
⊢ (D - B.conjTranspose * A⁻¹ * B).PosSemidef →
    (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
      ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
Tactic:
{ intro h; refine' ⟨h.1, _⟩; intro x
  rw [dotProduct_mulVec, ← Sum.elim_comp_inl_inr x, schur_complement_eq₁₁ B D _ _ hA.1]
  apply le_add_of_nonneg_of_le
  { rw [← dotProduct_mulVec]
    apply hA.posSemidef.2 }
  { rw [← dotProduct_mulVec _ _ (x ∘ Sum.inr)]
    apply h.2 } }
Proof state after:
no goals