OAI/Probability/MatroidSecretary/Selection/FeasibilitySpec.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.MainRuleFeasibility line 12

   Source documentation

   Core and hidden prefix feasibility, measurability after masking the initial observations, complete accepted-set nonanticipation, irrevocability, and literal rejection of sacrificed labels. The mask depends only on the initial seed by the type of HiddenRule; no weight-dependent mask is allowed.

   def MainRuleFeasibility {n bits : ℕ} (M : Matroid (Fin n))
       (A : HiddenRule n bits) : Prop :=
   …

   Mentions: OAI.MatroidProphet.HiddenRule