SubspaceCountingLemmas.lean`

77 declarations, 0 contain sorry, 0 declared as axioms

Finite-field subspace cardinality bounds used in Appendix A.4. The objects counted here are actual mathlib submodules, not encoded cardinality assumptions.

def OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.generators line 30
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.span_generators line 34
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.card_subspaces_rank_le line 42
Source documentation
A k-subspace is determined by a chosen ordered k-tuple of spanning vectors.
```
theorem card_subspaces_rank_le [Finite V] (k : ℕ) :
    Nat.card {S : Submodule K V // finrank K S = k} ≤ Nat.card V ^ k := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.card_subspaces_rank_le_field_power line 58
Source documentation
General finite-field form of the image-choice estimate in A.4.
```
theorem card_subspaces_rank_le_field_power [Finite K] (k : ℕ) :
    Nat.card {S : Submodule K V // finrank K S = k} ≤
      Nat.card K ^ (finrank K V * k) := by
…
```

theorem OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.card_binary_subspaces_rank_le line 68

Source documentation

Binary specialization: the ambient dimension is the dimension of Y's image, not the potentially much larger original vector space.

theorem card_binary_subspaces_rank_le
    {V : Type*} [AddCommGroup V] [Module (ZMod 2) V] [Module.Finite (ZMod 2) V]
    (d k : ℕ) (hd : finrank (ZMod 2) V ≤ d) :
    Nat.card {S : Submodule (ZMod 2) V // finrank (ZMod 2) S = k} ≤
      2 ^ (d * k) := by
…

theorem OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.card_linearMaps_le line 84
Source documentation
Evaluating on a basis bounds the number of linear maps without counting arbitrary functions on every vector.
```
theorem card_linearMaps_le [Finite V] :
    Nat.card (U →ₗ[K] V) ≤ Nat.card V ^ finrank K U := by
…
```

theorem OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.exists_rank_factorization line 96

Source documentation

Every rank-k map factors through the actual coordinate vector space K^k.

theorem exists_rank_factorization (f : U →ₗ[K] V) (k : ℕ)
    (hk : finrank K (LinearMap.range f) = k) :
    ∃ (a : (Fin k → K) →ₗ[K] V) (b : U →ₗ[K] (Fin k → K)), a.comp b = f := by
…

theorem OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.card_rank_maps_le line 108
Source documentation
Rank-k maps between r- and s-dimensional spaces number at most |K|^((r+s)k). This is a general finite-field bound, proved by selecting the preceding factorization and injecting into the pair of factor maps.
```
theorem card_rank_maps_le [Finite K] (k : ℕ) :
    Nat.card {f : U →ₗ[K] V // finrank K (LinearMap.range f) = k} ≤
      Nat.card K ^ ((finrank K U + finrank K V) * k) := by
…
```

def OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.quotientImageMap line 148

Source documentation

Factor a map whose kernel contains ker Y and whose image lies in range Y through the effective domain and codomain.

def quotientImageMap (Y X : U →ₗ[K] V)
    (hker : LinearMap.ker Y ≤ LinearMap.ker X)
    (himage : LinearMap.range X ≤ LinearMap.range Y) :
    (U ⧸ LinearMap.ker Y) →ₗ[K] LinearMap.range Y :=
…

theorem OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.quotientImageMap_mk line 158
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.rank_quotientImageMap line 164
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.card_constrained_maps_le line 177
Source documentation
General ambient-independent rank-k bound for maps constrained by the image and kernel of Y. This counts actual linear maps; neither cardinality nor rank-additive predecessor estimates are supplied as hypotheses.
```
theorem card_constrained_maps_le [Finite K] (Y : U →ₗ[K] V) (k : ℕ) :
    Nat.card {X : U →ₗ[K] V // finrank K (LinearMap.range X) = k ∧
      LinearMap.ker Y ≤ LinearMap.ker X ∧ LinearMap.range X ≤ LinearMap.range Y} ≤
      Nat.card K ^ (2 * finrank K (LinearMap.range Y) * k) := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.binary_add_cancel line 223
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceCounting.card_binary_predecessors_le line 231
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.horizontal line 293
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.hKernel line 294
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.scalarMap line 296
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.extension line 301
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.extension_mem line 305
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.mkQ_eq_smul_iff line 310
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.hKernel_horizontal line 317
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.hKernel_extension line 322
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.exists_one_extension line 329
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.eq_extension_of_one_mem line 333
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.eq_horizontal_of_no_one line 347
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.horizontal_ne_extension line 366
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.extension_injective line 373
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.encode line 381
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.encode_injective line 385
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.encode_surjective line 409
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.splitEquiv line 416
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.horizontalEquiv line 419
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.extensionEquiv line 432
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.finrank_horizontal line 472
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.finrank_extension line 475
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.weightedTotal line 489
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.card_eq_pow_finrank line 491
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.quotient_card_mul_pow line 499
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.weightedTotal_prod line 506
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.mobiusWeight line 532
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.mobiusTotal line 536
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.mobiusTotal_prod line 539
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.map_inverse line 562
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.subspaceEquiv line 567
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.subspaceMapEquiv line 573
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.finrank_map_equiv line 584
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.weightedTotal_equiv line 587
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.mobiusTotal_equiv line 600
def OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.coordinateSplit line 604
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.mobiusTotal_subsingleton line 618
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.coordinate_total_succ line 635
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.mobiusTotal_eq_if line 644
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.mobiusWeight_closed line 651
theorem OAI.UniqueGamesTheorem.Appendix.SubspaceExtensions.binary_subspace_mobius line 660
def OAI.UniqueGamesTheorem.Appendix.SubmoduleInterval.lowerIntervalEquiv line 681
def OAI.UniqueGamesTheorem.Appendix.SubmoduleInterval.lowerIntervalSpaceEquiv line 710
theorem OAI.UniqueGamesTheorem.Appendix.SubmoduleInterval.lowerInterval_finrank line 720
theorem OAI.UniqueGamesTheorem.Appendix.SubmoduleInterval.sum_lowerInterval line 728
def OAI.UniqueGamesTheorem.Appendix.SubmoduleInterval.lowerWeightedTotal line 740
theorem OAI.UniqueGamesTheorem.Appendix.SubmoduleInterval.lowerWeightedTotal_eq line 745
theorem OAI.UniqueGamesTheorem.Appendix.SubmoduleInterval.binary_lower_interval_mobius line 756
def OAI.UniqueGamesTheorem.Fourier.Deletion.trueCount line 774
Source documentation
The number of entries on which a Boolean function is true.
```
def trueCount {Ω : Type u} (f : Ω → Bool) : List Ω → Nat
  | [] => 0
  | x :: xs => (if f x then 1 else 0) + trueCount f xs
```
theorem OAI.UniqueGamesTheorem.Fourier.Deletion.trueCount_mono line 778
theorem OAI.UniqueGamesTheorem.Fourier.Deletion.trueCount_eq_zero line 790
structure OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem line 802
Source documentation
A family of admissible restrictions and their containing rows. Rows may overlap, and there is no requirement that different restrictions share the same ancillary data.
```
structure RestrictionSystem (Ω : Type u) (Row : Type v) (Witness : Type w) where
…
```
def OAI.UniqueGamesTheorem.Fourier.Deletion.Dense line 813
Source documentation
Strict density above the rational threshold p / q when q > 0.
```
def Dense (S : RestrictionSystem Ω Row Witness) (H : Ω → Bool)
    (p q : Nat) (t : Witness) : Prop :=
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem
def OAI.UniqueGamesTheorem.Fourier.Deletion.BadRow line 818
Source documentation
A row is bad when it contains a dense admissible restriction.
```
def BadRow (S : RestrictionSystem Ω Row Witness) (H : Ω → Bool)
    (p q : Nat) (r : Row) : Prop :=
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem
def OAI.UniqueGamesTheorem.Fourier.Deletion.DeletedSet line 823
Source documentation
All points of every bad row are removed.
```
def DeletedSet (S : RestrictionSystem Ω Row Witness) (H : Ω → Bool)
    (p q : Nat) (x : Ω) : Prop :=
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem
def OAI.UniqueGamesTheorem.Fourier.Deletion.remainder line 828
Source documentation
The Boolean remainder after deleting the union of bad rows.
```
noncomputable def remainder (S : RestrictionSystem Ω Row Witness)
    (H : Ω → Bool) (p q : Nat) (x : Ω) : Bool := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem
def OAI.UniqueGamesTheorem.Fourier.Deletion.removed line 834
Source documentation
The Boolean part removed from the original function.
```
noncomputable def removed (S : RestrictionSystem Ω Row Witness)
    (H : Ω → Bool) (p q : Nat) (x : Ω) : Bool := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem
theorem OAI.UniqueGamesTheorem.Fourier.Deletion.remainder_le_original line 839
theorem OAI.UniqueGamesTheorem.Fourier.Deletion.dense_deletes_whole_row line 850
Source documentation
A dense restriction makes its whole row bad, including points that were not sampled by the restriction.
```
theorem dense_deletes_whole_row (S : RestrictionSystem Ω Row Witness)
    (H : Ω → Bool) (p q : Nat) (t : Witness)
    (ha : S.admissible t) (hd : Dense S H p q t)
    (x : Ω) (hx : S.row (S.containingRow t) x) :
    remainder S H p q x = false := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem, OAI.UniqueGamesTheorem.Fourier.Deletion.Dense, OAI.UniqueGamesTheorem.Fourier.Deletion.remainder
theorem OAI.UniqueGamesTheorem.Fourier.Deletion.dense_restriction_remainder_zero line 860
def OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionGlobal line 869
Source documentation
Rational restriction globality of a Boolean function.
```
def RestrictionGlobal (S : RestrictionSystem Ω Row Witness) (G : Ω → Bool)
    (p q : Nat) : Prop :=
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem
theorem OAI.UniqueGamesTheorem.Fourier.Deletion.remainder_restrictionGlobal line 875
Source documentation
Whole-row deletion establishes every admissible restriction bound. This is the first assertion of Lemma 5.2, before applying Fourier estimates.
```
theorem remainder_restrictionGlobal
    (S : RestrictionSystem Ω Row Witness) (H : Ω → Bool) (p q : Nat) :
    RestrictionGlobal S (remainder S H p q) p q := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem, OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionGlobal, OAI.UniqueGamesTheorem.Fourier.Deletion.remainder
theorem OAI.UniqueGamesTheorem.Fourier.Deletion.boolean_partition line 891
Source documentation
Retained and removed contributions form a disjoint Boolean partition.
```
theorem boolean_partition (S : RestrictionSystem Ω Row Witness)
    (H : Ω → Bool) (p q : Nat) (x : Ω) :
    (remainder S H p q x || removed S H p q x) = H x ∧
    (remainder S H p q x && removed S H p q x) = false := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem, OAI.UniqueGamesTheorem.Fourier.Deletion.remainder, OAI.UniqueGamesTheorem.Fourier.Deletion.removed
theorem OAI.UniqueGamesTheorem.Fourier.Deletion.trueCount_partition line 899
Source documentation
Exact conservation of retained and removed mass on any sampling list.
```
theorem trueCount_partition (S : RestrictionSystem Ω Row Witness)
    (H : Ω → Bool) (p q : Nat) (xs : List Ω) :
    trueCount H xs = trueCount (remainder S H p q) xs +
      trueCount (removed S H p q) xs := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem, OAI.UniqueGamesTheorem.Fourier.Deletion.trueCount, OAI.UniqueGamesTheorem.Fourier.Deletion.remainder, OAI.UniqueGamesTheorem.Fourier.Deletion.removed