AveragedSafeExact.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exact density-averaged safety loss

This retains the first, sharper inequality in eq:averaged-safe-count (sections/transfer.tex, line 330). The density mask is averaged only after the exact conditional loss has been bounded by |D ∩ U_i| / κ. The previous endpoint route weakened this to |U_i| / κ before averaging, which suffices there but does not state the displayed |U_i| / (4κ) estimate.

The statistic remains zero on unlisted outcomes. No conditioning on listing, focal density bits, or an arrival order is introduced.

theorem OAI.MatroidProphet.MainAlgorithm.listedSafeStatistic_averaged_exact line 26

Source documentation

Literal first inequality of eq:averaged-safe-count, for a fixed true group and any independent comparison subset of that group.

theorem listedSafeStatistic_averaged_exact
    (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (κ : ℕ) (hκ : 0 < κ) (d : MainMasks n) (s : Fin n → Option ℤ) (i : ℤ)
    (Y : Set (Fin n)) (hY : Y ⊆ (trueGroup M d s i : Set (Fin n)))
    (hI : M.Indep Y) (q : Fin n → ℝ)
    (hq0 : ∀ e, 0 ≤ q e) (hq1 : ∀ e, q e ≤ 1) :
    retainedFraction * Y.ncard - (trueGroup M d s i).card / (4 * (κ : ℝ)) ≤
      tripleMaskExpectation (fun _ => (1 : ℝ) / 4) q q univ (fun D C T =>
        fairParityExpectation (fun p =>
          (listedSafeStatistic M hE κ (withMasks d D C T) s i Y
            (boolParity p) : ℝ))) := by
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.trueGroup, OAI.MatroidProphet.retainedFraction, OAI.MatroidProphet.tripleMaskExpectation, OAI.MatroidProphet.fairParityExpectation, OAI.MatroidProphet.MainAlgorithm.listedSafeStatistic, OAI.MatroidProphet.MainAlgorithm.withMasks, OAI.MatroidProphet.boolParity

theorem OAI.MatroidProphet.MainAlgorithm.averaged_safe_sampled_labels line 91
Source documentation
Source specialization for its global independent comparison set Y. The intersection appearing here is exactly the source's Y_i; all statistics are those of the actual density-dependent listed groups.
```
theorem averaged_safe_sampled_labels
    (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (d : MainMasks n) (s : Fin n → Option ℤ) (i : ℤ)
    (Y : Set (Fin n)) (hI : M.Indep Y) :
    retainedFraction * (Y ∩ (trueGroup M d s i : Set (Fin n))).ncard -
        (trueGroup M d s i).card / (4 * densityThreshold) ≤
      tripleMaskExpectation (fun _ => (1 : ℝ) / 4)
        (fun _ => thinningRate) (fun _ => thinningRate) univ (fun D C T =>
          fairParityExpectation (fun p =>
            (listedSafeStatistic M hE (2 ^ 100) (withMasks d D C T) s i Y
              (boolParity p) : ℝ))) := by
…
```
Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.retainedFraction, OAI.MatroidProphet.MainAlgorithm.trueGroup, OAI.MatroidProphet.densityThreshold, OAI.MatroidProphet.tripleMaskExpectation, OAI.MatroidProphet.thinningRate, OAI.MatroidProphet.fairParityExpectation, OAI.MatroidProphet.MainAlgorithm.listedSafeStatistic, OAI.MatroidProphet.MainAlgorithm.withMasks, OAI.MatroidProphet.boolParity