OAI/Probability/MatroidProphet/Statements.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Hidden-vector matroid selection
The observation mask depends only on the initial seed, before weights are seen. Observed labels are sacrificed. The minimum over all arrival permutations is taken separately for each seed, inside the expectation.
This file declares nothing itself. It gathers the import below, so a file that imports it gets all of them.