Grassmann.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.SidorenkoCounterexample.DimSubspace line 12
abbrev OAI.SidorenkoCounterexample.IndependentTuple line 15
theorem OAI.SidorenkoCounterexample.tuple_spans line 19
def OAI.SidorenkoCounterexample.tupleForget line 29
theorem OAI.SidorenkoCounterexample.tupleForget_bijective line 36

theorem OAI.SidorenkoCounterexample.subspace_count_identity line 60

Source documentation

Counting independent tuples by their span gives the exact Grassmann counting identity, with no division and including k=0.

 theorem subspace_count_identity (k : ℕ) (hk : k ≤ finrank K V) :
    Nat.card (DimSubspace K V k) *
      (∏ i : Fin k, (Fintype.card K ^ k - Fintype.card K ^ i.val)) =
        ∏ i : Fin k, (Fintype.card K ^ finrank K V - Fintype.card K ^ i.val) := by
…

Mentions: OAI.SidorenkoCounterexample.DimSubspace

theorem OAI.SidorenkoCounterexample.independent_tuple_count_pos line 75

theorem OAI.SidorenkoCounterexample.subspace_count_real line 83

Source documentation

The exact Gaussian binomial formula stated in the manuscript.

 theorem subspace_count_real (k : ℕ) (hk : k ≤ finrank K V) :
    (Nat.card (DimSubspace K V k) : ℝ) =
      ∏ i : Fin k, ((Fintype.card K : ℝ) ^ finrank K V - (Fintype.card K : ℝ)^i.val) /
        ((Fintype.card K : ℝ)^k - (Fintype.card K : ℝ)^i.val) := by
…

Mentions: OAI.SidorenkoCounterexample.DimSubspace

theorem OAI.SidorenkoCounterexample.subspace_count_upper line 109
Source documentation
A dimension-uniform explicit Grassmann bound, sufficient for all nullity union bounds; the constant 2^k is independent of the finite field.
```
 theorem subspace_count_upper (k : ℕ) (hk : k ≤ finrank K V) :
    (Nat.card (DimSubspace K V k) : ℝ) ≤
      2^k * (Fintype.card K : ℝ)^(k * (finrank K V - k)) := by
…
```
Mentions: OAI.SidorenkoCounterexample.DimSubspace
def OAI.SidorenkoCounterexample.symmetricSubmodule line 156
abbrev OAI.SidorenkoCounterexample.SymMatrix line 162
def OAI.SidorenkoCounterexample.symMatrixCoordinates line 165
Source documentation
A symmetric matrix is exactly a function on unordered pairs with repetition.
```
def symMatrixCoordinates (D : ℕ) : SymMatrix K D ≃ (Sym2 (Fin D) → K) :=
…
```
Mentions: OAI.SidorenkoCounterexample.SymMatrix
theorem OAI.SidorenkoCounterexample.symMatrix_card line 175
abbrev OAI.SidorenkoCounterexample.SymForm line 182
def OAI.SidorenkoCounterexample.symFormMatrix line 184
instance OAI.SidorenkoCounterexample.symForm_finite line 189
theorem OAI.SidorenkoCounterexample.symForm_card line 192
def OAI.SidorenkoCounterexample.formRadicalEquiv line 200
Source documentation
Symmetric forms whose radical contains a prescribed subspace descend bijectively to the quotient. This keeps the actual radical condition.
```
def formRadicalEquiv (U : Submodule K V) :
    {B : SymForm K V // U ≤ B.val.ker} ≃ SymForm K (V ⧸ U) where
…
```
Mentions: OAI.SidorenkoCounterexample.SymForm
theorem OAI.SidorenkoCounterexample.radical_containment_card line 230
theorem OAI.SidorenkoCounterexample.nullity_count_bound line 240
Source documentation
Union bound over genuine subspaces of the radical, not a rank heuristic.
```
 theorem nullity_count_bound [Fintype K] [Finite V] (u : ℕ) :
    Nat.card {B : SymForm K V // u ≤ finrank K B.val.ker} ≤
      Nat.card (DimSubspace K V u) *
        Fintype.card K ^ ((finrank K V - u + 1).choose 2) := by
…
```
Mentions: OAI.SidorenkoCounterexample.SymForm, OAI.SidorenkoCounterexample.DimSubspace
theorem OAI.SidorenkoCounterexample.symmetric_nullity_exponent line 272
theorem OAI.SidorenkoCounterexample.symmetric_nullity_probability_bound line 283
Source documentation
An explicit finite-field nullity tail bound. In the manuscript this is O(q^(-b(u))); here the constant is the concrete field-independent 2^u.
```
 theorem symmetric_nullity_probability_bound [Fintype K] [Finite V]
    (u : ℕ) (hu : u ≤ finrank K V) :
    (Nat.card {B : SymForm K V // u ≤ finrank K B.val.ker} : ℝ) /
      Nat.card (SymForm K V) ≤ 2^u / (Fintype.card K : ℝ)^((u+1).choose 2) := by
…
```
Mentions: OAI.SidorenkoCounterexample.SymForm