OAI/Analysis/MatrixSigning/Potential/DiagBlock.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Covariance.diagBlock line 18
  2. lemma OAI.CurrentKS.Covariance.diagBlock_symm line 21
  3. lemma OAI.CurrentKS.Covariance.diagBlock_apply_left line 25
  4. lemma OAI.CurrentKS.Covariance.diagBlock_apply_right line 34
  5. lemma OAI.CurrentKS.Covariance.quad_diagBlock line 43
  6. lemma OAI.CurrentKS.Covariance.diagBlock_psd line 50
  7. lemma OAI.CurrentKS.Covariance.diagBlock_diag line 67
  8. lemma OAI.CurrentKS.Interaction.coordinate_pos line 80
  9. lemma OAI.CurrentKS.Interaction.interaction_duality_le line 89
  10. lemma OAI.CurrentKS.Interaction.interaction_whiten_trace line 99
  11. theorem OAI.CurrentKS.Interaction.state_energy_ensemble line 125