MaximumWeighted.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The literal rounded-payoff maximum-branch claim eq:maximum in setup.tex. The observed input stays w; only the score attached to an accepted label is rounded. This distinguishes the source assertion from a raw-payoff bound.

lemma OAI.MatroidProphet.hiddenWorstScore_nonneg line 14
lemma OAI.MatroidProphet.Maximum.maximumHidden_accepted_single_qualifier line 29
Source documentation
A singleton qualifier gives the actual singleton accepted set, not just its raw reward. Therefore every nonnegative scoring of labels can use this event.
```
lemma maximumHidden_accepted_single_qualifier (M : Matroid (Fin n))
    (key : ℝ → K) (hkey : Measurable key) (active : K → Prop)
    (mask : Seed bits → Finset (Fin n)) (w : Weights n) (r : Seed bits) (g : Fin n)
    (hg : g ∉ mask r)
    (ha : ∀ e, threshold M active mask r (fun f => key (w f)) (e, key (w e)) ↔ e = g)
    (π : ArrivalOrder n) :
    hiddenAcceptedThrough (maximumHidden M key hkey active mask) r w π n = {g} := by
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.Maximum.threshold, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough, OAI.MatroidProphet.Maximum.maximumHidden

theorem OAI.MatroidProphet.Maximum.maximum_expectation_top_score line 52

Source documentation

The all-order top-label guarantee remains valid for any nonnegative score vector, while decisions still use exactly the original observations.

theorem maximum_expectation_top_score (M : Matroid (Fin n))
    (key : ℝ → K) (hkey : Measurable key) (active : K → Prop)
    (w score : Weights n) (hscore : ∀ e, 0 ≤ score e) (g : Fin n)
    (hg : M.Indep ({g} : Set (Fin n))) (hag : active (key (w g)))
    (htop : ∀ f, M.Indep ({f} : Set (Fin n)) → active (key (w f)) → f ≠ g →
      higher (g, key (w g)) (f, key (w f))) :
    score g / 4 ≤ bitsExpectation (fun _ => (1 / 2 : ℝ)) Finset.univ
      (fun H => hiddenWorstScore
        (maximumHidden M key hkey active (seedSet (bits := n))) w score (setSeed H)) := by
…

Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.Maximum.higher, OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.hiddenWorstScore, OAI.MatroidProphet.Maximum.maximumHidden, OAI.MatroidProphet.seedSet, OAI.MatroidProphet.setSeed

theorem OAI.MatroidProphet.SourceContracts.maximum_rounded line 107
Source documentation
The literal source eq:maximum: expected minimum rounded reward of the maximum branch is at least one quarter of the largest rounded nonloop. The observation mask is fair on every label and the minimum stays inside the expectation. Empty, rank-zero, and all-zero instances are included.
```
theorem maximum_rounded {n : ℕ} (M : Matroid (Fin n)) (w : Weights n)
    (_hw : ∀ e, 0 ≤ w e) :
    maximumRounded M w / 4 ≤
      ∫ r, hiddenWorstScore (roundedMaximumHidden M (seedSet (bits := n)))
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.maximumRounded, OAI.MatroidProphet.hiddenWorstScore, OAI.MatroidProphet.roundedMaximumHidden, OAI.MatroidProphet.seedSet