OAI/Analysis/CoulombRadii/RandomFields/ConditionalRMS.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.potentialForm_bounded_add line 14
  2. lemma OAI.Coulomb.coreConditionalObservable_nonneg line 21
  3. lemma OAI.Coulomb.coreConditionalObservable_mono line 25
  4. lemma OAI.Coulomb.coreConditionalObservable_add line 35
  5. lemma OAI.Coulomb.coreConditionalObservable_square_weight_integrable line 46
  6. lemma OAI.Coulomb.potentialForm_normalized_square_le line 58
  7. lemma OAI.Coulomb.slice_conditional_square_le line 66
  8. def OAI.Coulomb.RecordedEnsemble.dataRMS line 85
  9. lemma OAI.Coulomb.RecordedEnsemble.dataRMS_nonneg line 88
  10. lemma OAI.Coulomb.RecordedEnsemble.dataRMS_sq line 89
  11. lemma OAI.Coulomb.RecordedEnsemble.dataRMS_mono line 94
  12. lemma OAI.Coulomb.RecordedEnsemble.dataRMS_add line 104
  13. theorem OAI.Coulomb.RecordedEnsemble.Conserves.dataRMS_conditional_le line 132