OAI/Probability/MatroidSecretary/Selection/AssignedSafe.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatroidProphet.safeSampleCount_half_loss line 13

   Source documentation

   The stronger half-loss estimate explicitly obtained in the source proof. The named lemma then enlarges the loss from |D_h|/(2κ) to |D_h|/κ.

   theorem safeSampleCount_half_loss
       (M : Matroid α) (hE : M.E = Set.univ)
       (κ : ℕ) (hκ : 0 < κ) (D : ℕ → Set α) (G : ℕ → Finset α)
       (hG : Pairwise (fun i j => Disjoint (G i) (G j)))
       (q : α → ℝ) (hq0 : ∀ e, 0 ≤ q e) (hq1 : ∀ e, q e ≤ 1)
       (h : ℕ) (I : Finset α) (hI : M.Indep (I : Set α)) :
       (((2 : ℝ) ^ 12)⁻¹) / 4 * I.card - (D h).ncard / (2 * (κ : ℝ)) ≤
         bitsExpectation q univ (fun C => bitsExpectation q univ (fun T =>
           fairParityExpectation (safeSampleCount M hE κ D G h I C T))) := by
   …

   Mentions: OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.fairParityExpectation, OAI.MatroidProphet.safeSampleCount

2. theorem OAI.MatroidProphet.MainAlgorithm.listedSafeStatistic_exact_density line 44

   Source documentation

   The fixed-density safety estimate with the exact density-sample loss.

   theorem listedSafeStatistic_exact_density
       (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) :
       exitThreshold / 4 * ((d.D : Set (Fin n)) ∩ Y).ncard -
           (d.D ∩ trueGroup M d s i).card / (κ : ℝ) ≤
         bitsExpectation q univ (fun C => bitsExpectation q univ (fun T =>
           fairParityExpectation (fun p =>
             (listedSafeStatistic M hE κ (withMasks d d.D C T) s i Y
               (boolParity p) : ℝ)))) := by
   …

   Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.trueGroup, OAI.MatroidProphet.exitThreshold, OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.fairParityExpectation, OAI.MatroidProphet.MainAlgorithm.listedSafeStatistic, OAI.MatroidProphet.MainAlgorithm.withMasks, OAI.MatroidProphet.boolParity

3. theorem OAI.MatroidProphet.MainAlgorithm.listedSafeStatistic_inter_trueGroup line 78

   Source documentation

   Restricting the comparison set to this true group does not change its safe-label statistic. This permits the source's global independent set Y.

   theorem listedSafeStatistic_inter_trueGroup
       (M : Matroid (Fin n)) (hE : M.E = Set.univ) (κ : ℕ)
       (d : MainMasks n) (s : Fin n → Option ℤ) (i : ℤ)
       (Y : Set (Fin n)) (ε : Fin 2) :
       listedSafeStatistic M hE κ d s i
         (Y ∩ (trueGroup M d s i : Set (Fin n))) ε =
         listedSafeStatistic M hE κ d s i Y ε := by
   …

   Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.listedSafeStatistic, OAI.MatroidProphet.MainAlgorithm.trueGroup

4. theorem OAI.MatroidProphet.MainAlgorithm.safe_sampled_labels line 103

   Source documentation

   Source lem:safe, specialized to the manuscript's literal density threshold and thinning rate, for the global independent comparison set. It also covers an unlisted group, whose safe count is defined to be zero.

   theorem 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) :
       exitThreshold / 4 *
           ((d.D : Set (Fin n)) ∩ (Y ∩ (trueGroup M d s i : Set (Fin n)))).ncard -
           (d.D ∩ trueGroup M d s i).card / densityThreshold ≤
         bitsExpectation (fun _ => thinningRate) univ (fun C =>
           bitsExpectation (fun _ => thinningRate) univ (fun T =>
             fairParityExpectation (fun p =>
               (listedSafeStatistic M hE (2 ^ 100) (withMasks d d.D C T) s i Y
                 (boolParity p) : ℝ)))) := by
   …

   Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.exitThreshold, OAI.MatroidProphet.MainAlgorithm.trueGroup, OAI.MatroidProphet.densityThreshold, OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.thinningRate, OAI.MatroidProphet.fairParityExpectation, OAI.MatroidProphet.MainAlgorithm.listedSafeStatistic, OAI.MatroidProphet.MainAlgorithm.withMasks, OAI.MatroidProphet.boolParity

5. theorem OAI.MatroidProphet.MainAlgorithm.safe_sampled_labels_claim line 131

   Source documentation

   Proof of the independently stated complete safe-label claim.

   theorem safe_sampled_labels_claim : SafeSampleClaim := by
   …

   Mentions: OAI.MatroidProphet.SafeSampleClaim