OAI/Analysis/CoulombRadii/Propagation/EnsembleMoments.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.RecordedEnsemble.initial line 14
2. lemma OAI.Coulomb.RecordedEnsemble.initial_conserves line 22
3. lemma OAI.Coulomb.RecordedEnsemble.initial_fermionic line 29
4. lemma OAI.Coulomb.RecordedEnsemble.initial_supported line 34
5. lemma OAI.Coulomb.RecordedEnsemble.initial_mass line 38
6. lemma OAI.Coulomb.RecordedEnsemble.initial_form line 41
7. lemma OAI.Coulomb.RecordedEnsemble.out_square_le line 45
8. lemma OAI.Coulomb.RecordedEnsemble.count_cover_le line 63
9. lemma OAI.Coulomb.RecordedEnsemble.out_square_cover line 77