SharpCost.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Retaining the density-mask rate in the accounting budget

In accounting.tex immediately after eq:expected-cost, the manuscript notes that the exact density-mask contribution is 1 / (4 * κ), although the proof uses the more generous 1 / κ. This supplement proves that sharper inequality for the actual zero-extended cost, without conditioning on random listing.

theorem OAI.MatroidProphet.AccountingContracts.listedCost_le_sampled_true_counts line 19

Source documentation

Keep the sampled higher-group density count until after expectation.

theorem listedCost_le_sampled_true_counts (M : Matroid (Fin n)) (d : MainMasks n)
    (w : Fin n → Option ℤ) {h : ℕ} {i : ℤ}
    (hi : (groups M d w)[h]? = some i) :
    listedCost M d w h ≤
      (d.C ∩ trueGroup M d w i).card +
        (d.C ∩ higherTrueGroups M d w i).card +
          (d.D ∩ higherTrueGroups M d w i).card / densityThreshold := by
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.AccountingContracts.listedCost, OAI.MatroidProphet.densityThreshold

lemma OAI.MatroidProphet.AccountingContracts.mainMean_density_count line 51
Source documentation
The density mask is averaged at its original rate, independently of H.
```
lemma mainMean_density_count (d : MainMasks n) (K : Finset (Fin n)) :
    mainMean d (fun d' => ((d'.D ∩ K).card : ℝ)) = (1 / 4 : ℝ) * K.card := by
…
```
Mentions: OAI.MatroidProphet.MainMasks
lemma OAI.MatroidProphet.AccountingContracts.mainMean_div line 59

theorem OAI.MatroidProphet.AccountingContracts.trueCost_le_sampled_true_counts line 64

Source documentation

Listing is not a conditioning event: unlisted true groups have cost zero.

theorem trueCost_le_sampled_true_counts (M : Matroid (Fin n)) (d : MainMasks n)
    (w : Fin n → Option ℤ) (i : ℤ) :
    trueCost M d w i ≤
      (d.C ∩ trueGroup M d w i).card +
        (d.C ∩ higherTrueGroups M d w i).card +
          (d.D ∩ higherTrueGroups M d w i).card / densityThreshold := by
…

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

theorem OAI.MatroidProphet.AccountingContracts.expected_cost_sharp line 78
Source documentation
Source's sharper density contribution before relaxing 1/(4κ) to 1/κ.
```
theorem expected_cost_sharp (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 / (4 * 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_sharp_sum line 97

Source documentation

The equivalent finite sum over all higher true levels, listed or not.

theorem expected_cost_sharp_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 / (4 * 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