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

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]
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

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
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

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 }
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

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 } }
State after:
no goals

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
Tactic:
intro h
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
h :
  (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

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
h :
  (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:
refine' ⟨h.1, _⟩
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
h :
  (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
    ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
⊢ ∀ (x : n → 𝕜), 0 ≤ star x ⬝ᵥ (D - B.conjTranspose * A⁻¹ * B).mulVec x

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
h :
  (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
    ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
⊢ ∀ (x : n → 𝕜), 0 ≤ star x ⬝ᵥ (D - B.conjTranspose * A⁻¹ * B).mulVec x
Tactic:
intro x
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
h :
  (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
    ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ (D - B.conjTranspose * A⁻¹ * B).mulVec x

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
h :
  (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
    ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ (D - B.conjTranspose * A⁻¹ * B).mulVec x
Tactic:
have := h.2 (- ((A⁻¹ * B).mulVec x) ⊕ᵥ x)
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
h :
  (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
    ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
x : n → 𝕜
this : 0 ≤ star (-(A⁻¹ * B).mulVec x ⊕ᵥ x) ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec (-(A⁻¹ * B).mulVec x ⊕ᵥ x)
⊢ 0 ≤ star x ⬝ᵥ (D - B.conjTranspose * A⁻¹ * B).mulVec x

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
h :
  (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
    ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
x : n → 𝕜
this : 0 ≤ star (-(A⁻¹ * B).mulVec x ⊕ᵥ x) ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec (-(A⁻¹ * B).mulVec x ⊕ᵥ x)
⊢ 0 ≤ star x ⬝ᵥ (D - B.conjTranspose * A⁻¹ * B).mulVec x
Tactic:
rw [dotProduct_mulVec, schur_complement_eq₁₁ B D _ _ hA.1, neg_add_self,
  dotProduct_zero, zero_add] at this
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
h :
  (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
    ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
x : n → 𝕜
this : 0 ≤ star x ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x
⊢ 0 ≤ star x ⬝ᵥ (D - B.conjTranspose * A⁻¹ * B).mulVec x

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
h :
  (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
    ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
x : n → 𝕜
this : 0 ≤ star x ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x
⊢ 0 ≤ star x ⬝ᵥ (D - B.conjTranspose * A⁻¹ * B).mulVec x
Tactic:
rw [dotProduct_mulVec]
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
h :
  (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
    ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
x : n → 𝕜
this : 0 ≤ star x ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x
⊢ 0 ≤ star x ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x

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
h :
  (D - B.conjTranspose * A⁻¹ * B).IsHermitian ∧
    ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
x : n → 𝕜
this : 0 ≤ star x ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x
⊢ 0 ≤ star x ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x
Tactic:
exact this
State after:
no goals

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
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
h : (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

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
h : (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:
refine' ⟨h.1, _⟩
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
⊢ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x

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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
⊢ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
Tactic:
intro x
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x

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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
Tactic:
rw [dotProduct_mulVec, ← Sum.elim_comp_inl_inr x, schur_complement_eq₁₁ B D _ _ hA.1]
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤
    star (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr)) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr)) +
      star (x ∘ Sum.inr) ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr

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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤
    star (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr)) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr)) +
      star (x ∘ Sum.inr) ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
Tactic:
apply le_add_of_nonneg_of_le
State after:
case mpr.ha
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr)) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr))

case mpr.hbc
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr

State before:
case mpr.ha
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr)) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr))

case mpr.hbc
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
Tactic:
{ rw [← dotProduct_mulVec]
  apply hA.posSemidef.2 }
State after:
case mpr.hbc
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr

State before:
case mpr.hbc
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
Tactic:
{ rw [← dotProduct_mulVec _ _ (x ∘ Sum.inr)]
  apply h.2 }
State after:
no goals

State before:
case mpr.ha
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr)) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr))
Tactic:
rw [← dotProduct_mulVec]
State after:
case mpr.ha
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr)) ⬝ᵥ A.mulVec (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr))

State before:
case mpr.ha
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr)) ⬝ᵥ A.mulVec (x ∘ Sum.inl + (A⁻¹ * B).mulVec (x ∘ Sum.inr))
Tactic:
apply hA.posSemidef.2
State after:
no goals

State before:
case mpr.hbc
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
Tactic:
rw [← dotProduct_mulVec _ _ (x ∘ Sum.inr)]
State after:
case mpr.hbc
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inr) ⬝ᵥ (D - B.conjTranspose * A⁻¹ * B).mulVec (x ∘ Sum.inr)

State before:
case mpr.hbc
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inr) ⬝ᵥ (D - B.conjTranspose * A⁻¹ * B).mulVec (x ∘ Sum.inr)
Tactic:
apply h.2
State after:
no goals