OAI/Analysis/MatrixScaling/Gram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Kaplansky.weighted_variance_pos line 23

   Source documentation

   Strict positivity of the unnormalized weighted variance.

   theorem weighted_variance_pos (w a : ι → ℝ) (hw : ∀ i, 0 ≤ w i)
       (i j : ι) (hi : 0 < w i) (hj : 0 < w j) (hij : a i ≠ a j) :
       0 < (∑ k, w k) * (∑ k, w k * (a k)^2) - (∑ k, w k * a k)^2 := by
   …

2. def OAI.Kaplansky.expMoment line 56
3. theorem OAI.Kaplansky.hasDerivAt_expMoment line 59
4. theorem OAI.Kaplansky.expMoment_zero_pos line 72
5. theorem OAI.Kaplansky.strictConvexOn_log_expSum line 78
6. theorem OAI.Kaplansky.det_one_add_diagonal_mul line 114

   Source documentation

   Multivariate principal-minor expansion, with one scalar for each row.

   theorem det_one_add_diagonal_mul {R : Type*} [CommRing R]
       (G : Matrix n n R) (t : n → R) :
       (1 + Matrix.diagonal t * G).det =
         ∑ s : Finset n, (∏ i ∈ s, t i) *
           (G.submatrix (Subtype.val : s → n) Subtype.val).det := by
   …

7. theorem OAI.Kaplansky.gram_determinant_expansion line 143
8. theorem OAI.Kaplansky.gram_minor_nonneg line 151
9. def OAI.Kaplansky.gramCoefficient line 164
10. theorem OAI.Kaplansky.gramCoefficient_nonneg line 168
11. theorem OAI.Kaplansky.gramCoefficient_empty line 172
12. theorem OAI.Kaplansky.gramCoefficient_singleton line 176
13. theorem OAI.Kaplansky.gramCoefficient_singleton_pos line 189
14. theorem OAI.Kaplansky.gram_determinant_expSum line 195
15. theorem OAI.Kaplansky.strictConvexOn_log_gram line 210