LeanPool.RlTheoryInLean.Data.Matrix.PosDef

class Matrix.PosDefAsymm {α : Type u_1} [Fintype α] (A : Matrix α α ℝ) : Prop

A real square matrix whose quadratic form has positive asymmetric part.

• pd (x : α → ℝ) : x ≠ 0 → 0 < x ⬝ᵥ A.mulVec x

theorem Matrix.posDefAsymm_iff {α : Type u_1} [Fintype α] (A : Matrix α α ℝ) : A.PosDefAsymm ↔ (A + A.transpose).PosDef

theorem Matrix.posDefAsymm_iff' {α : Type u_2} [Fintype α] (A : Matrix α α ℝ) : A.PosDefAsymm ↔ ∃ (η : ℝ), 0 < η ∧ ∀ (x : α → ℝ), η * x ⬝ᵥ x ≤ x ⬝ᵥ A.mulVec x

class Matrix.NegDefAsymm {α : Type u_1} [Fintype α] (A : Matrix α α ℝ) : Prop

A real square matrix whose negation is asymmetrically positive definite.

• nd : (-A).PosDefAsymm

@[implicit_reducible]

noncomputable instance Matrix.instInvertibleRealDetOfPosDefAsymm {α : Type u_1} [Fintype α] (A : Matrix α α ℝ) [DecidableEq α] [A.PosDefAsymm] : Invertible A.det

Equations

• A.instInvertibleRealDetOfPosDefAsymm = invertibleOfNonzero ⋯

@[implicit_reducible]

noncomputable instance Matrix.instInvertibleRealOfPosDefAsymm {α : Type u_1} [Fintype α] (A : Matrix α α ℝ) [DecidableEq α] [A.PosDefAsymm] : Invertible A

Equations

• A.instInvertibleRealOfPosDefAsymm = A.invertibleOfDetInvertible

@[implicit_reducible]

noncomputable instance Matrix.instInvertibleRealDetOfNegDefAsymm {α : Type u_1} [Fintype α] (A : Matrix α α ℝ) [DecidableEq α] [A.NegDefAsymm] : Invertible A.det

Equations

• A.instInvertibleRealDetOfNegDefAsymm = invertibleOfNonzero ⋯

@[implicit_reducible]

noncomputable instance Matrix.instInvertibleRealOfNegDefAsymm {α : Type u_1} [Fintype α] (A : Matrix α α ℝ) [DecidableEq α] [A.NegDefAsymm] : Invertible A

Equations

• A.instInvertibleRealOfNegDefAsymm = A.invertibleOfDetInvertible