OAI/Combinatorics/LowSpaceSubsetSum/Counting/SurvivalLayout.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_prod_average line 18
2. theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_prod_lower line 27
3. def OAI.LowSpaceSubsetSum.baseLayoutTests line 37
4. theorem OAI.LowSpaceSubsetSum.balanced_base_layout_tests_probability line 43
5. def OAI.LowSpaceSubsetSum.actualLayoutTests line 87
6. theorem OAI.LowSpaceSubsetSum.actualLayoutTests_base_iff line 93
7. theorem OAI.LowSpaceSubsetSum.balanced_actual_layout_tests_probability line 104
8. def OAI.LowSpaceSubsetSum.halfComplementEquiv line 128

   Source documentation

   Complementation permutes the subsets having exactly half the ambient size.

   def halfComplementEquiv (α : Type*) [Fintype α] [DecidableEq α]
       (s : ℕ) (hα : Fintype.card α = 2 * s) :
       {S : Finset α // S.card = s} ≃ {S : Finset α // S.card = s} where
   …

9. def OAI.LowSpaceSubsetSum.orientationCoordinateEquiv line 140
10. def OAI.LowSpaceSubsetSum.orientBalancedSigns line 150
11. theorem OAI.LowSpaceSubsetSum.mixer_restriction_map line 158
12. theorem OAI.LowSpaceSubsetSum.mixer_fiber_univ_map line 166
13. theorem OAI.LowSpaceSubsetSum.orientBalancedSigns_selected line 179
14. theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_random_equiv line 213
15. def OAI.LowSpaceSubsetSum.baseLayoutSuccess line 223
16. theorem OAI.LowSpaceSubsetSum.balanced_base_layout_success_probability line 229
17. theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_product_restrict line 289

    Source documentation

    Restricting one coordinate gives the exact balance factor in the joint law.

    theorem finiteUniformProbability_product_restrict {Ω Ψ : Type*}
        [Fintype Ω] [Nonempty Ω] [Fintype Ψ] [Nonempty Ψ]
        (E : Ψ → Prop) [Fintype {y : Ψ // E y}] [Nonempty {y : Ψ // E y}]
        (Q : Ω → Ψ → Prop) :
        finiteUniformProbability (fun z : Ω × Ψ => E z.2 ∧ Q z.1 z.2) =
          finiteUniformProbability E *
            finiteUniformProbability (fun z : Ω × {y : Ψ // E y} => Q z.1 z.2.val) := by
    …

    Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability

18. def OAI.LowSpaceSubsetSum.signLayoutEquiv line 312

    Source documentation

    Independent uniform signs can be expressed in original or permuted coordinates.

    def signLayoutEquiv (ι : Type*) [Fintype ι] [DecidableEq ι] :
        Equiv.Perm ι × Finset ι ≃ Equiv.Perm ι × Finset ι where
    …

19. def OAI.LowSpaceSubsetSum.actualLayoutSuccess line 329
20. theorem OAI.LowSpaceSubsetSum.actualLayoutSuccess_signLayoutEquiv line 335
21. theorem OAI.LowSpaceSubsetSum.signed_layout_survival_probability line 343

    Source documentation

    The complete mixer event in the actual uniform permutation and sign experiment.

    theorem signed_layout_survival_probability {n s : ℕ} (hn : 180000000 ≤ n)
        (hs : (s : ℝ) ≤ (3 / 25 : ℝ) * n)
        (hm : ((2 * s : ℕ) : ℝ) ≤ (6 / 25 : ℝ) * n)
        (a : Fin n → ℤ) (M : Fin 3 → Finset (Fin n))
        (hdisj : ∀ i j, i ≠ j → Disjoint (M i) (M j))
        (hM : ∀ i, (M i).card = 2 * s)
        (hmean : meanDeficiency a Finset.univ s < (153 / 20000 : ℝ) * n) :
        1 / (16 * ((2 * s + 1 : ℕ) : ℝ) ^ 3) ≤ finiteUniformProbability
          (fun z : Equiv.Perm (Fin n) × Finset (Fin n) =>
            MixerBalanced (fun i => permuteSubset z.1 (M i)) s z.2 ∧
              actualLayoutSuccess a M z) := by
    …

    Mentions: OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.MixerBalanced, OAI.LowSpaceSubsetSum.permuteSubset, OAI.LowSpaceSubsetSum.actualLayoutSuccess