OAI/Analysis/CoulombRadii/RandomFields/CutJensen.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.boundedObservable_integrable line 13
2. lemma OAI.Coulomb.potentialForm_abs_le line 19
3. lemma OAI.Coulomb.mass_normalized_le_one line 43
4. def OAI.Coulomb.coreConditionalObservable line 48
5. lemma OAI.Coulomb.coreConditionalObservable_abs_le line 52
6. lemma OAI.Coulomb.coreConditionalObservable_aestronglyMeasurable line 60
7. lemma OAI.Coulomb.coreConditionalObservable_weight_integrable line 71
8. lemma OAI.Coulomb.coreConditionalObservable_positive_weight_integrable line 80
9. lemma OAI.Coulomb.sliceExpectation_coreConditionalObservable line 92
10. theorem OAI.Coulomb.conditional_ensemble_positive_jensen line 102