OAI/Analysis/CoulombRadii/Packets/InnerMeshCap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.exists_inner_shell_mesh line 12
2. def OAI.Coulomb.innerMeshCap line 35
3. lemma OAI.Coulomb.innerMeshCap_nonneg line 38
4. lemma OAI.Coulomb.innerMeshCap_sq line 41
5. lemma OAI.Coulomb.innerLocalCap_le_mesh line 45
6. lemma OAI.Coulomb.innerMeshCap_normalized_slice_aestronglyMeasurable line 51
7. lemma OAI.Coulomb.innerMeshCap_bound line 57
8. lemma OAI.Coulomb.innerMeshCap_weight_integrable line 66
9. structure OAI.Coulomb.RecordedEnsemble.InnerEnvelope line 80
10. theorem OAI.Coulomb.RecordedEnsemble.exists_inner_shell_envelope line 89