OAI/Analysis/HardSphere/Comparison/AffinityNormalization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Comparison.measureAffinity_eq_dominated line 11
2. lemma OAI.HardSphere.Comparison.affinity_finset_sum line 30
3. lemma OAI.HardSphere.Comparison.rnDeriv_real_mono line 47
4. lemma OAI.HardSphere.Comparison.measureAffinity_mono line 57
5. lemma OAI.HardSphere.Comparison.rnDeriv_real_finset_sum line 77
6. lemma OAI.HardSphere.Comparison.measureAffinity_finset_sum line 93
7. lemma OAI.HardSphere.Comparison.measureAffinity_smul line 119
8. lemma OAI.HardSphere.Comparison.affinity_tag_normalization line 141