ExpectedCost.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The literal conditional cost inequality eq:expected-cost. The cost is zero on an unlisted true group; listing is never conditioned upon.

def OAI.MatroidProphet.AccountingContracts.listedCost line 15
Source documentation
The single path-expansion budget of a listed group, with its real-valued density contribution.
```
noncomputable def listedCost (M : Matroid (Fin n)) (d : MainMasks n)
    (w : Fin n → Option ℤ) (h : ℕ) : ℝ :=
…
```
Mentions: OAI.MatroidProphet.MainMasks
def OAI.MatroidProphet.AccountingContracts.trueCost line 23
Source documentation
The source's c_i, extended by zero to unlisted true groups.
```
noncomputable def trueCost (M : Matroid (Fin n)) (d : MainMasks n)
    (w : Fin n → Option ℤ) (i : ℤ) : ℝ := by
…
```
Mentions: OAI.MatroidProphet.MainMasks
theorem OAI.MatroidProphet.AccountingContracts.listedCost_le_true_counts line 28
theorem OAI.MatroidProphet.AccountingContracts.trueCost_le_true_counts line 69
theorem OAI.MatroidProphet.AccountingContracts.expected_cost line 85
Source documentation
Conditional on H, the actual randomly listed cost is dominated before averaging. The higher-group cardinality is the sum over all higher true groups, including those that the density mask did not list.
```
theorem expected_cost (M : Matroid (Fin n)) (d : MainMasks n)
    (w : Fin n → Option ℤ) (i : ℤ) :
    mainMean d (fun d' => trueCost M d' w i) ≤
      thinningRate * (trueGroup M d w i).card +
        (thinningRate + 1 / densityThreshold) * (higherTrueGroups M d w i).card := by
…
```
Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.AccountingContracts.trueCost, OAI.MatroidProphet.thinningRate, OAI.MatroidProphet.densityThreshold

theorem OAI.MatroidProphet.AccountingContracts.expected_cost_sum line 104

Source documentation

Exact finite true-level sum presentation of eq:expected-cost.

theorem expected_cost_sum (M : Matroid (Fin n)) (d : MainMasks n)
    (w : Fin n → Option ℤ) (i : ℤ) :
    mainMean d (fun d' => trueCost M d' w i) ≤
      thinningRate * (trueGroup M d w i).card +
        (thinningRate + 1 / densityThreshold) *
          ∑ j ∈ trueLevels M w d.H with i < j, ((trueGroup M d w j).card : ℝ) := by
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.AccountingContracts.trueCost, OAI.MatroidProphet.thinningRate, OAI.MatroidProphet.densityThreshold