OAI/Combinatorics/SharpThreshold/BlockCounting.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem313.blockProbability line 16

   Source documentation

   Probability of an event for a uniformly chosen fixed-size subset.

   def blockProbability (U : Finset α) (m : ℕ) (P : Finset α → Prop) : ℝ := by
   …

2. theorem OAI.Problem313.blockProbability_eq line 21
3. theorem OAI.Problem313.blockProbability_nonneg line 28
4. theorem OAI.Problem313.blockProbability_mono line 34
5. theorem OAI.Problem313.blockProbability_mem_count line 47
6. theorem OAI.Problem313.choose_pred_ratio line 55
7. theorem OAI.Problem313.blockProbability_mem line 68
8. theorem OAI.Problem313.blockProbability_pair_count line 75
9. theorem OAI.Problem313.choose_two_pred_ratio line 82
10. theorem OAI.Problem313.blockProbability_pair line 103
11. theorem OAI.Problem313.blockProbability_congr line 114
12. theorem OAI.Problem313.blockProbability_false line 123
13. theorem OAI.Problem313.blockProbability_or_le line 127
14. theorem OAI.Problem313.blockProbability_exists_le line 138
15. theorem OAI.Problem313.blockProbability_avoid_ge line 154
16. theorem OAI.Problem313.inter_eq_singleton_iff_mem_avoid line 173
17. theorem OAI.Problem313.blockProbability_singleton_inter_ge line 196

    Source documentation

    A union bound conditioned on containing a specified vertex.

    theorem blockProbability_singleton_inter_ge (U V : Finset α) {m : ℕ} {u : α}
        (hVU : V ⊆ U) (hu : u ∈ V) (hm : 2 ≤ m) (hmn : m ≤ U.card) :
        (m : ℝ) / U.card *
            (1 - ((V.card : ℝ) - 1) * ((m : ℝ) - 1) / ((U.card : ℝ) - 1)) ≤
          blockProbability U m (fun B => B ∩ V = {u}) := by
    …

    Mentions: OAI.Problem313.blockProbability

18. theorem OAI.Problem313.blockProbability_inter_nonempty_le line 228

    Source documentation

    At most the sum of the individual inclusion probabilities can touch a fixed set.

    theorem blockProbability_inter_nonempty_le (U E : Finset α) {m : ℕ}
        (hEU : E ⊆ U) (hm : 1 ≤ m) (hmn : m ≤ U.card) :
        blockProbability U m (fun B => (B ∩ E).Nonempty) ≤
          (E.card : ℝ) * m / U.card := by
    …

    Mentions: OAI.Problem313.blockProbability

19. theorem OAI.Problem313.blockProbability_edge_touch_le line 248

    Source documentation

    The graph-edge touch bound used when averaging the block restriction.

    theorem blockProbability_edge_touch_le (U E : Finset α) {m : ℕ}
        (hEU : E ⊆ U) (hE : E.card = 2) (hm : 1 ≤ m) (hmn : m ≤ U.card) :
        blockProbability U m (fun B => (B ∩ E).Nonempty) ≤ (2 : ℝ) * m / U.card := by
    …

    Mentions: OAI.Problem313.blockProbability

20. theorem OAI.Problem313.blockProbability_singleton_inter_ge_half line 254

    Source documentation

    Collision estimate reduced to a half yields the usual capture lower bound.

    theorem blockProbability_singleton_inter_ge_half (U V : Finset α) {m : ℕ} {u : α}
        (hVU : V ⊆ U) (hu : u ∈ V) (hm : 2 ≤ m) (hmn : m ≤ U.card)
        (hcollision : ((V.card : ℝ) - 1) * ((m : ℝ) - 1) / ((U.card : ℝ) - 1) ≤ 1 / 2) :
        (m : ℝ) / (2 * U.card) ≤ blockProbability U m (fun B => B ∩ V = {u}) := by
    …

    Mentions: OAI.Problem313.blockProbability