KMSAffineRestrictionComplementLemmas.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

Complements adapted to an affine restriction. The prescribed directions are contained in a small summand, and the complementary directions are mapped into the prescribed target subspace. This is ordinary finite-dimensional geometry; no Fourier inequality or pseudorandomness hypothesis is used.

theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionComplement.exists_bounded_complement_of_linearMap line 28

Source documentation

Enlarge prescribed directions by at most the rank of L, leaving a complement on which L vanishes.

theorem exists_bounded_complement_of_linearMap
    (V1 : Submodule K E) (L : E →ₗ[K] F) :
    ∃ U E0 : Submodule K E,
      V1 ≤ U ∧ E0 ≤ LinearMap.ker L ∧ IsCompl U E0 ∧
      Module.finrank K U ≤
        Module.finrank K V1 + Module.finrank K (LinearMap.range L) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionComplement.exists_bounded_complement line 49

Source documentation

Split the domain while preserving V1 and mapping all complementary directions into W. The extra dimension is at most the codimension of W.

theorem exists_bounded_complement [FiniteDimensional K F]
    (V1 : Submodule K E) (W : Submodule K F) (T : E →ₗ[K] F) :
    ∃ U E0 : Submodule K E,
      V1 ≤ U ∧ E0 ≤ LinearMap.ker (W.mkQ.comp T) ∧ IsCompl U E0 ∧
      Module.finrank K U ≤
        Module.finrank K V1 + Module.finrank K (F ⧸ W) := by
…

def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticFunctionalSplit.splitEquiv line 78
Source documentation
Split off the coordinate measured by a, using the prescribed vector t. The kernel coordinate is exactly x - a x • t.
```
def splitEquiv (a : F →ₗ[K] K) (t : F) (ht : a t = 1) :
    F ≃ₗ[K] (a.ker × K) where
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_apply_snd line 107
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_apply_fst_coe line 110
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_symm_apply line 113
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_symm_apply_zero line 117
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_apply_ker line 121
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_apply_unit line 126
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticFunctionalSplit.finrank_eq_ker_add_one line 132
Source documentation
A functional with a unit preimage has a kernel of codimension one.
```
theorem finrank_eq_ker_add_one [FiniteDimensional K F]
    (a : F →ₗ[K] K) (t : F) (ht : a t = 1) :
    Module.finrank K F = Module.finrank K a.ker + 1 := by
…
```
abbrev OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.F2 line 155
structure OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting line 164
Source documentation
Data of one common coordinate and compatible section vectors. All maps and all smaller spaces below are constructed from these original data.
```
structure CompatibleSplitting (π : I →ₗ[F2] K) (A : F →ₗ[F2] K) where
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.F2
abbrev OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.K0 line 179
abbrev OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.J line 180
abbrev OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.B line 181
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.targetEquiv line 183
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftEquiv line 187
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightEquiv line 192
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftMap line 198
Source documentation
The remaining part of the left surjection is its literal restriction.
```
def leftMap (s : CompatibleSplitting π A) : s.J →ₗ[F2] s.K0 :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.F2
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightMap line 203
Source documentation
The remaining part of the right surjection is its literal restriction.
```
def rightMap (s : CompatibleSplitting π A) : s.B →ₗ[F2] s.K0 :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.F2
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftMap_apply_val line 207
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightMap_apply_val line 210
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftMap_surjective line 213
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightMap_surjective line 224
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftEquiv_symm_apply line 235
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightEquiv_symm_apply line 238
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.targetEquiv_symm_apply line 241
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.left_symm_apply line 244
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.right_symm_apply line 249
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.left_conjugation line 255
Source documentation
Both changes of coordinates use the same final binary coordinate.
```
theorem left_conjugation (s : CompatibleSplitting π A) :
    s.targetEquiv.toLinearMap.comp (π.comp s.leftEquiv.symm.toLinearMap) =
      s.leftMap.prodMap (LinearMap.id : F2 →ₗ[F2] F2) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.F2
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.right_conjugation line 263
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.target_finrank line 271
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.left_finrank line 276
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.right_finrank line 282
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.exists_compatibleSplitting line 292
Source documentation
Positive target dimension supplies a basis coordinate; surjectivity supplies its two lifts. No additional splitting hypothesis is required.
```
theorem exists_compatibleSplitting [FiniteDimensional F2 K]
    (π : I →ₗ[F2] K) (A : F →ₗ[F2] K)
    (hπ : Function.Surjective π) (hA : Function.Surjective A)
    (hdim : 0 < Module.finrank F2 K) : Nonempty (CompatibleSplitting π A) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.F2, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticCompatibleSplitting.chooseSplit line 304
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.compressBlock line 325
Source documentation
The chosen block compression: restrict to B, then forget A.
```
def compressBlock (S : (B × C) →ₗ[R] (A × (W × D))) : B →ₗ[R] (W × D) :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.compressBlock_apply line 328
structure OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.Coordinates line 333
Source documentation
Coordinates of a map whose compression is (z,0).
```
structure Coordinates (z : B →ₗ[R] W) where
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.Coordinates.ext line 339
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.assemble line 349
Source documentation
Assemble the three blocks. The last coordinate vanishes on B.
```
def assemble {z : B →ₗ[R] W} (p : Coordinates (A := A) (D := D) (C := C) z) :
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.Coordinates
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.assemble_apply line 353
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.compressBlock_assemble line 357
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.extract line 367
Source documentation
Extract the unique coordinates from an actual compressed-fiber element.
```
def extract (z : B →ₗ[R] W)
    (S : {S : (B × C) →ₗ[R] (A × (W × D)) //
      compressBlock S = z.prod (0 : B →ₗ[R] D)}) :
    Coordinates (A := A) (D := D) (C := C) z where
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.compressBlock, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.Coordinates
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.assemble_extract line 380
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.extract_assemble line 399
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.compressedFiberEquiv line 414
Source documentation
An exact compressed-fiber parametrization, valid over any ring.
```
def compressedFiberEquiv (z : B →ₗ[R] W) :
    {S : (B × C) →ₗ[R] (A × (W × D)) //
      compressBlock S = z.prod (0 : B →ₗ[R] D)} ≃
      Coordinates (A := A) (D := D) (C := C) z where
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.compressBlock, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.Coordinates
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.assemble_injective line 425
Source documentation
Equality of assembled maps forces equality of every chosen coordinate; there are no hidden change-of-basis fibers in this parametrization.
```
theorem assemble_injective (z : B →ₗ[R] W) :
    Function.Injective (assemble (R := R) (A := A) (D := D) (C := C) (z := z)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.assemble