KMSFoundationLemmas.lean`

52 declarations, 0 contain sorry, 0 declared as axioms

An independent frame inside L can be completed using vectors from W whenever L lies in the sum of the frame's span and W.

def OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity line 29
Source documentation
Relative density, with value zero when the conditioning set is empty.
```
def relativeDensity (S I : Finset Ω) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMS.inter_chart_eq line 34
Source documentation
Restricting the denominator to a chart containing the set preserves the numerator. This is the exact finite-set step used after Grassmann expansion.
```
theorem inter_chart_eq (S I C : Finset Ω) (hSC : S ⊆ C) :
    S ∩ (I ∩ C) = S ∩ I := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMS.chart_inter_nonempty line 46
Source documentation
A nonempty part of the set in an interval witnesses that the chart and interval meet. No positive denominator is silently assumed.
```
theorem chart_inter_nonempty (S I C : Finset Ω) (hSC : S ⊆ C)
    (hSI : (S ∩ I).Nonempty) : (I ∩ C).Nonempty := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity_le_chart line 54
Source documentation
Intersecting a nonempty conditioning interval with a chart containing the set can only increase its relative density.
```
theorem relativeDensity_le_chart (S I C : Finset Ω) (hSC : S ⊆ C)
    (hIC : (I ∩ C).Nonempty) :
    relativeDensity S I ≤ relativeDensity S (I ∩ C) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity
theorem OAI.UniqueGamesTheorem.Inverse.KMS.density_bound_passes_to_chart line 65
Source documentation
The quantitative density conclusion passes to the matrix chart without losing any factor.
```
theorem density_bound_passes_to_chart (S I C : Finset Ω) (hSC : S ⊆ C)
    (hSI : (S ∩ I).Nonempty) {α : ℝ} (hα : α ≤ relativeDensity S I) :
    (I ∩ C).Nonempty ∧ α ≤ relativeDensity S (I ∩ C) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity
abbrev OAI.UniqueGamesTheorem.Inverse.KMS.F2 line 73
abbrev OAI.UniqueGamesTheorem.Inverse.KMS.Ambient line 74
def OAI.UniqueGamesTheorem.Inverse.KMS.Vertex line 77
Source documentation
Actual ell-dimensional subspaces of the ambient binary vector space.
```
def Vertex (n ell : ℕ) :=
…
```
instance OAI.UniqueGamesTheorem.Inverse.KMS.vertexFinite line 80
instance OAI.UniqueGamesTheorem.Inverse.KMS.vertexFintype line 87
def OAI.UniqueGamesTheorem.Inverse.KMS.Adjacent line 91
Source documentation
A neighbor is distinct and meets the vertex in a hyperplane. The explicit distinctness also makes the definition harmless at dimension zero.
```
def Adjacent {n ell : ℕ} (L M : Vertex n ell) : Prop :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex
def OAI.UniqueGamesTheorem.Inverse.KMS.neighbors line 94
def OAI.UniqueGamesTheorem.Inverse.KMS.retention line 98
Source documentation
Uniform start in S, followed by a uniform Grassmann neighbor.
```
def retention {n ell : ℕ} (S : Finset (Vertex n ell)) : ℝ :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex
def OAI.UniqueGamesTheorem.Inverse.KMS.interval line 102
Source documentation
The actual interval A ≤ L ≤ B among the ell-dimensional vertices.
```
def interval {n ell : ℕ} (A B : Submodule F2 (Ambient n)) :
    Finset (Vertex n ell) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.F2, OAI.UniqueGamesTheorem.Inverse.KMS.Ambient, OAI.UniqueGamesTheorem.Inverse.KMS.Vertex
def OAI.UniqueGamesTheorem.Inverse.KMS.ExpansionPrinciple line 109
Source documentation
The parameter order needed from KMS, including a nonempty dense interval. The parameters r and alpha must be fixed before ell, and the ambient threshold may then depend on ell. A bound with alpha = 2^(-ell) does not meet this interface.
```
def ExpansionPrinciple : Prop :=
…
```

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.exists_restricted_completion line 139

Source documentation

Restricted completion of an independent frame. The original vectors need not belong to W; only the newly chosen vectors are required to do so.

theorem exists_restricted_completion {n q t : ℕ}
    (Q : Fin q → Ambient n) (W L : Submodule F2 (Ambient n))
    (hQ : LinearIndependent F2 Q)
    (hQL : Submodule.span F2 (Set.range Q) ≤ L)
    (hLW : L ≤ Submodule.span F2 (Set.range Q) ⊔ W)
    (hL : Module.finrank F2 L = q + t) :
    ∃ z : Fin t → W,
      LinearIndependent F2 (Sum.elim Q (fun i => (z i : Ambient n))) ∧
        Submodule.span F2
          (Set.range (Sum.elim Q (fun i => (z i : Ambient n)))) = L := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.nat_card_eq_sum_fibers line 219
Source documentation
Decompose a finite domain by its exact fibers.
```
theorem nat_card_eq_sum_fibers (f : X → Y) :
    Nat.card X = ∑ y : Y, Nat.card {x : X // f x = y} := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.nat_card_event_eq_sum_fibers line 224
Source documentation
The event count is the sum of the same fibers over the event.
```
theorem nat_card_event_eq_sum_fibers (f : X → Y) (p : Y → Prop) :
    Nat.card {x : X // p (f x)} =
      ∑ y : {y : Y // p y}, Nat.card {x : X // f x = y.val} := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.uniformFiber_card_ratio line 237
Source documentation
Constant fibers give an exact density identity, including an empty target. The nonzero fiber size is established geometrically for restricted bases.
```
theorem uniformFiber_card_ratio (f : X → Y) (p : Y → Prop)
    (c : ℕ) (hc : 0 < c)
    (hf : ∀ y, Nat.card {x : X // f x = y} = c) :
    (Nat.card {x : X // p (f x)} : ℝ) / Nat.card X =
      (Nat.card {y : Y // p y} : ℝ) / Nat.card Y := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.subtype_event_ratio_le line 256
Source documentation
Sampling from a larger finite space and accepting only a subset never increases the density of an event within that subset. Empty subsets are handled explicitly, so this statement makes no hidden nonemptiness assumption.
```
theorem subtype_event_ratio_le {Z : Type*} [Fintype Z] (D : Z → Prop)
    (p : {z : Z // D z} → Prop) :
    (Nat.card {z : {z : Z // D z} // p z} : ℝ) / Nat.card Z ≤
      (Nat.card {z : {z : Z // D z} // p z} : ℝ) / Nat.card {z : Z // D z} := by
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.prefixSpan line 295
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.joinedTuple line 298
abbrev OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.IndependentCompletion line 302
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionVertex line 305
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.prefix_le_completion line 310
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completion_le_sup line 317
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completion_mem_interval line 329
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.prefix_independent line 335
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.interval_complexity_le line 341
Source documentation
The restriction's Grassmann interval satisfies the same total complexity budget. This uses only W ≤ span Q ⊔ W, never the false assumption Q ⊆ W.
```
theorem interval_complexity_le (Q : Fin q → Ambient n) (W : Submodule F2 (Ambient n))
    (hQ : LinearIndependent F2 Q) :
    Module.finrank F2 (prefixSpan Q) +
      (n - Module.finrank F2 ↥(prefixSpan Q ⊔ W : Submodule F2 (Ambient n))) ≤
        q + (n - Module.finrank F2 W) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.prefixSpan
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.GrassmannPseudorandom line 355
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionEvent line 361
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity line 367
Source documentation
The denominator counts all remaining tuples drawn uniformly from W. Dependent completions are rejected, without conditioning away their mass.
```
def restrictedLiftDensity (S : Finset (Vertex n (q + t)))
    (Q : Fin q → Ambient n) (W : Submodule F2 (Ambient n)) : ℝ :=
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.TuplePseudorandom line 372
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity_eq_zero_of_dependent line 378
abbrev OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.IntervalVertex line 388
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionIntervalVertex line 391
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionFiberEquiv line 395
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.interval_completion_nonempty line 405
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionEventEquiv line 414
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.intervalEventEquiv line 423
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.independent_density_eq_interval line 435
Source documentation
The uniform law on successful completions is exactly the uniform Grassmann interval law, even when the fixed prefix is not contained in W.
```
theorem independent_density_eq_interval (S : Finset (Vertex n (q + t)))
    (Q : Fin q → Ambient n) (W : Submodule F2 (Ambient n))
    (hQ : LinearIndependent F2 Q)
    (z₀ : IndependentCompletion (t := t) Q W) :
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.IndependentCompletion
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity_le_interval line 466
Source documentation
The unconditioned restricted lift has density at most that of its exact Grassmann interval. Unlike a union-bound argument, no independence-error term is needed because dependent tuples are rejected by the lift.
```
theorem restrictedLiftDensity_le_interval (S : Finset (Vertex n (q + t)))
    (Q : Fin q → Ambient n) (W : Submodule F2 (Ambient n))
    (hQ : LinearIndependent F2 Q) :
    restrictedLiftDensity S Q W ≤
      relativeDensity S (interval (prefixSpan Q) (prefixSpan Q ⊔ W)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.prefixSpan
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.grassmann_pseudorandom_restricted line 484
Source documentation
The full KMS restriction transfer, with the stronger exact ε bound.
```
theorem grassmann_pseudorandom_restricted {r : ℕ} {ε : ℝ}
    (S : Finset (Vertex n (q + t))) (hS : GrassmannPseudorandom S r ε)
    (hε : 0 ≤ ε) (Q : Fin q → Ambient n) (W : Submodule F2 (Ambient n))
    (hbudget : q + (n - Module.finrank F2 W) ≤ r) :
    restrictedLiftDensity S Q W ≤ ε := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.GrassmannPseudorandom, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.grassmann_pseudorandom_lift line 496
theorem OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity_map line 520
Source documentation
An embedding preserves the numerator and denominator of relative density.
```
theorem relativeDensity_map (e : Ω ↪ Γ) (S I : Finset Ω) :
    relativeDensity (S.map e) (I.map e) = relativeDensity S I := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity
theorem OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity_equiv line 526
def OAI.UniqueGamesTheorem.Inverse.KMS.finiteChart line 534
Source documentation
The image of the entire finite matrix domain.
```
def finiteChart (e : Ω ↪ Γ) : Finset Γ := Finset.univ.map e
```
def OAI.UniqueGamesTheorem.Inverse.KMS.intervalPreimage line 537
Source documentation
Matrices whose chart images lie in an ambient interval.
```
def intervalPreimage (e : Ω ↪ Γ) (I : Finset Γ) : Finset Ω :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMS.map_intervalPreimage line 541
theorem OAI.UniqueGamesTheorem.Inverse.KMS.mapped_subset_finiteChart line 555
theorem OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity_intervalPreimage line 563
Source documentation
Pulling the chart-intersected interval back to matrices preserves density exactly; matrices are sampled uniformly on this actual preimage.
```
theorem relativeDensity_intervalPreimage (e : Ω ↪ Γ) (S : Finset Ω) (I : Finset Γ) :
    relativeDensity (S.map e) (I ∩ finiteChart e) =
      relativeDensity S (intervalPreimage e I) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity, OAI.UniqueGamesTheorem.Inverse.KMS.finiteChart, OAI.UniqueGamesTheorem.Inverse.KMS.intervalPreimage
theorem OAI.UniqueGamesTheorem.Inverse.KMS.ambient_density_passes_to_preimage line 571
Source documentation
A nonempty lifted fiber in an ambient interval yields a nonempty matrix slice and loses no relative-density factor on transport.
```
theorem ambient_density_passes_to_preimage (e : Ω ↪ Γ)
    (S : Finset Ω) (I : Finset Γ) (hSI : (S.map e ∩ I).Nonempty)
    {α : ℝ} (hα : α ≤ relativeDensity (S.map e) I) :
    (intervalPreimage e I).Nonempty ∧ α ≤ relativeDensity S (intervalPreimage e I) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity, OAI.UniqueGamesTheorem.Inverse.KMS.intervalPreimage