OAI/Analysis/CoulombIonization/RadialBounds/GlobalDensityBarrier.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombPauli.memLp_tensor line 19
  2. lemma OAI.CoulombPauli.l2_norm_sq line 28
  3. def OAI.CoulombPauli.tensor line 36
  4. lemma OAI.CoulombPauli.tensor_ae line 40
  5. lemma OAI.CoulombPauli.tensor_norm_sq line 43
  6. lemma OAI.CoulombPauli.tensor_norm line 53
  7. lemma OAI.CoulombPauli.tensor_add_right line 58
  8. lemma OAI.CoulombPauli.tensor_smul_right line 67
  9. def OAI.CoulombPauli.tensorLeft line 76
  10. lemma OAI.CoulombPauli.tensorLeft_apply line 83
  11. lemma OAI.CoulombPauli.tensor_inner line 85
  12. lemma OAI.CoulombPauli.tensorLeft_adjoint_tensor line 96
  13. lemma OAI.CoulombPauli.integrable_eq_zero_of_rectangles line 103
  14. lemma OAI.CoulombPauli.tensor_indicator line 116
  15. lemma OAI.CoulombPauli.rectangle_integral_eq_zero_of_tensor_orthogonal line 132
  16. lemma OAI.CoulombPauli.rectangle_indicator_eq_zero_of_tensor_orthogonal line 141
  17. lemma OAI.CoulombPauli.eq_zero_of_tensor_orthogonal line 159
  18. lemma OAI.CoulombPauli.continuousLinearMap_ext_tensor line 182