KMSAnalyticHybridCoordinatesRankLemmas.lean`

66 declarations, 0 contain sorry, 0 declared as axioms

The exact injection/surjection factorization of the adapted coordinates.

def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.fullCoordinates line 40
Source documentation
The small frequency map before its last coordinate is embedded into D.
```
def fullCoordinates {z : B →ₗ[R] W}
    (p : Coordinates (A := A) (D := D) (C := C) z) :
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.Coordinates
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.embedLast line 46
Source documentation
The injection chosen by the last block, keeping the first two blocks fixed.
```
def embedLast (v : C →ₗ[R] D) : (A × (W × C)) →ₗ[R] (A × (W × D)) :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.embedLast_apply line 49
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.embedLast_injective line 52
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.assemble_eq_embedLast_comp line 62
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.range_assemble_of_fullCoordinates_surjective line 69
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.finrank_assemble line 76
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.ker_assemble line 83
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.hybridFiberEquiv line 111
Source documentation
The exact coordinate parametrization after imposing the genuine hybrid selector. The two remaining conditions are ordinary injectivity and surjectivity of displayed linear maps.
```
def hybridFiberEquiv (z : B →ₗ[R] W) (hz : Function.Surjective z) :
    {S : (B × C) →ₗ[R] (A × (W × D)) //
      compressBlock S = z.prod (0 : B →ₗ[R] D) ∧
        LinearIdentities.Hybrid S
          (LinearMap.range (LinearMap.inl R A (W × D)))
          (LinearMap.range (LinearMap.inl R B C))} ≃
      {p : Coordinates (A := A) (D := D) (C := C) z //
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.compressBlock, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.Coordinates

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.hybridFiber_finrank line 133

Source documentation

Every map in the actual fiber has the prescribed small rank.

theorem hybridFiber_finrank (z : B →ₗ[R] W) (hz : Function.Surjective z)
    (S : (B × C) →ₗ[R] (A × (W × D)))
    (hc : compressBlock S = z.prod (0 : B →ₗ[R] D))
    (hh : LinearIdentities.Hybrid S
      (LinearMap.range (LinearMap.inl R A (W × D)))
      (LinearMap.range (LinearMap.inl R B C))) :
    Module.finrank R S.range = Module.finrank R (A × (W × C)) := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.compressBlock

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.phase_weighted_sum_sq_le line 167
Source documentation
Unit-bounded squared phases cost at most the number of summands in the finite Cauchy--Schwarz inequality.
```
theorem phase_weighted_sum_sq_le {Ψ : Type*} (s : Finset Ψ)
    (b H : Ψ → ℝ) (hb : ∀ ψ ∈ s, b ψ ^ 2 ≤ 1) :
    (∑ ψ ∈ s, b ψ * H ψ) ^ 2 ≤ (s.card : ℝ) * ∑ ψ ∈ s, H ψ ^ 2 := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.phase_sum_sq_le_card_sq line 179
Source documentation
A finite sum of phases has square at most the squared cardinality. The statement also covers an empty indexing type.
```
theorem phase_sum_sq_le_card_sq {V : Type*} [Fintype V]
    (a : V → ℝ) (ha : ∀ v, a v ^ 2 ≤ 1) :
    (∑ v, a v) ^ 2 ≤ (Fintype.card V : ℝ) ^ 2 := by
…
```

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sum_fiber_phase_sq_le line 189

Source documentation

Summing the Cauchy--Schwarz bounds over the disjoint restriction fibers loses only the largest fiber cardinality.

theorem sum_fiber_phase_sq_le {Ψ Z : Type*} [Fintype Ψ] [Fintype Z]
    (r : Ψ → Z) (b H : Ψ → ℝ) (maxFiber : ℕ)
    (hb : ∀ ψ, b ψ ^ 2 ≤ 1)
    (hcard : ∀ z, (Finset.univ.filter (fun ψ => r ψ = z)).card ≤ maxFiber) :
    (∑ z, (∑ ψ with r ψ = z, b ψ * H ψ) ^ 2) ≤
      (maxFiber : ℝ) * ∑ ψ, H ψ ^ 2 := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sum_fiber_product_sq_le line 214

Source documentation

The hybrid coefficient factorization has energy bounded by the squared number of complementary choices times the extension-fiber size and the original mixed coefficient energy. No phase cancellation is assumed.

theorem sum_fiber_product_sq_le {V Ψ Z : Type*}
    [Fintype V] [Fintype Ψ] [Fintype Z]
    (r : Ψ → Z) (a : V → ℝ) (b H : Ψ → ℝ) (maxFiber : ℕ)
    (ha : ∀ v, a v ^ 2 ≤ 1) (hb : ∀ ψ, b ψ ^ 2 ≤ 1)
    (hcard : ∀ z, (Finset.univ.filter (fun ψ => r ψ = z)).card ≤ maxFiber) :
    (∑ z, ((∑ v, a v) * (∑ ψ with r ψ = z, b ψ * H ψ)) ^ 2) ≤
      (Fintype.card V : ℝ) ^ 2 * (maxFiber : ℝ) * ∑ ψ, H ψ ^ 2 := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.range_subtype_comp_of_surjective line 261
Source documentation
The inclusion of the target subspace preserves the prescribed image of a surjective map.
```
theorem range_subtype_comp_of_surjective (W : Submodule R U)
    (z : B →ₗ[R] W) (hz : Function.Surjective z) :
    (W.subtype.comp z).range = W := by
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.fixedImageEquivSurjection line 273
Source documentation
The full fixed-image fiber, with its canonical surjective coordinates.
```
def fixedImageEquivSurjection (W : Submodule R U) :
    {z : B →ₗ[R] U // z.range = W} ≃
      {z : B →ₗ[R] W // Function.Surjective z} where
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.fixedImageEquivSurjection_symm_val line 294
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.fixedImageEquivSurjection_apply_coe line 298
abbrev OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency line 303
Source documentation
Frequencies of an exact rank.
```
abbrev ImageRankFrequency (q : ℕ) :=
…
```
abbrev OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.RankImage line 307
Source documentation
Actual image subspaces of the required dimension.
```
abbrev RankImage (R U : Type*) [Ring R] [AddCommGroup U] [Module R U] (q : ℕ) :=
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.frequencyImage line 311
Source documentation
The image classification of an exact-rank frequency.
```
def frequencyImage (q : ℕ) (z : ImageRankFrequency (R := R) (B := B) (U := U) q) :
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.frequencyImageFiberEquiv line 315
Source documentation
Removing the redundant rank certificate from a fixed-image fiber.
```
def frequencyImageFiberEquiv (q : ℕ) (W : RankImage R U q) :
    {z : ImageRankFrequency (R := R) (B := B) (U := U) q // frequencyImage q z = W} ≃
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.RankImage, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.frequencyImage
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.rankFrequencyImageEquiv line 325
Source documentation
Exact rank frequencies are in bijection with a choice of actual image and a surjective map onto it.
```
def rankFrequencyImageEquiv (q : ℕ) :
    ImageRankFrequency (R := R) (B := B) (U := U) q ≃
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.rankFrequencyImageEquiv_symm_val line 332

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sum_fixedImage_eq_sum_surjection line 343

Source documentation

Exact fixed-image reindexing for arbitrary real weights.

theorem sum_fixedImage_eq_sum_surjection (W : Submodule R U)
    (weight : (B →ₗ[R] U) → ℝ) :
    (∑ z : {z : B →ₗ[R] U // z.range = W}, weight z.val) =
      ∑ z : {z : B →ₗ[R] W // Function.Surjective z}, weight (W.subtype.comp z.val) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sum_rankFrequency_eq_sum_image line 353
Source documentation
Partition the exact-rank frequency sum by the actual image subspace.
```
theorem sum_rankFrequency_eq_sum_image (q : ℕ) (weight : (B →ₗ[R] U) → ℝ) :
    (∑ z : ImageRankFrequency (R := R) (B := B) (U := U) q, weight z.val) =
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sum_filter_rank_eq_sum_image line 370
Source documentation
The same partition in filtered-sum form, convenient for Fourier support conditions that are expressed as vanishing away from one rank.
```
theorem sum_filter_rank_eq_sum_image (q : ℕ) (weight : (B →ₗ[R] U) → ℝ) :
    (∑ z : B →ₗ[R] U with Module.finrank R z.range = q, weight z) =
      ∑ W : RankImage R U q,
        ∑ z : {z : B →ₗ[R] W.val // Function.Surjective z},
          weight (W.val.subtype.comp z.val) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.RankImage

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sum_eq_sum_image_of_rank_support line 382

Source documentation

If a weight vanishes outside rank q, the full sum has the same exact image partition. No positivity assumption on the weight is needed.

theorem sum_eq_sum_image_of_rank_support (q : ℕ) (weight : (B →ₗ[R] U) → ℝ)
    (hsupport : ∀ z, Module.finrank R z.range ≠ q → weight z = 0) :
    (∑ z : B →ₗ[R] U, weight z) =
      ∑ W : RankImage R U q,
        ∑ z : {z : B →ₗ[R] W.val // Function.Surjective z},
          weight (W.val.subtype.comp z.val) := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.RankImage

def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageCoordinates line 402
Source documentation
Coordinates adapted to a prescribed image and any chosen complement.
```
def imageCoordinates (W D : Submodule K V) (h : IsCompl W D) : V ≃ₗ[K] (W × D) :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageCoordinates_subtype line 406
Source documentation
Vectors in the prescribed image have zero complementary coordinate.
```
@[simp] theorem imageCoordinates_subtype (W D : Submodule K V) (h : IsCompl W D)
    (w : W) : imageCoordinates W D h (w : V) = (w, 0) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageCoordinates
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageCoordinates_frequency line 412
Source documentation
Each fixed-image frequency has exactly the block form used by the compressed Hybrid-coordinate parametrization.
```
theorem imageCoordinates_frequency {X : Type*} [AddCommGroup X] [Module K X]
    (W D : Submodule K V) (h : IsCompl W D) (z : X →ₗ[K] W) :
    (imageCoordinates W D h).toLinearMap.comp (W.subtype.comp z) =
      z.prod (0 : X →ₗ[K] D) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageCoordinates
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageCoordinates_finrank line 421
Source documentation
A complement contributes exactly the remaining ambient dimension.
```
theorem imageCoordinates_finrank [FiniteDimensional K V]
    (W D : Submodule K V) (h : IsCompl W D) :
    Module.finrank K W + Module.finrank K D = Module.finrank K V := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.exists_imageCoordinates line 427
Source documentation
Every image subspace admits the required product coordinates.
```
theorem exists_imageCoordinates (W : Submodule K V) :
    ∃ D : Submodule K V, ∃ e : V ≃ₗ[K] (W × D), ∀ w : W, e (w : V) = (w, 0) := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.ker_comp_mkQ line 459
Source documentation
Composing an injective map with the quotient projection has exactly the prescribed kernel.
```
theorem ker_comp_mkQ (K : Submodule R F) (J : (F ⧸ K) →ₗ[R] E)
    (hJ : Function.Injective J) : (J.comp K.mkQ).ker = K := by
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.fixedKernelEquivQuotientInjection line 466
Source documentation
Every map with kernel K factors uniquely through an injective quotient map; the inverse sends that quotient map to its composition with K.mkQ.
```
def fixedKernelEquivQuotientInjection (K : Submodule R F) :
    {S : F →ₗ[R] E // S.ker = K} ≃
      {J : (F ⧸ K) →ₗ[R] E // Function.Injective J} where
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.fixedKernelEquiv_apply_mkQ line 483
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.fixedKernelEquiv_symm_apply line 488
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.range_forward line 493
Source documentation
Quotient factorization leaves the image subspace unchanged.
```
theorem range_forward (K : Submodule R F)
    (S : {S : F →ₗ[R] E // S.ker = K}) :
    (fixedKernelEquivQuotientInjection K S).val.range = S.val.range :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.fixedKernelEquivQuotientInjection
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.finrank_range_forward line 499
Source documentation
The quotient lift has the same rank as the original map.
```
theorem finrank_range_forward (K : Submodule R F)
    (S : {S : F →ₗ[R] E // S.ker = K}) :
    Module.finrank R (fixedKernelEquivQuotientInjection K S).val.range =
      Module.finrank R S.val.range := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.fixedKernelEquivQuotientInjection
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.fixedKernel_finrank_eq_quotient line 506
Source documentation
A prescribed kernel fixes the rank to the dimension of its quotient.
```
theorem fixedKernel_finrank_eq_quotient (K : Submodule R F)
    (S : {S : F →ₗ[R] E // S.ker = K}) :
    Module.finrank R S.val.range = Module.finrank R (F ⧸ K) := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.range_comp_mkQ line 514
Source documentation
Surjectivity of the quotient projection preserves the range of any map defined on the quotient.
```
theorem range_comp_mkQ (K : Submodule R F) (J : (F ⧸ K) →ₗ[R] E) :
    (J.comp K.mkQ).range = J.range := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.quotientInjection_comp_finrank line 526
Source documentation
The inverse factorization of an injection has quotient dimension as its rank. In the finite-dimensional binary case this is the ordinary finite rank.
```
theorem quotientInjection_comp_finrank (K : Submodule R F)
    (J : (F ⧸ K) →ₗ[R] E) (hJ : Function.Injective J) :
    Module.finrank R (J.comp K.mkQ).range = Module.finrank R (F ⧸ K) := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.natCard_fixedKernel_eq_injectiveQuotient line 533
Source documentation
Exact fixed-kernel count, stated without requiring a chosen enumeration.
```
theorem natCard_fixedKernel_eq_injectiveQuotient (K : Submodule R F) :
    Nat.card {S : F →ₗ[R] E // S.ker = K} =
      Nat.card {J : (F ⧸ K) →ₗ[R] E // Function.Injective J} :=
…
```

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticKernelCount.card_fixedKernel_eq_injectiveQuotient line 539

Source documentation

The same counting equality for any finite enumerations of the two sides.

theorem card_fixedKernel_eq_injectiveQuotient (K : Submodule R F)
    [Fintype {S : F →ₗ[R] E // S.ker = K}]
    [Fintype {J : (F ⧸ K) →ₗ[R] E // Function.Injective J}] :
    Fintype.card {S : F →ₗ[R] E // S.ker = K} =
      Fintype.card {J : (F ⧸ K) →ₗ[R] E // Function.Injective J} :=
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedCharacter_constant_step line 561

Source documentation

The recurrence cost in Lemma 3.19 is absorbed by 2^(4 i²). The proof only needs n < ell, weaker than the usual 2*(n+1) ≤ ell induction hypothesis.

theorem fixedCharacter_constant_step (n m ell : ℕ) (hnell : n < ell) :
    (2 : ℝ) ^ n * ((2 : ℝ) ^ n + 1) ^ 2 * (2 : ℝ) ^ (4 * n * n) /
        ((((2 : ℝ) ^ ell - (2 : ℝ) ^ n) ^ 2) * (2 : ℝ) ^ ((n + m) * ell)) ≤
      (2 : ℝ) ^ (4 * (n + 1) * (n + 1)) /
        (2 : ℝ) ^ (((n + 1) + (m + 1)) * ell) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.expect_coe_eq line 643
Source documentation
Finset conditioning and uniform sampling from its membership subtype are the same normalized finite sum, including the empty event.
```
theorem expect_coe_eq (s : Finset Ω) (f : Ω → ℝ) :
    (𝔼 x : s, f x.val) = s.expect f := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.expect_unit_interval line 649
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.mass_mul_expect line 659
Source documentation
The weighted conditional expectation is the unnormalized sum divided by the ambient cardinality, also for an empty conditioning event.
```
theorem mass_mul_expect (s : Finset Ω) (f : Ω → ℝ) :
    (s.card : ℝ) / Fintype.card Ω * s.expect f =
      (∑ x ∈ s, f x) / Fintype.card Ω := by
…
```

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.expect_partition line 672

Source documentation

Exact two-event total expectation, with the same zero convention on both conditional expectations as mathlib's finite expectation.

theorem expect_partition (s : Finset Ω) (f : Ω → ℝ) :
    (𝔼 x, f x) =
      (s.card : ℝ) / Fintype.card Ω * s.expect f +
      ((Finset.univ \ s).card : ℝ) / Fintype.card Ω *
        (Finset.univ \ s).expect f := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.abs_expect_sub_restrict_le line 683
Source documentation
Conditioning a bounded function changes its expectation by at most the discarded probability mass. No independence assumption is used here.
```
theorem abs_expect_sub_restrict_le [Nonempty Ω] (s : Finset Ω) (f : Ω → ℝ)
    (hf0 : ∀ x, 0 ≤ f x) (hf1 : ∀ x, f x ≤ 1) :
    |(𝔼 x, f x) - s.expect f| ≤
      ((Finset.univ \ s).card : ℝ) / Fintype.card Ω := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.binary_functional_eq_of_ker_eq line 729
Source documentation
A binary functional is determined by its zero set.
```
theorem binary_functional_eq_of_ker_eq
    {a b : E →ₗ[ZMod 2] ZMod 2} (h : a.ker = b.ker) : a = b := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.binary_functional_eq_of_map_ker_eq line 745
Source documentation
The image of a binary functional's kernel under an injective linear map still determines that functional uniquely.
```
theorem binary_functional_eq_of_map_ker_eq
    (X : E →ₗ[ZMod 2] F) (hX : Function.Injective X)
    {a b : E →ₗ[ZMod 2] ZMod 2}
    (h : a.ker.map X = b.ker.map X) : a = b := by
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion line 775
Source documentation
Ordered completions in W of Q to an independent spanning tuple for L.
```
def RestrictedCompletion (Q : Fin q → V) (W L : Submodule K V) :=
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionBasis line 783
Source documentation
A completion, regarded as a basis of the resulting subspace.
```
def completionBasis (z : RestrictedCompletion (t := t) Q W L) :
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionBasis_coe line 787
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionOfBasis line 793
Source documentation
Recover a restricted completion from a basis having the prescribed prefix.
```
def completionOfBasis (b : Module.Basis (Fin q ⊕ Fin t) K L)
    (hQ : ∀ i, (b (Sum.inl i) : V) = Q i)
    (hW : ∀ i, (b (Sum.inr i) : V) ∈ W) :
    RestrictedCompletion (t := t) Q W L := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv line 815
Source documentation
The unique basis change carrying the first completion to the second.
```
def completionSpanEquiv
    (x : RestrictedCompletion (t := t) Q W L)
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv_basis line 820
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv_symm line 826
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv_sub_mem line 833
Source documentation
Changing the completion changes every vector by an element of W.
```
theorem completionSpanEquiv_sub_mem
    (x : RestrictedCompletion (t := t) Q W L)
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv_mem_iff line 854
Source documentation
The basis change preserves membership in W, without requiring Q ⊆ W.
```
theorem completionSpanEquiv_mem_iff
    (x : RestrictedCompletion (t := t) Q W L)
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.transportCompletion line 866
Source documentation
Transport every restricted completion along one fixed basis change.
```
def transportCompletion
    (x : RestrictedCompletion (t := t) Q W L)
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.transportCompletion_coe line 884
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.transportCompletion_inverse line 891
def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.restrictedCompletionEquiv line 908
Source documentation
All nonempty restricted-completion fibers are equivalent.
```
def restrictedCompletionEquiv
    (x : RestrictedCompletion (t := t) Q W L)
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.restrictedCompletionCard_eq line 918
Source documentation
Equal fiber cardinality follows from the explicit completion equivalence.
```
theorem restrictedCompletionCard_eq
    (x : RestrictedCompletion (t := t) Q W L)
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion