OAI/Analysis/CoulombRadii/Screening/OutCap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.positive_square_ballCloud_integral_le line 14
  2. def OAI.Coulomb.localFarCap line 37
  3. lemma OAI.Coulomb.localFarCap_nonneg line 42
  4. lemma OAI.Coulomb.localFarCap_sq line 45
  5. lemma OAI.Coulomb.localFarCap_le line 53
  6. lemma OAI.Coulomb.localFarCap_normalized_slice_aestronglyMeasurable line 65
  7. lemma OAI.Coulomb.localFarCap_weight_integrable line 77
  8. theorem OAI.Coulomb.sliceExpectation_localFarCap_sq line 87
  9. lemma OAI.Coulomb.pairPotential_nonneg_pointwise line 98
  10. theorem OAI.Coulomb.conditionalOutCost_lower_local line 106