OAI/Analysis/HyperbolicCones/PositivePath.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Paper256.posSemidef_of_nonsingular_path line 14

   Source documentation

   A continuous symmetric matrix path with no singularities at positive times cannot change from indefinite to positive definite.

   theorem posSemidef_of_nonsingular_path {n : ℕ} (F : ℝ → Sym n)
       (hF : ContinuousOn F (Ici 0)) (hF0 : ContinuousAt F 0)
       (hunit : ∀ t : ℝ, 0 < t → IsUnit (F t : Mat n ℝ))
       (hpos : ∃ t : ℝ, 0 < t ∧ (F t : Mat n ℝ).PosDef) :
       (F 0 : Mat n ℝ).PosSemidef := by
   …

   Mentions: OAI.Paper256.Sym, OAI.Paper256.Mat