OAI/Analysis/AffineBernstein/MatrixMetric.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.inverseMatrixPair line 12
2. lemma OAI.AffineBernstein.inverseMatrixPair_eq_dot line 15
3. lemma OAI.AffineBernstein.inverseMatrixPair_self_nonneg line 25
4. lemma OAI.AffineBernstein.inverseMatrixPair_symm line 30
5. lemma OAI.AffineBernstein.inverseMatrixPair_add_left line 42
6. lemma OAI.AffineBernstein.inverseMatrixPair_add_right line 46
7. lemma OAI.AffineBernstein.inverseMatrixPair_smul_left line 50
8. lemma OAI.AffineBernstein.inverseMatrixPair_smul_right line 59
9. lemma OAI.AffineBernstein.inverseMatrixPair_cauchy line 69

   Source comment

   Cauchy--Schwarz for a positive definite inverse matrix, including zero vectors.

   lemma inverseMatrixPair_cauchy {A : Matrix ι ι ℝ} (hA : A.PosDef) (x y : ι → ℝ) :
       inverseMatrixPair A x y^2 ≤ inverseMatrixPair A x x*inverseMatrixPair A y y := by
   …

   Mentions: OAI.AffineBernstein.inverseMatrixPair