OAI/Analysis/CoulombIonization/FieldAnalysis/dShellInnerField.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.rawInnerField line 17
  2. def OAI.CoulombAtom.oneBodyInnerField line 20
  3. def OAI.CoulombAtom.weightedInnerPairs line 24
  4. lemma OAI.CoulombAtom.graph_pair_integrable_all line 29
  5. lemma OAI.CoulombAtom.weightedInnerPairs_integrable line 36
  6. lemma OAI.CoulombAtom.weightedInnerPairs_le line 43
  7. lemma OAI.CoulombAtom.innerField_density_arithmetic line 62
  8. lemma OAI.CoulombAtom.oneBodyInnerField_density line 74
  9. lemma OAI.CoulombAtom.oneBodyInnerField_density_integrable line 84
  10. lemma OAI.CoulombAtom.integral_sum_sub_sum line 92
  11. lemma OAI.CoulombAtom.oneBodyInnerField_density_integral line 105
  12. lemma OAI.CoulombAtom.oneBodyInnerField_raw_integral line 116
  13. theorem OAI.CoulombAtom.quantum_shell_inner_field_residual line 134
  14. theorem OAI.CoulombAtom.quantum_shell_inner_field line 148