FrameSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite union bound chooses one sign matrix that passes every real net test for every injective subfamily of the prescribed size.

theorem OAI.Dixmier.SignMatrix.embedding_card_le line 13
theorem OAI.Dixmier.SignMatrix.exists_sign_matrix line 20
Source documentation
A real sign-matrix realization for all size-p subfamilies. The proof uses the actual finite sign sample space, cardinality bounds, and net tests.
```
theorem exists_sign_matrix {n k p : ℕ} (hk : 0 < k)
    (hf : 2 * (n : ℝ)^p * 9^(k+p) * Real.exp (-25*(k : ℝ)/2) < 1) :
    ∃ σ : Fin k × Fin n → Bool, ∀ e : Fin p ↪ Fin n, ‖synthesis σ e‖ ≤ 10 := by
…
```
Mentions: OAI.Dixmier.SignMatrix.synthesis