OAI/Combinatorics/LowSpaceSubsetSum/Counting/BalancedPartitions.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LowSpaceSubsetSum.BalancedProfile line 21

   Source documentation

   Counts differ by at most one across all labeled blocks.

   def BalancedProfile (t : K → ℕ) : Prop := ∀ i j, t i ≤ t j + 1

2. theorem OAI.LowSpaceSubsetSum.poisson_mass_at_adjacent_mode line 23
3. theorem OAI.LowSpaceSubsetSum.balanced_multinomial_max line 35
4. theorem OAI.LowSpaceSubsetSum.balanced_multinomial_lower line 63

   Source documentation

   A balanced profile receives at least the average multinomial mass. There are at most (n+1)^|K| profiles.

   theorem balanced_multinomial_lower [Nonempty K] (t : K → ℕ) (n : ℕ)
       (ht : BalancedProfile t) (hsum : ∑ i, t i = n) :
       (Fintype.card K : ℝ) ^ n ≤ (n + 1 : ℝ) ^ Fintype.card K *
         Nat.multinomial Finset.univ t := by
   …

   Mentions: OAI.LowSpaceSubsetSum.BalancedProfile

5. def OAI.LowSpaceSubsetSum.sigma_fst_fiber_equiv line 87
6. theorem OAI.LowSpaceSubsetSum.exists_coloring_of_sum line 94
7. theorem OAI.LowSpaceSubsetSum.card_colorings_of_sum line 108
8. abbrev OAI.LowSpaceSubsetSum.CategoryDomain line 116

   Source documentation

   The domain is the disjoint union of the three categories in the paper.

   abbrev CategoryDomain (C : Fin 3 → Type*) := Σ a, C a

9. abbrev OAI.LowSpaceSubsetSum.PrescribedLabelings line 118
10. instance OAI.LowSpaceSubsetSum.prescribedLabelingsFintype line 122
11. theorem OAI.LowSpaceSubsetSum.card_prescribedLabelings line 126
12. theorem OAI.LowSpaceSubsetSum.histogram_categoryDomain line 140
13. theorem OAI.LowSpaceSubsetSum.prescribedLabelings_fill_blocks line 154
14. theorem OAI.LowSpaceSubsetSum.prescribed_partition_probability_eq line 163

    Source documentation

    Exact favorable/total counting formula, before applying the balanced bounds.

    theorem prescribed_partition_probability_eq
        (C : Fin 3 → Type*) [∀ a, Fintype (C a)] (q : Fin 3 → K → ℕ) (b : ℕ)
        (hrows : ∀ a, ∑ i, q a i = Fintype.card (C a))
        (hcols : ∀ i, ∑ a, q a i = b) :
        finiteUniformProbability
            (fun f : MatchingSmoothing.Colorings (CategoryDomain C) K (fun _ => b) =>
              ∀ a, MatchingSmoothing.histogram (fun x : C a => f.val ⟨a, x⟩) = q a) =
          (∏ a, (Nat.multinomial Finset.univ (q a) : ℝ)) /
            Nat.multinomial (Finset.univ : Finset K) (fun _ => b) := by
    …

    Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.MatchingSmoothing.Colorings, OAI.LowSpaceSubsetSum.CategoryDomain, OAI.MatchingSmoothing.histogram

15. theorem OAI.LowSpaceSubsetSum.balanced_category_count_lower line 195
16. theorem OAI.LowSpaceSubsetSum.balanced_partition_probability line 226

    Source documentation

    Uniform labeled equal-size partitions preserve all three balanced category prescriptions with the paper's inverse-polynomial probability.

    theorem balanced_partition_probability [Nonempty K]
        (C : Fin 3 → Type*) [∀ a, Fintype (C a)] (q : Fin 3 → K → ℕ) (b : ℕ)
        (hrows : ∀ a, ∑ i, q a i = Fintype.card (C a))
        (hcols : ∀ i, ∑ a, q a i = b) (hbal : ∀ a, BalancedProfile (q a)) :
        1 / (Fintype.card (CategoryDomain C) + 1 : ℝ) ^ (3 * Fintype.card K) ≤
          finiteUniformProbability
            (fun f : MatchingSmoothing.Colorings (CategoryDomain C) K (fun _ => b) =>
              ∀ a, MatchingSmoothing.histogram (fun x : C a => f.val ⟨a, x⟩) = q a) := by
    …

    Mentions: OAI.LowSpaceSubsetSum.BalancedProfile, OAI.LowSpaceSubsetSum.CategoryDomain, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.MatchingSmoothing.Colorings, OAI.MatchingSmoothing.histogram

17. theorem OAI.LowSpaceSubsetSum.balanced_partition_probability_two_or_four line 269

    Source documentation

    The only two arities used by the algorithm: top blocks (l=4) and local blocks (l=2).

    theorem balanced_partition_probability_two_or_four (l b : ℕ) (hl : l = 2 ∨ l = 4)
        (C : Fin 3 → Type*) [∀ a, Fintype (C a)] (q : Fin 3 → Fin l → ℕ)
        (hrows : ∀ a, ∑ i, q a i = Fintype.card (C a))
        (hcols : ∀ i, ∑ a, q a i = b) (hbal : ∀ a, BalancedProfile (q a)) :
        1 / (Fintype.card (CategoryDomain C) + 1 : ℝ) ^ (3 * l) ≤
          finiteUniformProbability
            (fun f : MatchingSmoothing.Colorings (CategoryDomain C) (Fin l) (fun _ => b) =>
              ∀ a, MatchingSmoothing.histogram (fun x : C a => f.val ⟨a, x⟩) = q a) := by
    …

    Mentions: OAI.LowSpaceSubsetSum.BalancedProfile, OAI.LowSpaceSubsetSum.CategoryDomain, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.MatchingSmoothing.Colorings, OAI.MatchingSmoothing.histogram

18. theorem OAI.LowSpaceSubsetSum.surviving_fraction_probability line 281

    Source documentation

    A bounded surviving fraction has a polynomially likely substantial value.

    theorem surviving_fraction_probability {Ω : Type*} [Fintype Ω] [Nonempty Ω]
        (Z : Ω → ℝ) {p : ℝ} (_hZ0 : ∀ ω, 0 ≤ Z ω) (hZ1 : ∀ ω, Z ω ≤ 1)
        (hp : p ≤ (∑ ω, Z ω) / Fintype.card Ω) :
        p / 2 ≤ finiteUniformProbability (fun ω => p / 2 ≤ Z ω) := by
    …

    Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability

19. theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_eq_indicator_mean line 305
20. theorem OAI.LowSpaceSubsetSum.surviving_representative_family line 316

    Source documentation

    Pointwise survival gives a likely partition retaining at least half the expected fraction of an arbitrary finite representative family.

    theorem surviving_representative_family {Ω R : Type*}
        [Fintype Ω] [Nonempty Ω] [Fintype R] [Nonempty R]
        (keeps : Ω → R → Prop) {p : ℝ}
        (hp : ∀ r, p ≤ finiteUniformProbability (fun ω => keeps ω r)) :
        p / 2 ≤ finiteUniformProbability
          (fun ω => p / 2 ≤ finiteUniformProbability (keeps ω)) := by
    …

    Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability