ZeroBenchmark.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MatroidProphet.ZeroBenchmark.optimum_congr_on_singletons line 13
Source documentation
Only singleton-independent labels can affect the offline optimum. No sign or integrability assumption is necessary for this identity.
```
theorem optimum_congr_on_singletons {n : ℕ} (M : Matroid (Fin n))
    (w v : Weights n)
    (h : ∀ e, M.Indep ({e} : Set (Fin n)) → w e = v e) :
    optimum M w = optimum M v := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.ZeroBenchmark.optimum_zero line 29
Source documentation
The zero-weight benchmark is zero, also for empty or rank-zero matroids.
```
@[simp] theorem optimum_zero {n : ℕ} (M : Matroid (Fin n)) :
    optimum M (fun _ => 0) = 0 := by
…
```
Mentions: OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.ZeroBenchmark.optimum_eq_zero_iff line 36
Source documentation
On nonnegative inputs, a zero benchmark is exactly the condition that every label that could be accepted on its own has zero weight.
```
theorem optimum_eq_zero_iff {n : ℕ} (M : Matroid (Fin n))
    (w : Weights n) (hw : ∀ e, 0 ≤ w e) :
    optimum M w = 0 ↔ ∀ e, M.Indep ({e} : Set (Fin n)) → w e = 0 := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.ZeroBenchmark.optimum_ignore_infeasible_coordinates line 50
Source documentation
Replacing all loop coordinates by zero never changes the objective. Here ground-set outsiders, if any, are also harmless.
```
theorem optimum_ignore_infeasible_coordinates {n : ℕ} (M : Matroid (Fin n))
    (w : Weights n) :
    optimum M (fun e => if M.Indep ({e} : Set (Fin n)) then w e else 0) =
      optimum M w := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.ZeroBenchmark.optimum_eq_zero_of_no_independent_singleton line 60
Source documentation
Rank-zero behavior needs no bound at all on the values of its labels.
```
theorem optimum_eq_zero_of_no_independent_singleton {n : ℕ}
    (M : Matroid (Fin n))
    (hM : ∀ e, ¬ M.Indep ({e} : Set (Fin n))) (w : Weights n) :
    optimum M w = 0 := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.ZeroBenchmark.optimum_empty line 68
Source documentation
The empty instance has the zero benchmark without a positive-size premise.
```
@[simp] theorem optimum_empty (M : Matroid (Fin 0)) (w : Weights 0) :
    optimum M w = 0 := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.ZeroBenchmark.hiddenReward_eq_zero line 75
Source documentation
Every feasible realized hidden reward vanishes when the benchmark does.
```
theorem hiddenReward_eq_zero {n bits : ℕ} (M : Matroid (Fin n))
    (A : HiddenRule n bits) (r : Seed bits) (w : Weights n)
    (π : ArrivalOrder n) (hw : ∀ e, 0 ≤ w e)
    (hA : M.Indep (hiddenAcceptedThrough A r w π n : Set (Fin n)))
    (hopt : optimum M w = 0) : hiddenReward A r w π = 0 := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough, OAI.MatroidProphet.optimum, OAI.MatroidProphet.hiddenReward
theorem OAI.MatroidProphet.ZeroBenchmark.hiddenWorstReward_eq_zero line 86
Source documentation
The zero-benchmark conclusion also holds for the minimum taken separately at each complete seed, before any expectation.
```
theorem hiddenWorstReward_eq_zero {n bits : ℕ} (M : Matroid (Fin n))
    (A : HiddenRule n bits) (w : Weights n) (hw : ∀ e, 0 ≤ w e)
    (hA : ∀ r π, M.Indep (hiddenAcceptedThrough A r w π n : Set (Fin n)))
    (hopt : optimum M w = 0) (r : Seed bits) :
    hiddenWorstReward A w r = 0 := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.hiddenAcceptedThrough, OAI.MatroidProphet.optimum, OAI.MatroidProphet.Seed, OAI.MatroidProphet.hiddenWorstReward
theorem OAI.MatroidProphet.ZeroBenchmark.integral_hiddenWorstReward_eq_zero line 97
Source documentation
No probability-law or moment premise is needed in the zero case.
```
theorem integral_hiddenWorstReward_eq_zero {n bits : ℕ} (M : Matroid (Fin n))
    (A : HiddenRule n bits) (w : Weights n) (hw : ∀ e, 0 ≤ w e)
    (hA : ∀ r π, M.Indep (hiddenAcceptedThrough A r w π n : Set (Fin n)))
    (hopt : optimum M w = 0) (ν : Measure (Seed bits)) :
    (∫ r, hiddenWorstReward A w r ∂ν) = 0 := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.hiddenAcceptedThrough, OAI.MatroidProphet.optimum, OAI.MatroidProphet.Seed, OAI.MatroidProphet.hiddenWorstReward
theorem OAI.MatroidProphet.ZeroBenchmark.integrable_optimum_of_usable_coordinates_zero line 107
Source documentation
Even completely unrestricted loop coordinates cannot create a moment requirement when the usable coordinates vanish almost everywhere.
```
theorem integrable_optimum_of_usable_coordinates_zero {n : ℕ}
    (M : Matroid (Fin n)) {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) (V : Ω → Weights n)
    (hV : ∀ᵐ ω ∂μ, ∀ e, M.Indep ({e} : Set (Fin n)) → V ω e = 0) :
    Integrable (fun ω => optimum M (V ω)) μ := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.ZeroBenchmark.integral_optimum_of_usable_coordinates_zero line 119