OAI/Analysis/CoulombRadii/Localization/DeletedLabels.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.sliceExpectation_add line 134
  2. lemma OAI.Coulomb.sliceExpectation_sub line 140
  3. lemma OAI.Coulomb.sliceExpectation_const_mul line 146
  4. lemma OAI.Coulomb.sliceExpectation_mono_ae line 150
  5. lemma OAI.Coulomb.normalized_coreForm_weight_integrable line 158
  6. lemma OAI.Coulomb.retainedFinePower_weight_integrable line 163
  7. lemma OAI.Coulomb.retainedFineCoulomb_weight_integrable line 169
  8. lemma OAI.Coulomb.outerPair_weight_integrable line 175
  9. def OAI.Coulomb.deletedLabels line 179
  10. lemma OAI.Coulomb.deletedLabels_measurable line 181
  11. lemma OAI.Coulomb.retained_deleted_sum line 186
  12. def OAI.Coulomb.discreteFineTF line 191
  13. def OAI.Coulomb.fineLocalizationError line 196
  14. lemma OAI.Coulomb.discreteFineTF_weight_integrable line 199
  15. lemma OAI.Coulomb.fine_energy_expectation_lower line 208
  16. theorem OAI.Coulomb.conditional_fine_lower line 226