HalfOrientations.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Orienting three pairs of mixer halves

The orientations here describe the conditional sign experiment; they are analysis variables, not extra random draws made by the algorithm. Every unordered pair of halves has a good orientation by deficiency superadditivity. A uniform vector of three orientations therefore succeeds with probability at least one eighth. The product-space bound also permits an arbitrary preceding event depending on the unordered pairs.

theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_ge_card_inv_of_exists line 18
def OAI.LowSpaceSubsetSum.orientedHalf line 31
theorem OAI.LowSpaceSubsetSum.exists_good_half_orientation line 34
theorem OAI.LowSpaceSubsetSum.three_half_orientations_probability line 46
theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_joint_orientation line 66
Source documentation
Counting one successful orientation over every preceding good outcome gives the joint lower bound without assuming that the preceding event and the successful orientation event are independent.
```
theorem finiteUniformProbability_joint_orientation {Ω : Type*} [Fintype Ω]
    [Nonempty Ω] (E : Ω → Prop) (G : Ω → (Fin 3 → Bool) → Prop)
    (hG : ∀ ω, E ω → ∃ b, G ω b) :
    finiteUniformProbability E / 8 ≤
      finiteUniformProbability (fun p : Ω × (Fin 3 → Bool) => E p.1 ∧ G p.1 p.2) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability