OAI/Analysis/CoulombRadii/FieldAnalysis/CubeMassMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.cubeMass_le_mass line 19
2. lemma OAI.Coulomb.cubeKinetic_le_kinetic line 29
3. lemma OAI.Coulomb.cubeState_weighted line 43
4. lemma OAI.Coulomb.cubeState_weighted_summable line 51
5. lemma OAI.Coulomb.cubeState_weighted_le line 58
6. lemma OAI.Coulomb.cubeRumin_constant line 67
7. theorem OAI.Coulomb.cube_density_power_bound line 73