OAI/Combinatorics/GraphThreshold/SpreadCounting.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Exact intersection counting for a finite, weighted spread family.

No injectivity of the label map and no strict positivity of individual weights is required. The fixed target is an arbitrary finite set, and may be empty.

  1. theorem OAI.LeanBlast.SecondKahnKalai.IsSpread.containment_le line 24

    Source documentation

    The spread bound also holds for the empty test set, by normalization.

    theorem IsSpread.containment_le {μ : FiniteLaw B} {A : B → Finset X} {a : ℝ}
    (hs : IsSpread μ A a) (J : Finset X) :
    μ.prob (fun c => J ⊆ A c) ≤ a ^ J.card := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread

  2. theorem OAI.LeanBlast.SecondKahnKalai.intersection_card_ge_le_subsets line 35

    Source documentation

    If the intersection has at least r points, it contains an r-set from the target. This is the weighted finite union bound.

    theorem intersection_card_ge_le_subsets (μ : FiniteLaw B) (A : B → Finset X)
    (T : Finset X) (r : ℕ) :
    μ.prob (fun c => r ≤ (A c ∩ T).card) ≤
      ∑ J ∈ T.powersetCard r, μ.prob (fun c => J ⊆ A c) := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw

  3. theorem OAI.LeanBlast.SecondKahnKalai.intersection_card_ge_le_target line 66

    Source documentation

    Exact binomial count of potential witnesses bounds the intersection tail.

    theorem intersection_card_ge_le_target {μ : FiniteLaw B} {A : B → Finset X}
    {a : ℝ} (hs : IsSpread μ A a) (T : Finset X) (r : ℕ) :
    μ.prob (fun c => r ≤ (A c ∩ T).card) ≤
      (T.card.choose r : ℝ) * a ^ r := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread

  4. theorem OAI.LeanBlast.SecondKahnKalai.intersection_card_ge_le line 82

    Source documentation

    Uniform capacity version, including r = 0 and empty target sets.

    theorem intersection_card_ge_le {μ : FiniteLaw B} {A : B → Finset X}
    {a : ℝ} (hs : IsSpread μ A a) (ha : 0 ≤ a) {m : ℕ}
    {T : Finset X} (hT : T.card ≤ m) (r : ℕ) :
    μ.prob (fun c => r ≤ (A c ∩ T).card) ≤
      (m.choose r : ℝ) * a ^ r := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread

  5. theorem OAI.LeanBlast.SecondKahnKalai.intersection_card_eq_le line 92

    Source documentation

    The exact intersection histogram is bounded by the same binomial count.

    theorem intersection_card_eq_le {μ : FiniteLaw B} {A : B → Finset X}
    {a : ℝ} (hs : IsSpread μ A a) (ha : 0 ≤ a) {m : ℕ}
    {T : Finset X} (hT : T.card ≤ m) (r : ℕ) :
    μ.prob (fun c => (A c ∩ T).card = r) ≤
      (m.choose r : ℝ) * a ^ r := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread

  6. theorem OAI.LeanBlast.SecondKahnKalai.expectation_intersection_eq_sum line 108

    Source documentation

    Reindex any function of the intersection by the exact finite histogram.

    theorem expectation_intersection_eq_sum (μ : FiniteLaw B) (A : B → Finset X)
    {m : ℕ} {T : Finset X} (hT : T.card ≤ m) (g : ℕ → ℝ) :
    μ.expectation (fun c => g (A c ∩ T).card) =
      ∑ r ∈ Finset.range (m + 1),
        μ.prob (fun c => (A c ∩ T).card = r) * g r := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw

  7. theorem OAI.LeanBlast.SecondKahnKalai.expectation_intersection_le_binomial line 126

    Source documentation

    Any nonnegative function of the intersection admits a binomial majorant.

    theorem expectation_intersection_le_binomial {μ : FiniteLaw B} {A : B → Finset X}
    {a : ℝ} (hs : IsSpread μ A a) (ha : 0 ≤ a) {m : ℕ}
    {T : Finset X} (hT : T.card ≤ m) (g : ℕ → ℝ) (hg : ∀ r, 0 ≤ g r) :
    μ.expectation (fun c => g (A c ∩ T).card) ≤
      ∑ r ∈ Finset.range (m + 1), (m.choose r : ℝ) * a ^ r * g r := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread

  8. theorem OAI.LeanBlast.SecondKahnKalai.intersection_truncated_moment_le line 136

    Source documentation

    A predicate can truncate the intersection generating function arbitrarily.

    theorem intersection_truncated_moment_le {μ : FiniteLaw B} {A : B → Finset X}
    {a : ℝ} (hs : IsSpread μ A a) (ha : 0 ≤ a) {m : ℕ}
    {T : Finset X} (hT : T.card ≤ m) {t : ℝ} (ht : 0 ≤ t)
    (Q : ℕ → Prop) [DecidablePred Q] :
    μ.expectation (fun c => if Q (A c ∩ T).card then t ^ (A c ∩ T).card else 0) ≤
      ∑ r ∈ Finset.range (m + 1),
        if Q r then (m.choose r : ℝ) * (a * t) ^ r else 0 := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread

  9. theorem OAI.LeanBlast.SecondKahnKalai.intersection_truncated_sum_le line 156

    Source documentation

    Raw-sum form of the truncated moment estimate.

    theorem intersection_truncated_sum_le {μ : FiniteLaw B} {A : B → Finset X}
    {a : ℝ} (hs : IsSpread μ A a) (ha : 0 ≤ a) {m : ℕ}
    {T : Finset X} (hT : T.card ≤ m) {t : ℝ} (ht : 0 ≤ t)
    (Q : ℕ → Prop) [DecidablePred Q] :
    (∑ c, if Q (A c ∩ T).card then μ.weight c * t ^ (A c ∩ T).card else 0) ≤
      ∑ r ∈ Finset.range (m + 1),
        if Q r then (m.choose r : ℝ) * (a * t) ^ r else 0 := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread

  10. theorem OAI.LeanBlast.SecondKahnKalai.intersection_moment_le line 167

    Source documentation

    The full generating-function bound needs only a nonnegative argument.

    theorem intersection_moment_le {μ : FiniteLaw B} {A : B → Finset X}
    {a : ℝ} (hs : IsSpread μ A a) (ha : 0 ≤ a) {m : ℕ}
    {T : Finset X} (hT : T.card ≤ m) {t : ℝ} (ht : 0 ≤ t) :
    μ.expectation (fun c => t ^ (A c ∩ T).card) ≤ (1 + a * t) ^ m := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread

  11. theorem OAI.LeanBlast.SecondKahnKalai.intersection_inverse_moment_le line 182

    Source documentation

    Inverse-parameter moment used by the resampling density estimate.

    theorem intersection_inverse_moment_le {μ : FiniteLaw B} {A : B → Finset X}
    {a : ℝ} (hs : IsSpread μ A a) (ha : 0 ≤ a) {m : ℕ}
    {T : Finset X} (hT : T.card ≤ m) {ρ : ℝ} (hρ : 0 < ρ) :
    μ.expectation (fun c => (ρ⁻¹) ^ (A c ∩ T).card) ≤ (1 + a / ρ) ^ m := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread

  12. theorem OAI.LeanBlast.SecondKahnKalai.intersection_inverse_sum_le line 190

    Source documentation

    Raw-sum form of the inverse-parameter moment.

    theorem intersection_inverse_sum_le {μ : FiniteLaw B} {A : B → Finset X}
    {a : ℝ} (hs : IsSpread μ A a) (ha : 0 ≤ a) {m : ℕ}
    {T : Finset X} (hT : T.card ≤ m) {ρ : ℝ} (hρ : 0 < ρ) :
    (∑ c, μ.weight c * (ρ⁻¹) ^ (A c ∩ T).card) ≤ (1 + a / ρ) ^ m :=
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread

  13. theorem OAI.LeanBlast.SecondKahnKalai.intersection_inverse_truncated_sum_le line 197

    Source documentation

    Inverse-parameter truncated moment, retaining an arbitrary tail predicate.

    theorem intersection_inverse_truncated_sum_le
    {μ : FiniteLaw B} {A : B → Finset X} {a : ℝ}
    (hs : IsSpread μ A a) (ha : 0 ≤ a) {m : ℕ}
    {T : Finset X} (hT : T.card ≤ m) {ρ : ℝ} (hρ : 0 < ρ)
    (Q : ℕ → Prop) [DecidablePred Q] :
    (∑ c, if Q (A c ∩ T).card then μ.weight c * (ρ⁻¹) ^ (A c ∩ T).card else 0) ≤
      ∑ r ∈ Finset.range (m + 1),
        if Q r then (m.choose r : ℝ) * (a / ρ) ^ r else 0 := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.IsSpread