OAI/Probability/MatroidSecretary/Contracts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatroidProphet.Assigned.one_sample line 49

   Distinct definitions of this name: ComparatorChallenges/MatroidSecretary.lean:235 (same statement text; different proof or body). Qualify references as OAI.MatroidProphet.Assigned.one_sample@path.

2. theorem OAI.MatroidProphet.Assigned.hidden_vector line 52

   Distinct definitions of this name: ComparatorChallenges/MatroidSecretary.lean:238 (same statement text; different proof or body). Qualify references as OAI.MatroidProphet.Assigned.hidden_vector@path.

3. theorem OAI.MatroidProphet.Assigned.filter line 56

   Source documentation

   Source lem:filter: actual priority-greedy survivors and candidate mass.

   theorem filter : MatroidProphet.CandidateSpecification.CandidateMass := MatroidProphet.CandidateSpecification.candidateMass

   Mentions: OAI.MatroidProphet.CandidateSpecification.CandidateMass, OAI.MatroidProphet.CandidateSpecification.candidateMass

4. theorem OAI.MatroidProphet.Assigned.density line 59

   Source documentation

   Source lem:density: concrete largest optimizer and its residual bound.

   theorem density {α : Type*} [Fintype α] (M : Matroid α)
       (hE : M.E = Set.univ) (κ : ℕ) (D : Set α) :
       DensityExpansionContract M hE κ D := source_density_expansion M hE κ D

   Mentions: OAI.MatroidProphet.DensityExpansionContract, OAI.MatroidProphet.source_density_expansion

5. theorem OAI.MatroidProphet.Assigned.paths line 64

   Source documentation

   Source lem:paths: the full integer timeline, including least births.

   theorem paths {α : Type*} [Fintype α] (M : Matroid α)
       (hE : M.E = Set.univ) (κ : ℕ) (D C : ℕ → Set α) :
       PathPropertiesContract M hE κ D C := source_path_properties M hE κ D C

   Mentions: OAI.MatroidProphet.PathPropertiesContract, OAI.MatroidProphet.source_path_properties

6. theorem OAI.MatroidProphet.Assigned.generators line 69

   Source documentation

   Source lem:generators: one increasing generator family and one total budget.

   theorem generators {α : Type*} [Fintype α] (M : Matroid α)
       (hE : M.E = Set.univ) (κ : ℕ) (hκ : 0 < κ) (D C : ℕ → Set α) :
       GeneratorBudgetContract M hE κ D C := source_generator_budget M hE κ hκ D C

   Mentions: OAI.MatroidProphet.GeneratorBudgetContract, OAI.MatroidProphet.source_generator_budget

7. theorem OAI.MatroidProphet.Assigned.all_orders line 73
8. theorem OAI.MatroidProphet.Assigned.rank_cost line 88
9. theorem OAI.MatroidProphet.Assigned.exit line 101
10. theorem OAI.MatroidProphet.Assigned.secretary line 118

    Distinct definitions of this name: ComparatorChallenges/MatroidSecretary.lean:241 (same statement text; different proof or body). Qualify references as OAI.MatroidProphet.Assigned.secretary@path.

11. theorem OAI.MatroidProphet.Assigned.simulation line 121
12. theorem OAI.MatroidProphet.Assigned.feasibility line 123
13. theorem OAI.MatroidProphet.Assigned.safe line 126
14. theorem OAI.MatroidProphet.Assigned.pivot_patterns line 128
15. theorem OAI.MatroidProphet.Assigned.pattern_family line 130
16. theorem OAI.MatroidProphet.Assigned.transfer line 132
17. theorem OAI.MatroidProphet.Assigned.transactions line 134