RepresentationConcentration.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The low-mean layout event

These estimates concern one uniform permutation of a fixed layout. All six half blocks and all three mixers have the required marginals without any independence assumption. The spread test retains the integer floor used by the program. The separate balance law connects this layout law to the conditional signed-solution experiment.

theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_union_le line 19
def OAI.LowSpaceSubsetSum.mixerSpreadTest line 29
Source documentation
The exact pairwise integer spread test; it also bounds the largest list by the smallest list times the displayed factor.
```
def mixerSpreadTest {ι : Type*} [Fintype ι] [DecidableEq ι] (a : ι → ℤ)
    (M : Fin 3 → Finset ι) (n : ℕ) : Prop :=
…
```
theorem OAI.LowSpaceSubsetSum.spread_floor_margin line 33
theorem OAI.LowSpaceSubsetSum.mixerSpreadTest_of_centered line 42

theorem OAI.LowSpaceSubsetSum.representation_layout_good_probability line 63

Source documentation

Simultaneous concentration for the six halves and three pre-order mixers. This is a marginal union bound, with explicit absolute threshold.

theorem representation_layout_good_probability {n s m : ℕ} (hn : 0 < n)
    (hs : (s : ℝ) ≤ (3 / 25 : ℝ) * n)
    (hm : (m : ℝ) ≤ (6 / 25 : ℝ) * n)
    (a : Fin n → ℤ) (H : Fin 6 → Finset (Fin n))
    (M : Fin 3 → Finset (Fin n))
    (hH : ∀ i, (H i).card = s) (hM : ∀ i, (M i).card = m)
    (hmean : meanDeficiency a Finset.univ s < (153 / 20000 : ℝ) * n) :
    1 - (90000000 : ℝ) / n ≤ finiteUniformProbability (fun e : Equiv.Perm (Fin n) =>
      (∀ i, deficiency a (permuteSubset e (H i)) ≤ (39 / 5000 : ℝ) * n) ∧
      (∀ i, |deficiency a (permuteSubset e (M i)) -
        meanDeficiency a Finset.univ m| ≤ (n : ℝ) / 5000)) := by
…

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

theorem OAI.LowSpaceSubsetSum.representation_layout_tests_probability line 146