OAI/Analysis/AffineBernstein/MatrixShiftBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.adjugate_eq_det_smul_transpose' line 13
2. lemma OAI.AffineBernstein.adjugate_conjugate_orthogonal' line 20
3. lemma OAI.AffineBernstein.trace_adjugate_le_card_mul_det_add_one line 34

   Source comment

   A coarse uniform bound for the sum of all principal cofactors by the Jacobian of the identity-shifted positive semidefinite map.

   lemma trace_adjugate_le_card_mul_det_add_one {A : Matrix ι ι ℝ}
       (hA : A.PosSemidef) :
       A.adjugate.trace ≤ (Fintype.card ι : ℝ) * (A + 1).det := by
   …