OAI/Probability/MemoryPrecision/WeightedSelection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MemoryPrecision.realNormalize line 19
2. lemma OAI.MemoryPrecision.realNormalize_local line 24
3. lemma OAI.MemoryPrecision.realNormalize_support line 50
4. lemma OAI.MemoryPrecision.realNormalize_finite line 68
5. lemma OAI.MemoryPrecision.realNormalize_reconstruct line 77
6. lemma OAI.MemoryPrecision.normalized_scale_le line 90
7. lemma OAI.MemoryPrecision.normalized_weighted_selection line 135
8. lemma OAI.MemoryPrecision.localized_weighted_selection line 202