OAI/Analysis/AffineBernstein/MatrixCombination.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.inverseMatrixPair_sum_left line 14
2. lemma OAI.AffineBernstein.inverseMatrixPair_combination line 25

   Source comment

   Cauchy--Schwarz for an arbitrary finite linear combination in the literal inverse metric.

   lemma inverseMatrixPair_combination {A : Matrix ι ι ℝ} (hA : A.PosDef)
       (a : J → ℝ) (v : J → ι → ℝ) :
       inverseMatrixPair A (fun i => ∑ j, a j*v j i) (fun i => ∑ j, a j*v j i) ≤
         (∑ j, a j^2)*(∑ j, inverseMatrixPair A (v j) (v j)) := by
   …

   Mentions: OAI.AffineBernstein.inverseMatrixPair