OAI/Probability/MatroidSecretary/Accounting/StrictSmallGroups.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatroidProphet.sum_zpow_lt_two line 8
2. lemma OAI.MatroidProphet.sum_zpow_lt_two_of_pos_bound line 20
3. lemma OAI.MatroidProphet.small_group_mass_strict line 33
4. lemma OAI.MatroidProphet.maximumRounded_pos_of_optimum_pos line 46
5. lemma OAI.MatroidProphet.MainAlgorithm.small_comparison_mass_strict line 67

   Source documentation

   Exact strict version of the discarded-group bound in the positive-W case.

   lemma small_comparison_mass_strict {n : ℕ} (M : Matroid (Fin n))
       (hE : M.E = Set.univ) (w : Weights n) (H : Finset (Fin n))
       (hW : 0 < optimum M (fun e => roundedWeight weightBase (w e))) :
       comparisonMass M (fun e => roundedLevel weightBase (w e)) H <
         analyzedComparisonMass M (fun e => roundedLevel weightBase (w e)) H +
           2 * densityThreshold * maximumRounded M w := by
   …

   Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum, OAI.MatroidProphet.roundedWeight, OAI.MatroidProphet.weightBase, OAI.MatroidProphet.MainAlgorithm.comparisonMass, OAI.MatroidProphet.roundedLevel, OAI.MatroidProphet.MainAlgorithm.analyzedComparisonMass, OAI.MatroidProphet.densityThreshold, OAI.MatroidProphet.maximumRounded