OAI/Analysis/CoulombIonization/FormDomain/GraphWeightIntegral.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.weightedMass_eq_integral line 17
  2. lemma OAI.CoulombAtom.graph_weight_integrable line 23
  3. lemma OAI.CoulombAtom.gradientError_eq_weightedMass line 28
  4. def OAI.CoulombAtom.rawGradientWeight line 38
  5. lemma OAI.CoulombAtom.rawGradientWeight_nonneg line 41
  6. lemma OAI.CoulombAtom.rawGradientWeight_measurable line 44
  7. lemma OAI.CoulombAtom.rawGradientWeight_le line 48
  8. lemma OAI.CoulombAtom.rawGradientWeight_integrable line 55
  9. lemma OAI.CoulombAtom.gradientError_eq_integral line 61
  10. lemma OAI.CoulombAtom.graph_sum_value line 85
  11. lemma OAI.CoulombAtom.graph_sub_value line 91
  12. lemma OAI.CoulombAtom.finite_apply_sum_value line 97
  13. lemma OAI.CoulombAtom.ofReal_sub_mul_complex line 114
  14. lemma OAI.CoulombAtom.finite_apply_sum_eq_sub line 117