MixerBalance.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Balanced random signs and conditional mixer halves

The three mixers are disjoint. Uniform global sign subsets therefore induce independent uniform subsets on them. Conditioning each restriction to have half the mixer size gives the exact balance probability and uniform halves.

def OAI.LowSpaceSubsetSum.partitionFinsetEquiv line 23
Source documentation
Split a finite set into its restrictions to the fibers of a finite coloring.
```
def partitionFinsetEquiv (c : ι → K) :
    Finset ι ≃ ((k : K) → Finset {x : ι // c x = k}) where
…
```
theorem OAI.LowSpaceSubsetSum.card_partition_profile line 50
def OAI.LowSpaceSubsetSum.ColorBalanced line 61
Source documentation
Balance of the three non-outside color classes.
```
def ColorBalanced (c : ι → Option (Fin 3)) (s : ℕ) (S : Finset ι) : Prop :=
…
```
theorem OAI.LowSpaceSubsetSum.colorBalanced_card line 64
theorem OAI.LowSpaceSubsetSum.central_binomial_lower line 89
theorem OAI.LowSpaceSubsetSum.colorBalanced_probability line 102
theorem OAI.LowSpaceSubsetSum.colorBalanced_probability_lower line 118
def OAI.LowSpaceSubsetSum.mixerColor line 127
Source documentation
The index of a mixer containing an input position, or the outside category.
```
noncomputable def mixerColor (M : Fin 3 → Finset ι) (x : ι) : Option (Fin 3) :=
…
```
theorem OAI.LowSpaceSubsetSum.mixerColor_eq_some_iff line 130
def OAI.LowSpaceSubsetSum.MixerBalanced line 152
theorem OAI.LowSpaceSubsetSum.mixerColor_restriction_card line 155
theorem OAI.LowSpaceSubsetSum.colorBalanced_mixerColor_iff line 164
theorem OAI.LowSpaceSubsetSum.mixerColor_card line 170

theorem OAI.LowSpaceSubsetSum.mixer_balance_probability line 179

Source documentation

Exact balance probability, independent of the locations of the three mixers.

theorem mixer_balance_probability [Fintype ι] (M : Fin 3 → Finset ι)
    (hdisj : ∀ i j, i ≠ j → Disjoint (M i) (M j)) (s : ℕ)
    (hsize : ∀ i, (M i).card = 2 * s) :
    finiteUniformProbability (MixerBalanced M s) =
      (((2 * s).choose s : ℝ) / (2 : ℝ) ^ (2 * s)) ^ 3 := by
…

Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.MixerBalanced

theorem OAI.LowSpaceSubsetSum.mixer_balance_probability_lower line 193

Source documentation

The inverse-cubic balance bound used before the deficiency estimates.

theorem mixer_balance_probability_lower [Fintype ι] (M : Fin 3 → Finset ι)
    (hdisj : ∀ i j, i ≠ j → Disjoint (M i) (M j)) (s : ℕ)
    (hsize : ∀ i, (M i).card = 2 * s) :
    1 / (2 * s + 1 : ℝ) ^ 3 ≤ finiteUniformProbability (MixerBalanced M s) := by
…

Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.MixerBalanced

theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_equiv line 205

theorem OAI.LowSpaceSubsetSum.permuted_family_uniform line 214

Source documentation

Randomly permuting any independently chosen size-s set gives the same uniform marginal, even when the choice of that set has additional constraints.

theorem permuted_family_uniform [Fintype ι] {Ξ : Type*} [Fintype Ξ] [Nonempty Ξ]
    (B : Ξ → Finset ι) (s : ℕ) (hB : ∀ ξ, (B ξ).card = s) (P : Finset ι → Prop) :
    finiteUniformProbability (fun z : Equiv.Perm ι × Ξ => P (permuteSubset z.1 (B z.2))) =
      finiteUniformProbability (fun S : ↥((Finset.univ : Finset ι).powersetCard s) => P S.val) := by
…

Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.permuteSubset

theorem OAI.LowSpaceSubsetSum.permuteSubset_inter line 262
theorem OAI.LowSpaceSubsetSum.permuteSubset_sdiff line 266
theorem OAI.LowSpaceSubsetSum.mixerBalanced_permute line 270
abbrev OAI.LowSpaceSubsetSum.BalancedSignSubsets line 276
instance OAI.LowSpaceSubsetSum.balancedSignSubsetsFintype line 279
abbrev OAI.LowSpaceSubsetSum.BalancedMixerJoint line 282
instance OAI.LowSpaceSubsetSum.balancedMixerJointFintype line 286
def OAI.LowSpaceSubsetSum.balancedMixerJointEquiv line 291
Source documentation
Conditioning the global sign subset on mixer balance leaves the permutation uniform and independent of the balanced sign subset in the original coordinates.
```
def balancedMixerJointEquiv [Fintype ι] (M : Fin 3 → Finset ι) (s : ℕ) :
    BalancedMixerJoint M s ≃ Equiv.Perm ι × BalancedSignSubsets M s where
…
```
Mentions: OAI.LowSpaceSubsetSum.BalancedMixerJoint, OAI.LowSpaceSubsetSum.BalancedSignSubsets
theorem OAI.LowSpaceSubsetSum.balancedSignSubsets_nonempty line 316
theorem OAI.LowSpaceSubsetSum.conditioned_mixer_permutation_uniform line 327
theorem OAI.LowSpaceSubsetSum.conditioned_selected_half_uniform line 338
theorem OAI.LowSpaceSubsetSum.conditioned_complement_half_uniform line 361
abbrev OAI.LowSpaceSubsetSum.BalancedColorRestriction line 389
Source documentation
A restriction in a mixer must have size s; the outside restriction is free.
```
abbrev BalancedColorRestriction (c : ι → Option (Fin 3)) (s : ℕ)
    (k : Option (Fin 3)) :=
…
```
instance OAI.LowSpaceSubsetSum.balancedColorRestrictionFintype line 395
def OAI.LowSpaceSubsetSum.colorBalancedRestrictionEquiv line 399
def OAI.LowSpaceSubsetSum.balancedMixerRestrictionEquiv line 424
Source documentation
The full conditional sign law is the product of the three uniform halves and the unrestricted outside signs.
```
noncomputable def balancedMixerRestrictionEquiv (M : Fin 3 → Finset ι)
    (hdisj : ∀ i j, i ≠ j → Disjoint (M i) (M j)) (s : ℕ) :
    BalancedSignSubsets M s ≃
      ((k : Option (Fin 3)) → BalancedColorRestriction (mixerColor M) s k) :=
…
```
Mentions: OAI.LowSpaceSubsetSum.BalancedSignSubsets, OAI.LowSpaceSubsetSum.BalancedColorRestriction, OAI.LowSpaceSubsetSum.mixerColor
theorem OAI.LowSpaceSubsetSum.conditioned_mixer_restrictions_uniform line 431
theorem OAI.LowSpaceSubsetSum.conditioned_mixer_restrictions_point line 438