OAI/Analysis/CoulombIonization/ThomasFermi/Tensor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAnalysis.tf_memLp_prod line 38
  2. def OAI.CoulombAnalysis.tfTensor line 48
  3. lemma OAI.CoulombAnalysis.tfTensor_coe line 51
  4. lemma OAI.CoulombAnalysis.tfTensor_norm line 56
  5. lemma OAI.CoulombAnalysis.tfTensor_add_left line 66
  6. lemma OAI.CoulombAnalysis.tfTensor_add_right line 75
  7. lemma OAI.CoulombAnalysis.tfTensor_smul_left line 84
  8. lemma OAI.CoulombAnalysis.tfTensor_smul_right line 93
  9. def OAI.CoulombAnalysis.tfTensorₗ line 102
  10. lemma OAI.CoulombAnalysis.tfTensorₗ_bound line 106
  11. def OAI.CoulombAnalysis.tfTensorL line 111
  12. lemma OAI.CoulombAnalysis.tfTensorL_apply line 114
  13. instance OAI.CoulombAnalysis.tfDualFact line 118
  14. instance OAI.CoulombAnalysis.tfConjugate line 120