internlm/Lean-Github huggingface dataset:
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
Tactic:
intro h
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
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
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
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, _⟩
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
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
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
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
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
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
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
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)
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
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
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
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
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
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
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
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]
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
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
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
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
Proof state after:
no goals
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
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
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
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
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, _⟩
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
⊢ ∀ (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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
⊢ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ (A.fromBlocks B B.conjTranspose D).mulVec x
Tactic:
intro x
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
h : (D - B.conjTranspose * A⁻¹ * B).PosSemidef
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
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]
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
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
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
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
Proof 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
Theorem: Matrix.PosSemidef.fromBlocks₁₁
Proof 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 }
Proof 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
Theorem: Matrix.PosSemidef.fromBlocks₁₁
Proof 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 }
Proof state after:
no goals
Theorem: Matrix.PosSemidef.fromBlocks₁₁
Proof 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]
Proof 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))
Theorem: Matrix.PosSemidef.fromBlocks₁₁
Proof 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
Proof state after:
no goals
Theorem: Matrix.PosSemidef.fromBlocks₁₁
Proof 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)]
Proof 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)
Theorem: Matrix.PosSemidef.fromBlocks₁₁
Proof 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
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✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.PosDef
inst✝ : Invertible D
⊢ (A.fromBlocks B B.conjTranspose D).PosSemidef ↔ (A - B * D⁻¹ * B.conjTranspose).PosSemidef
Tactic:
rw [← posSemidef_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply,
  fromBlocks_submatrix_sum_swap_sum_swap]
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 𝕜
hD : D.PosDef
inst✝ : Invertible D
⊢ (D.fromBlocks B.conjTranspose B A).PosSemidef ↔ (A - B * D⁻¹ * B.conjTranspose).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✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.PosDef
inst✝ : Invertible D
⊢ (D.fromBlocks B.conjTranspose B A).PosSemidef ↔ (A - B * D⁻¹ * B.conjTranspose).PosSemidef
Tactic:
convert @PosSemidef.fromBlocks₁₁ m n 𝕜 _ _ _ _ _ _ _ hD _ <;>
rw [conjTranspose_conjTranspose]
Proof state after:
no goals
Theorem: Vec.div_le_iff
Proof state before:
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
⊢ a / b ≤ c ↔ a ≤ c * b
Tactic:
constructor
Proof state after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
⊢ a / b ≤ c → a ≤ c * b

case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
⊢ a ≤ c * b → a / b ≤ c
Theorem: Vec.div_le_iff
Proof state before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
⊢ a / b ≤ c → a ≤ c * b
Tactic:
intro h i
Proof state after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
⊢ a i ≤ (c * b) i
Theorem: Vec.div_le_iff
Proof state before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
⊢ a i ≤ (c * b) i
Tactic:
have hi := h i
Proof state after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
hi : (a / b) i ≤ c i
⊢ a i ≤ (c * b) i
Theorem: Vec.div_le_iff
Proof state before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
hi : (a / b) i ≤ c i
⊢ a i ≤ (c * b) i
Tactic:
simp at hi
Proof state after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
hi : a i / b i ≤ c i
⊢ a i ≤ (c * b) i
Theorem: Vec.div_le_iff
Proof state before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
hi : a i / b i ≤ c i
⊢ a i ≤ (c * b) i
Tactic:
rw [_root_.div_le_iff (hb i)] at hi
Proof state after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
hi : a i ≤ c i * b i
⊢ a i ≤ (c * b) i
Theorem: Vec.div_le_iff
Proof state before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
hi : a i ≤ c i * b i
⊢ a i ≤ (c * b) i
Tactic:
exact hi
Proof state after:
no goals
Theorem: Vec.div_le_iff
Proof state before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
⊢ a ≤ c * b → a / b ≤ c
Tactic:
intro h i
Proof state after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
⊢ (a / b) i ≤ c i
Theorem: Vec.div_le_iff
Proof state before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
⊢ (a / b) i ≤ c i
Tactic:
have hi := h i
Proof state after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ (c * b) i
⊢ (a / b) i ≤ c i
Theorem: Vec.div_le_iff
Proof state before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ (c * b) i
⊢ (a / b) i ≤ c i
Tactic:
simp at hi
Proof state after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ c i * b i
⊢ (a / b) i ≤ c i
Theorem: Vec.div_le_iff
Proof state before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ c i * b i
⊢ (a / b) i ≤ c i
Tactic:
dsimp
Proof state after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ c i * b i
⊢ a i / b i ≤ c i
Theorem: Vec.div_le_iff
Proof state before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ c i * b i
⊢ a i / b i ≤ c i
Tactic:
rw [_root_.div_le_iff (hb i)]
Proof state after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ c i * b i
⊢ a i ≤ c i * b i
Theorem: Vec.div_le_iff
Proof state before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ c i * b i
⊢ a i ≤ c i * b i
Tactic:
exact hi
Proof state after:
no goals
Theorem: Vec.le_div_iff
Proof state before:
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
⊢ a ≤ b / c ↔ a * c ≤ b
Tactic:
constructor
Proof state after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
⊢ a ≤ b / c → a * c ≤ b

case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
⊢ a * c ≤ b → a ≤ b / c
Theorem: Vec.le_div_iff
Proof state before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
⊢ a ≤ b / c → a * c ≤ b
Tactic:
intro h i
Proof state after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
⊢ (a * c) i ≤ b i
Theorem: Vec.le_div_iff
Proof state before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
⊢ (a * c) i ≤ b i
Tactic:
have hi := h i
Proof state after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
hi : a i ≤ (b / c) i
⊢ (a * c) i ≤ b i
Theorem: Vec.le_div_iff
Proof state before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
hi : a i ≤ (b / c) i
⊢ (a * c) i ≤ b i
Tactic:
simp at hi
Proof state after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
hi : a i ≤ b i / c i
⊢ (a * c) i ≤ b i
Theorem: Vec.le_div_iff
Proof state before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
hi : a i ≤ b i / c i
⊢ (a * c) i ≤ b i
Tactic:
rw [_root_.le_div_iff (hc i)] at hi
Proof state after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
hi : a i * c i ≤ b i
⊢ (a * c) i ≤ b i
Theorem: Vec.le_div_iff
Proof state before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
hi : a i * c i ≤ b i
⊢ (a * c) i ≤ b i
Tactic:
exact hi
Proof state after:
no goals