OAI/Analysis/MatrixSigning/Potential/Interaction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Interaction.interaction line 16
  2. def OAI.CurrentKS.Interaction.responseInput line 19
  3. lemma OAI.CurrentKS.Interaction.interaction_symm line 22
  4. lemma OAI.CurrentKS.Interaction.interaction_nonneg line 29
  5. lemma OAI.CurrentKS.Interaction.sandwich_responseInput line 35
  6. lemma OAI.CurrentKS.Interaction.interaction_mulVec line 40
  7. lemma OAI.CurrentKS.Interaction.interaction_diag line 49
  8. lemma OAI.CurrentKS.Interaction.interaction_quad line 64
  9. lemma OAI.CurrentKS.Interaction.interaction_psd line 80
  10. lemma OAI.CurrentKS.Interaction.interaction_entry_bound line 87
  11. lemma OAI.CurrentKS.Interaction.interaction_entry_square line 97
  12. lemma OAI.CurrentKS.Interaction.eta_response line 105
  13. lemma OAI.CurrentKS.Interaction.eta_as_response line 119
  14. lemma OAI.CurrentKS.Interaction.sandwich_one_square line 131
  15. lemma OAI.CurrentKS.Interaction.interaction_duality line 136