CandidateSpecificationTheorems.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Correspondence of the independent source definitions with the implemented candidate filter and positive priority-greedy, followed by the source contract.

lemma OAI.MatroidProphet.CandidateSpecification.higher_eq_main line 13
lemma OAI.MatroidProphet.CandidateSpecification.candidates_eq_main line 17
lemma OAI.MatroidProphet.CandidateSpecification.greedy_eq_main line 32
lemma OAI.MatroidProphet.CandidateSpecification.survivors_eq_main line 45
theorem OAI.MatroidProphet.CandidateSpecification.candidateMass line 52
lemma OAI.MatroidProphet.CandidateSpecification.candidate_membership_congr line 59
Source documentation
Candidate membership uses only the focal key and keys on the revealed mask, never another unobserved label's key.
```
lemma candidate_membership_congr {n : ℕ} (M : Matroid (Fin n))
    (a a' : Fin n → Option ℤ) (H : Finset (Fin n)) (e : Fin n)
    (he : a e = a' e) (hH : ∀ f ∈ H, a f = a' f) :
    e ∈ candidates M a H ↔ e ∈ candidates M a' H := by
…
```
Mentions: OAI.MatroidProphet.CandidateSpecification.candidates
theorem OAI.MatroidProphet.CandidateSpecification.source_rounding_and_greedy line 76
Source documentation
The source greedy definition really attains rounded OPT, with the source's rounding comparison on both sides. This verifies the ancillary input I* rather than assuming its optimality.
```
theorem source_rounding_and_greedy {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (w : Weights n) (hw : ∀ e, 0 ≤ w e) :
    let u := fun e => roundedWeight weightBase (w e)
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.roundedWeight, OAI.MatroidProphet.weightBase