OAI/Analysis/CoulombRadii/RandomFields/JointSlice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.potentialForm_coreSlice_joint_aestronglyMeasurable line 13
2. lemma OAI.Coulomb.potentialForm_normalized_coreSlice_joint_aestronglyMeasurable line 42
3. lemma OAI.Coulomb.restrictedOutPotential_joint_measurable line 51
4. lemma OAI.Coulomb.restrictedCorePotential_normalized_slice_joint line 59
5. lemma OAI.Coulomb.recordedFarField_normalized_slice_joint line 69
6. lemma OAI.Coulomb.farSquare_mass_ballCloud_integrable line 77
7. theorem OAI.Coulomb.sliceExpectation_farSquare_ballCloud line 112