GenericSubspaceProbability.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The polynomial exceptional-event bound is transported first to all binary linear parameter maps and then, by proved uniformity conditional on injectivity, to the actual finite Grassmannian. The same argument supplies a generic subspace, rather than presupposing that one exists.

theorem OAI.UniqueGamesTheorem.Quadratic.conditioning_counts line 26
theorem OAI.UniqueGamesTheorem.Quadratic.generic_subspace_and_probability_of_parameter_error line 73
Source documentation
Both generic-subspace existence and the conditional Grassmannian bound follow from the single unconditional parameter-map exceptional bound.
```
theorem generic_subspace_and_probability_of_parameter_error (α : ℚ)
    (hα₀ : 0 ≤ α) (hα : α < 1)
    (herror : (finiteAssignmentProbability (fun x : (Fin 3 × J) → F =>
      ¬(Function.Injective (parameterMap x) ∧ IsGeneric (parameterMap x).range)) : ℚ) ≤ α) :
    (∃ S : RankSpace (ZMod 2) (Fin 3 → F) (Fintype.card J), IsGeneric S.1) ∧
      nongenericFraction F (Fintype.card J) ≤ α / (1 - α) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.finiteAssignmentProbability, OAI.UniqueGamesTheorem.Quadratic.parameterMap, OAI.UniqueGamesTheorem.Quadratic.IsGeneric, OAI.UniqueGamesTheorem.Quadratic.nongenericFraction

theorem OAI.UniqueGamesTheorem.Quadratic.exists_generic_subspace_error_numerator line 117

Source documentation

The exact v2 genericity statement with a positive numerator fixed before the extension field. The property quantifies over every binary linear lift.

theorem exists_generic_subspace_error_numerator (J : Type*) [Fintype J] :
    ∃ D : ℕ, 0 < D ∧
      ∀ (F : Type*) [Field F] [Fintype F] [CharP F 2] [Algebra (ZMod 2) F],
        (D : ℚ) / Fintype.card F < 1 →
        (∃ S : RankSpace (ZMod 2) (Fin 3 → F) (Fintype.card J), IsGeneric S.1) ∧
          nongenericFraction F (Fintype.card J) ≤
            ((D : ℚ) / Fintype.card F) / (1 - (D : ℚ) / Fintype.card F) := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.D, OAI.UniqueGamesTheorem.Quadratic.IsGeneric, OAI.UniqueGamesTheorem.Quadratic.nongenericFraction

theorem OAI.UniqueGamesTheorem.Quadratic.conditional_error_le_of_small line 133
Source documentation
A convenient numerical threshold for choosing one field for finitely many ranks: α ≤ min(1/2, ε/2) is sufficient.
```
theorem conditional_error_le_of_small (α ε : ℚ) (hα : 0 ≤ α)
    (hhalf : α ≤ 1 / 2) (hε : α ≤ ε / 2) : α / (1 - α) ≤ ε := by
…
```