DegenerateCases.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exceptional inputs for the actual secretary execution

These lemmas specialize the canonical history-only secretary model. They do not assume a conditional-mask coupling and do not replace the competitive theorem. All pointwise statements hold for every complete initial seed, including seeds outside the support of a chosen probability law.

theorem OAI.MatroidProphet.ZeroBenchmark.secretaryReward_eq_zero line 20
Source documentation
A feasible secretary rule has zero realized reward whenever actual OPT is zero.
```
theorem secretaryReward_eq_zero {n : ℕ} {Q : Type*} [MeasurableSpace Q]
    (M : Matroid (Fin n)) (A : SecretaryRule n Q) (hA : SecretaryFeasible M A)
    (q : Q) (w : Weights n) (hw : ∀ e, 0 ≤ w e) (π : ArrivalOrder n)
    (hopt : optimum M w = 0) : secretaryReward A q w π = 0 := by
…
```
Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.SecretaryFeasible, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.optimum, OAI.MatroidProphet.secretaryReward

theorem OAI.MatroidProphet.ZeroBenchmark.integrable_secretaryReward_of_optimum_zero line 29

Source documentation

There is no moment or independence condition in the zero-benchmark case.

theorem integrable_secretaryReward_of_optimum_zero {n : ℕ} {Q Ω : Type*}
    [MeasurableSpace Q] [MeasurableSpace Ω]
    (M : Matroid (Fin n)) (A : SecretaryRule n Q) (hA : SecretaryFeasible M A)
    (w : Weights n) (hw : ∀ e, 0 ≤ w e) (hopt : optimum M w = 0)
    (μ : Measure Ω) (q : Ω → Q) (π : Ω → ArrivalOrder n) :
    Integrable (fun ω => secretaryReward A (q ω) w (π ω)) μ := by
…

Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.SecretaryFeasible, OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.secretaryReward

theorem OAI.MatroidProphet.ZeroBenchmark.integral_secretaryReward_of_optimum_zero line 39

Source documentation

Even an arbitrary full-seed-aware order has zero expected reward at zero OPT.

theorem integral_secretaryReward_of_optimum_zero {n : ℕ} {Q Ω : Type*}
    [MeasurableSpace Q] [MeasurableSpace Ω]
    (M : Matroid (Fin n)) (A : SecretaryRule n Q) (hA : SecretaryFeasible M A)
    (w : Weights n) (hw : ∀ e, 0 ≤ w e) (hopt : optimum M w = 0)
    (μ : Measure Ω) (q : Ω → Q) (π : Ω → ArrivalOrder n) :
    (∫ ω, secretaryReward A (q ω) w (π ω) ∂μ) = 0 := by
…

theorem OAI.MatroidProphet.ZeroBenchmark.secretaryAcceptedThrough_eq_empty_of_full_prefix line 49
Source documentation
A fully sacrificed instance never accepts, even after the last arrival.
```
theorem secretaryAcceptedThrough_eq_empty_of_full_prefix {n : ℕ} {Q : Type*}
    [MeasurableSpace Q] (A : SecretaryRule n Q) (q : Q)
    (hfull : (A.prefixLength q).val = n) (w : Weights n)
    (π : ArrivalOrder n) (t : ℕ) : secretaryAcceptedThrough A q w π t = ∅ := by
…
```
Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.secretaryAcceptedThrough
theorem OAI.MatroidProphet.ZeroBenchmark.secretaryReward_eq_zero_of_full_prefix line 60
Source documentation
Full-prefix sacrifice forces zero reward without feasibility or sign assumptions.
```
theorem secretaryReward_eq_zero_of_full_prefix {n : ℕ} {Q : Type*}
    [MeasurableSpace Q] (A : SecretaryRule n Q) (q : Q)
    (hfull : (A.prefixLength q).val = n) (w : Weights n)
    (π : ArrivalOrder n) : secretaryReward A q w π = 0 := by
…
```
Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.secretaryReward
theorem OAI.MatroidProphet.ZeroBenchmark.secretaryAcceptedThrough_empty line 67
Source documentation
Empty-ground execution is defined and empty for every seed and time.
```
theorem secretaryAcceptedThrough_empty {Q : Type*} [MeasurableSpace Q]
    (A : SecretaryRule 0 Q) (q : Q) (w : Weights 0)
    (π : ArrivalOrder 0) (t : ℕ) : secretaryAcceptedThrough A q w π t = ∅ := by
…
```
Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.secretaryAcceptedThrough
theorem OAI.MatroidProphet.ZeroBenchmark.secretaryReward_empty line 75
Source documentation
Empty-ground reward is identically zero, with no positive-size premise.
```
theorem secretaryReward_empty {Q : Type*} [MeasurableSpace Q]
    (A : SecretaryRule 0 Q) (q : Q) (w : Weights 0)
    (π : ArrivalOrder 0) : secretaryReward A q w π = 0 := by
…
```
Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.secretaryReward