RepresentationFamilies.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Representative families in actual mixer subblock partitions

The three categories are the chosen representative, its complement in the selected half, and the outside half. Their canonical disjoint-union counting model is transported to partitions of the actual mixer indices.

def OAI.LowSpaceSubsetSum.balancedBlockCounts line 24
Source documentation
The implementation assigns the remainder in the fixed block order.
```
def balancedBlockCounts (l k : ℕ) (j : Fin l) : ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.balancedBlockCounts_sum line 27
theorem OAI.LowSpaceSubsetSum.balancedBlockCounts_balanced line 44
theorem OAI.LowSpaceSubsetSum.balancedBlockCounts_le line 49
def OAI.LowSpaceSubsetSum.representativeBlockProfile line 54
Source documentation
Smaller masks, complementary masks, and outside indices fill each block.
```
def representativeBlockProfile (l t k : ℕ) : Fin 3 → Fin l → ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.representativeBlockProfile_properties line 57
def OAI.LowSpaceSubsetSum.representativeCategories line 92
theorem OAI.LowSpaceSubsetSum.representativeCategories_subset line 96
theorem OAI.LowSpaceSubsetSum.representativeCategories_disjoint line 105
theorem OAI.LowSpaceSubsetSum.representativeCategories_card line 115
def OAI.LowSpaceSubsetSum.representativeCategoryEquiv line 122
Source documentation
The canonical three-category domain is exactly the actual mixer.
```
noncomputable def representativeCategoryEquiv {D A M : Finset ι}
    (hDA : D ⊆ A) (hAM : A ⊆ M) :
    CategoryDomain (fun i => ↥(representativeCategories D A M i)) ≃ ↥M := by
…
```
Mentions: OAI.LowSpaceSubsetSum.CategoryDomain, OAI.LowSpaceSubsetSum.representativeCategories
def OAI.LowSpaceSubsetSum.coloringsPrecomposeEquiv line 145

theorem OAI.LowSpaceSubsetSum.actual_representative_partition_probability line 157

Source documentation

The actual labeled mixer partitions have the same category probability as the canonical multinomial model.

theorem actual_representative_partition_probability {D A M : Finset ι}
    (hDA : D ⊆ A) (hAM : A ⊆ M) (l b : ℕ) (hl : l = 2 ∨ l = 4)
    (q : Fin 3 → Fin l → ℕ)
    (hrows : ∀ i, ∑ j, q i j = (representativeCategories D A M i).card)
    (hcols : ∀ j, ∑ i, q i j = b) (hbal : ∀ i, BalancedProfile (q i)) :
    1 / (M.card + 1 : ℝ) ^ (3 * l) ≤
      finiteUniformProbability
        (fun f : MatchingSmoothing.Colorings ↥M (Fin l) (fun _ => b) =>
          ∀ i, MatchingSmoothing.histogram
            (fun x : ↥(representativeCategories D A M i) =>
              f.val ⟨x.val, representativeCategories_subset hDA hAM i x.property⟩) = q i) := by
…

Mentions: OAI.LowSpaceSubsetSum.representativeCategories, OAI.LowSpaceSubsetSum.BalancedProfile, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.MatchingSmoothing.Colorings, OAI.MatchingSmoothing.histogram, OAI.LowSpaceSubsetSum.representativeCategories_subset

def OAI.LowSpaceSubsetSum.representativeMask line 181
Source documentation
One concrete mask for every distinct integer weight at the selected size.
```
noncomputable def representativeMask (a : ι → ℤ) (A : Finset ι) (k : ℕ)
    (x : ↥(sumsAtSize a A k)) : Finset ι :=
…
```
Mentions: OAI.LowSpaceSubsetSum.sumsAtSize
theorem OAI.LowSpaceSubsetSum.representativeMask_spec line 185
theorem OAI.LowSpaceSubsetSum.representativeMask_weights_injective line 191
def OAI.LowSpaceSubsetSum.survivingWeights line 199
Source documentation
The image contains distinct weights rather than repeated subset occurrences.
```
noncomputable def survivingWeights {R : Type*} [Fintype R]
    (a : ι → ℤ) (mask : R → Finset ι) (P : R → Prop) : Finset ℤ := by
…
```
theorem OAI.LowSpaceSubsetSum.survivingWeights_probability line 204
theorem OAI.LowSpaceSubsetSum.retained_family_denominator line 220

theorem OAI.LowSpaceSubsetSum.retained_family_count line 236

Source documentation

The paper's exponent fourteen absorbs the size pigeonhole factor and half of the expected retained fraction, for both arities.

theorem retained_family_count {R : Type*} [Fintype R] [Nonempty R]
    (a : ι → ℤ) (mask : R → Finset ι)
    (hinj : Function.Injective (fun r => weight a (mask r)))
    (P : R → Prop) (s l : ℕ) (L u : ℝ) (hu : 2 ≤ u)
    (hs : (s : ℝ) + 1 ≤ u) (hl : l = 2 ∨ l = 4)
    (hsize : (2 : ℝ) ^ L / ((s : ℝ) + 1) ≤ Fintype.card R)
    (hretained : (1 / u ^ (3 * l)) / 2 ≤ finiteUniformProbability P) :
    (2 : ℝ) ^ L / u ^ 14 ≤ (survivingWeights a mask P).card := by
…

Mentions: OAI.LowSpaceSubsetSum.weight, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.survivingWeights

theorem OAI.LowSpaceSubsetSum.retained_distinct_weight_probability line 263
def OAI.LowSpaceSubsetSum.representativePrescriptions line 286

theorem OAI.LowSpaceSubsetSum.actual_representative_family_survival line 295

Source documentation

The finite family consists of actual masks inside the selected half, and the sample space consists of actual equal-size mixer partitions.

theorem actual_representative_family_survival {R : Type*} [Fintype R] [Nonempty R]
    (a : ι → ℤ) (A M : Finset ι) (mask : R → Finset ι)
    (hinj : Function.Injective (fun r => weight a (mask r)))
    (hDA : ∀ r, mask r ⊆ A) (hAM : A ⊆ M) (l b : ℕ)
    (hl : l = 2 ∨ l = 4) (hparts : l * b = M.card)
    (q : Fin 3 → Fin l → ℕ)
    (hrows : ∀ r i, ∑ j, q i j = (representativeCategories (mask r) A M i).card)
    (hcols : ∀ j, ∑ i, q i j = b) (hbal : ∀ i, BalancedProfile (q i))
    (s : ℕ) (L u : ℝ) (hu : 2 ≤ u) (hs : (s : ℝ) + 1 ≤ u)
    (hm : (M.card : ℝ) + 1 ≤ u)
    (hsize : (2 : ℝ) ^ L / ((s : ℝ) + 1) ≤ Fintype.card R) :
    1 / (2 * u ^ (3 * l)) ≤ finiteUniformProbability
…

Mentions: OAI.LowSpaceSubsetSum.weight, OAI.LowSpaceSubsetSum.representativeCategories, OAI.LowSpaceSubsetSum.BalancedProfile, OAI.LowSpaceSubsetSum.finiteUniformProbability

theorem OAI.LowSpaceSubsetSum.fixed_profile_family_survival line 321

Source documentation

The algorithm's fixed-order remainder counts satisfy every category condition, including the complementary masks and the outside half.

theorem fixed_profile_family_survival {R : Type*} [Fintype R] [Nonempty R]
    (a : ι → ℤ) (A M : Finset ι) (mask : R → Finset ι)
    (hinj : Function.Injective (fun r => weight a (mask r)))
    (hDA : ∀ r, mask r ⊆ A) (hAM : A ⊆ M) (l t k : ℕ)
    (hl : l = 2 ∨ l = 4) (hk : k ≤ l * t)
    (hD : ∀ r, (mask r).card = k) (hA : A.card = l * t)
    (hM : M.card = 2 * (l * t)) (L u : ℝ) (hu : 2 ≤ u)
    (hs : ((l * t : ℕ) : ℝ) + 1 ≤ u) (hm : (M.card : ℝ) + 1 ≤ u)
    (hsize : (2 : ℝ) ^ L / ((l * t : ℕ) + 1) ≤ Fintype.card R) :
    1 / (2 * u ^ (3 * l)) ≤ finiteUniformProbability
      (fun f : MatchingSmoothing.Colorings ↥M (Fin l) (fun _ => 2 * t) =>
        (2 : ℝ) ^ L / u ^ 14 ≤ (survivingWeights a mask
…

Mentions: OAI.LowSpaceSubsetSum.weight, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.MatchingSmoothing.Colorings, OAI.LowSpaceSubsetSum.survivingWeights

theorem OAI.LowSpaceSubsetSum.distinct_sum_representatives_survival line 345

Source documentation

Applying the survival estimate to the concrete representative chosen for each distinct sum gives the actual retained-weight event.

theorem distinct_sum_representatives_survival
    (a : ι → ℤ) (A M : Finset ι) (hAM : A ⊆ M) (l t k : ℕ)
    (hl : l = 2 ∨ l = 4) (hk : k ≤ l * t)
    (hA : A.card = l * t) (hM : M.card = 2 * (l * t))
    (L u : ℝ) (hu : 2 ≤ u) (hs : ((l * t : ℕ) : ℝ) + 1 ≤ u)
    (hm : (M.card : ℝ) + 1 ≤ u)
    (hsize : (2 : ℝ) ^ L / ((l * t : ℕ) + 1) ≤ (sumsAtSize a A k).card) :
    1 / (2 * u ^ (3 * l)) ≤ finiteUniformProbability
      (fun f : MatchingSmoothing.Colorings ↥M (Fin l) (fun _ => 2 * t) =>
        (2 : ℝ) ^ L / u ^ 14 ≤ (survivingWeights a (representativeMask a A k)
          (fun r => representativePrescriptions (representativeMask_spec a A k r).1 hAM
            (representativeBlockProfile l t k) f)).card) := by
…

Mentions: OAI.LowSpaceSubsetSum.sumsAtSize, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.MatchingSmoothing.Colorings, OAI.LowSpaceSubsetSum.survivingWeights, OAI.LowSpaceSubsetSum.representativeMask, OAI.LowSpaceSubsetSum.representativePrescriptions, OAI.LowSpaceSubsetSum.representativeMask_spec, OAI.LowSpaceSubsetSum.representativeBlockProfile

theorem OAI.LowSpaceSubsetSum.exists_large_representative_family line 371

Source documentation

Pigeonhole-selected sizes give concrete, weight-injective representative families on each actual selected half.

theorem exists_large_representative_family (a : ι → ℤ) (A : Finset ι)
    (L : ℝ) (hL : L ≤ (A.card : ℝ) - deficiency a A) :
    ∃ k ≤ A.card / 2,
      (2 : ℝ) ^ L / (A.card + 1) ≤ (sumsAtSize a A k).card ∧
      (∀ x : ↥(sumsAtSize a A k), representativeMask a A k x ⊆ A ∧
        (representativeMask a A k x).card = k ∧
        weight a (representativeMask a A k x) = x.val) ∧
      Function.Injective (fun x : ↥(sumsAtSize a A k) => weight a (representativeMask a A k x)) := by
…

Mentions: OAI.LowSpaceSubsetSum.deficiency, OAI.LowSpaceSubsetSum.sumsAtSize, OAI.LowSpaceSubsetSum.representativeMask, OAI.LowSpaceSubsetSum.weight

theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_pi line 385

theorem OAI.LowSpaceSubsetSum.three_representative_families_probability line 396

Source documentation

One top partition and two local partitions are independent in the actual product sample space; their inverse-polynomial costs multiply.

theorem three_representative_families_probability
    (Ω : Fin 3 → Type v) [∀ i, Fintype (Ω i)] (P : ∀ i, Ω i → Prop)
    (u : ℝ) (hu : 8 ≤ u)
    (h0 : 1 / (2 * u ^ 12) ≤ finiteUniformProbability (P 0))
    (h1 : 1 / (2 * u ^ 6) ≤ finiteUniformProbability (P 1))
    (h2 : 1 / (2 * u ^ 6) ≤ finiteUniformProbability (P 2)) :
    1 / u ^ 25 ≤ finiteUniformProbability (fun x : ∀ i, Ω i => ∀ i, P i (x i)) := by
…

Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability