OAI/Analysis/MatrixSigning/Matrices/TraceCLM.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentKS.Hermitian.realTrace_zero line 15
  2. lemma OAI.CurrentKS.Hermitian.realTrace_add line 18
  3. lemma OAI.CurrentKS.Hermitian.realTrace_sub line 22
  4. lemma OAI.CurrentKS.Hermitian.realTrace_smul line 26
  5. lemma OAI.CurrentKS.Hermitian.realTrace_one line 32
  6. lemma OAI.CurrentKS.Hermitian.realTrace_nonneg line 35
  7. lemma OAI.CurrentKS.Hermitian.realTrace_pos line 38
  8. lemma OAI.CurrentKS.Hermitian.realTrace_mono line 41
  9. def OAI.CurrentKS.Hermitian.traceCLM line 45
  10. lemma OAI.CurrentKS.Hermitian.traceCLM_apply line 47
  11. lemma OAI.CurrentKS.Hermitian.continuous_realTrace line 49
  12. lemma OAI.CurrentKS.Hermitian.continuousAt_invH line 54
  13. lemma OAI.CurrentKS.Hermitian.pd_of_lower line 63
  14. lemma OAI.CurrentKS.Hermitian.inverse_bound_below line 69
  15. lemma OAI.CurrentKS.Hermitian.psd_nonneg line 77
  16. lemma OAI.CurrentKS.Hermitian.mem_psd_iff_nonneg line 79
  17. lemma OAI.CurrentKS.Hermitian.scalar_one_mono line 86
  18. lemma OAI.CurrentKS.Hermitian.trace_bound_above line 92