UniformSubspaces.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform injective parameter maps induce the uniform law on subspaces of the specified rank. The proof uses actual transitivity of ambient linear automorphisms on injections, not an assumed distributional premise.

def OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.Injection line 28
Source documentation
A linear parameter map with its injectivity proof.
```
def Injection (K V W : Type*) [Field K] [AddCommGroup V] [Module K V]
    [AddCommGroup W] [Module K W] :=
…
```
instance OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.injectionAction line 32
theorem OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.injection_transitive line 46
Source documentation
Every two injections are carried to each other by an automorphism of the ambient space: extend the isomorphism between their two images.
```
theorem injection_transitive (J₁ J₂ : Injection K V W) :
    ∃ a : W ≃ₗ[K] W, a • J₁ = J₂ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.Injection
def OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.image line 61
Source documentation
The image has the dimension of the parameter space.
```
def image (J : Injection K V W) : RankSpace K W (finrank K V) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.Injection
theorem OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.image_action line 65
theorem OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.mean_image line 74
Source documentation
Exact uniform image law, conditional only on injectivity of the map.
```
theorem mean_image (J₀ : Injection K V W) (f : RankSpace K W (finrank K V) → ℚ) :
    (∑ J : Injection K V W, f (image J)) / Fintype.card (Injection K V W) =
      (∑ S : RankSpace K W (finrank K V), f S) /
        Fintype.card (RankSpace K W (finrank K V)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.Injection, OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.image
theorem OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.bad_image_count_ratio line 84
Source documentation
Indicator specialization of the exact law, without assuming genericity or independence of a subsequently chosen lift.
```
theorem bad_image_count_ratio (J₀ : Injection K V W)
    (Bad : RankSpace K W (finrank K V) → Prop) :
    (Nat.card {J : Injection K V W // Bad (image J)} : ℚ) /
        Fintype.card (Injection K V W) =
      (Nat.card {S : RankSpace K W (finrank K V) // Bad S} : ℚ) /
        Fintype.card (RankSpace K W (finrank K V)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.Injection, OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.image

theorem OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.bad_subspace_bound line 97

Source documentation

An unconditional bad-parameter count bound transfers after conditioning on injectivity, paying exactly the usual 1/(1-β) factor. The premises are ordinary count inequalities and can come from polynomial union bounds.

theorem bad_subspace_bound (J₀ : Injection K V W)
    (Bad : RankSpace K W (finrank K V) → Prop) (α β : ℚ) (hα : 0 ≤ α) (hβ : β < 1)
    (hbad : (Nat.card {J : Injection K V W // Bad (image J)} : ℚ) ≤
      α * Nat.card (V →ₗ[K] W))
    (hinj : (1 - β) * Nat.card (V →ₗ[K] W) ≤ Fintype.card (Injection K V W)) :
    (Nat.card {S : RankSpace K W (finrank K V) // Bad S} : ℚ) /
        Fintype.card (RankSpace K W (finrank K V)) ≤ α / (1 - β) := by
…

Mentions: OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.Injection, OAI.UniqueGamesTheorem.Quadratic.UniformSubspaces.image