OAI/Probability/MatroidSecretary/Selection/CandidateContract.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatroidProphet.SourceContracts.roundedWeight_pos_iff line 10

   Source documentation

   Positive rounding does not remove a positive weight or create one at zero.

   theorem roundedWeight_pos_iff {B x : ℝ} (hB : 0 < B) :
       0 < roundedWeight B x ↔ 0 < x := by
   …

   Mentions: OAI.MatroidProphet.roundedWeight

2. theorem OAI.MatroidProphet.SourceContracts.mem_candidateLabels_iff line 21

   Source documentation

   The actual candidate test is exactly eq:candidates, with higher rounded levels taking priority and the original fixed label order breaking ties.

   theorem mem_candidateLabels_iff {n : ℕ} (M : Matroid (Fin n))
       (w : Weights n) (B : ℝ) (H : Finset (Fin n)) (e : Fin n) :
       e ∈ candidateLabels M (fun f => roundedLevel B (w f)) H ↔
         0 < w e ∧ e ∉ H ∧
           e ∉ M.closure {f | f ∈ H ∧
             higher f (roundedLevel B (w f)) e (roundedLevel B (w e))} := by
   …

   Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.roundedLevel

3. theorem OAI.MatroidProphet.SourceContracts.mem_candidateLabels_iff_rounded line 39

   Source documentation

   The same test in the source's literal u_e > 0 notation.

   theorem mem_candidateLabels_iff_rounded {n : ℕ} (M : Matroid (Fin n))
       (w : Weights n) {B : ℝ} (hB : 0 < B) (H : Finset (Fin n)) (e : Fin n) :
       e ∈ candidateLabels M (fun f => roundedLevel B (w f)) H ↔
         0 < roundedWeight B (w e) ∧ e ∉ H ∧
           e ∉ M.closure {f | f ∈ H ∧
             higher f (roundedLevel B (w f)) e (roundedLevel B (w e))} := by
   …

   Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.roundedLevel, OAI.MatroidProphet.roundedWeight

4. theorem OAI.MatroidProphet.SourceContracts.candidateLabels_nonloop line 49

   Source documentation

   Candidates cannot be loops, including when loops have positive weights.

   theorem candidateLabels_nonloop {n : ℕ} (M : Matroid (Fin n))
       (a : Fin n → Option ℤ) (H : Finset (Fin n)) (e : Fin n)
       (he : e ∈ candidateLabels M a H) : e ∉ M.closure ∅ := by
   …

5. theorem OAI.MatroidProphet.SourceContracts.candidate_mass line 58

   Source documentation

   Both deterministic assertions and both expectation assertions in lem:filter. The assumptions include no positive-rank, nonempty-ground, or no-ties condition.

   theorem candidate_mass {n : ℕ} (M : Matroid (Fin n)) (hE : M.E = Set.univ)
       (w : Weights n) (_hw : ∀ e, 0 ≤ w e) {B : ℝ} (hB : 1 < B) :
       (∀ H : Finset (Fin n),
         M.Indep ((positiveGreedy M (fun e => roundedLevel B (w e)) \ H :
           Finset (Fin n)) : Set (Fin n)) ∧
         positiveGreedy M (fun e => roundedLevel B (w e)) \ H ⊆
           candidateLabels M (fun e => roundedLevel B (w e)) H) ∧
       bitsExpectation (fun _ => (1 / 2 : ℝ)) Finset.univ
         (fun H => ∑ e ∈ positiveGreedy M (fun e => roundedLevel B (w e)) \ H,
           roundedWeight B (w e)) = optimum M (fun e => roundedWeight B (w e)) / 2 ∧
       bitsExpectation (fun _ => (1 / 2 : ℝ)) Finset.univ
         (fun H => ∑ e ∈ candidateLabels M (fun e => roundedLevel B (w e)) H,
   …

   Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.roundedLevel, OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.roundedWeight, OAI.MatroidProphet.optimum

6. theorem OAI.MatroidProphet.SourceContracts.optimum_rounding line 78

   Source documentation

   The two-sided optimum rounding estimate eq:rounding, including zero weights.

   theorem optimum_rounding {n : ℕ} (M : Matroid (Fin n))
       (w : Weights n) (hw : ∀ e, 0 ≤ w e) {B : ℝ} (hB : 1 < B) :
       optimum M w / B ≤ optimum M (fun e => roundedWeight B (w e)) ∧
         optimum M (fun e => roundedWeight B (w e)) ≤ optimum M w := by
   …

   Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum, OAI.MatroidProphet.roundedWeight