OAI/Computability/UniqueGames/Inverse/MatrixChartIntervalsLemmas.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Every Grassmann interval has a chart description with exactly dim A lower equations and codim B upper equations. This supplies the quantitative row/column budget used when the expansion theorem selects an interval.

  1. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.span_basis_values line 23
  2. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.lowerRows_basis line 30
  3. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.mem_iff_annihilator_basis line 36

    Source documentation

    Checking an annihilator basis suffices to test membership in a subspace.

    theorem mem_iff_annihilator_basis {ι : Type*} (B : Submodule K (X × Y))
    (b : Module.Basis ι K B.dualAnnihilator) (x : X × Y) :
    x ∈ B ↔ ∀ i, (b i).val x = 0 := by
…
  4. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.functional_coordinate_decomposition line 51

    Source documentation

    Split a product functional into its two coordinate functionals.

    theorem functional_coordinate_decomposition (φ : (X × Y) →ₗ[K] K) (x : X) (y : Y) :
    φ (x, y) = φ (x, 0) + φ (0, y) := by
…
  5. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.upperColumns_annihilator_basis line 56
  6. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.exists_interval_coordinates line 79

    Source documentation

    Coordinates for an arbitrary interval. There are exactly dim A rows and codim B columns, so an interval order bound gives the required slice bound.

    theorem exists_interval_coordinates [FiniteDimensional K X] [FiniteDimensional K Y]
    (A B : Submodule K (X × Y)) :
    ∃ (n_r n_c : Nat) (d : Fin n_r → X) (s : Fin n_r → Y)
      (t : Fin n_c → X →ₗ[K] K) (q : Fin n_c → Y →ₗ[K] K),
      n_r = Module.finrank K A ∧ n_c = Module.finrank K ((X × Y) ⧸ B) ∧
      ∀ T : X →ₗ[K] Y,
        (A ≤ T.graph ∧ T.graph ≤ B) ↔
          ((∀ i, T (d i) = s i) ∧ (∀ j, (q j).comp T = t j)) := by
…
  7. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.exists_smulRight_of_rank_one line 123

    Source documentation

    Every map with one-dimensional range is a nonzero functional times a nonzero vector. This existence statement is valid over any field.

    theorem exists_smulRight_of_rank_one (T : X →ₗ[K] Y)
    (hT : Module.finrank K T.range = 1) :
    ∃ (a : X →ₗ[K] K) (l : Y), a ≠ 0 ∧ l ≠ 0 ∧ T = a.smulRight l := by
…
  8. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.rank_one_iff_exists_smulRight line 148

    Source documentation

    The exact algebraic characterization of nonzero rank-one maps.

    theorem rank_one_iff_exists_smulRight (T : X →ₗ[K] Y) :
    Module.finrank K T.range = 1 ↔
      ∃ (a : X →ₗ[K] K) (l : Y), a ≠ 0 ∧ l ≠ 0 ∧ T = a.smulRight l := by
…
  9. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.binary_smulRight_unique line 166

    Source documentation

    Over the two-element field there is no nontrivial rescaling ambiguity.

    theorem binary_smulRight_unique
    {a b : X →ₗ[ZMod 2] ZMod 2} {l k : Y}
    (ha : a ≠ 0) (hl : l ≠ 0)
    (h : a.smulRight l = b.smulRight k) : a = b ∧ l = k := by
…
  10. abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryRankOneFactors line 187

    Source documentation

    Ordered nonzero factors, with functional coordinate first.

    abbrev BinaryRankOneFactors (X Y : Type*)
    [AddCommGroup X] [Module (ZMod 2) X]
    [AddCommGroup Y] [Module (ZMod 2) Y] :=
…
  11. abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryRankOneMaps line 193

    Source documentation

    The actual linear maps whose range has dimension one.

    abbrev BinaryRankOneMaps (X Y : Type*)
    [AddCommGroup X] [Module (ZMod 2) X]
    [AddCommGroup Y] [Module (ZMod 2) Y] :=
…
  12. def OAI.UniqueGamesTheorem.Inverse.MatrixChart.binaryRankOneMap line 198
  13. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.binary_smulRight_injective line 203
  14. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.binary_smulRight_surjective line 210
  15. def OAI.UniqueGamesTheorem.Inverse.MatrixChart.binaryRankOneEquiv line 218

    Source documentation

    Bijection justifying uniform rank-one sampling by independent uniform nonzero factors. The inverse uses choice only to select the proved unique pair.

    noncomputable def binaryRankOneEquiv :
    BinaryRankOneFactors X Y ≃ BinaryRankOneMaps X Y :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryRankOneFactors, OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryRankOneMaps

  16. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.binaryRankOneEquiv_apply line 223
  17. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_binaryRankOneMaps line 228

    Source documentation

    The number of binary rank-one maps is exactly the product of the two nonzero-factor counts, including the zero-dimensional edge cases.

    theorem card_binaryRankOneMaps [Fintype (X →ₗ[ZMod 2] ZMod 2)] [Fintype Y] :
    Nat.card (BinaryRankOneMaps X Y) =
      (Fintype.card (X →ₗ[ZMod 2] ZMod 2) - 1) * (Fintype.card Y - 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryRankOneMaps

  18. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_binaryRankOneMaps_pow line 240

    Source documentation

    Dimensional form of the exact rank-one count.

    theorem card_binaryRankOneMaps_pow [Fintype (X →ₗ[ZMod 2] ZMod 2)] [Fintype Y] :
    Nat.card (BinaryRankOneMaps X Y) =
      (2 ^ Module.finrank (ZMod 2) X - 1) *
        (2 ^ Module.finrank (ZMod 2) Y - 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryRankOneMaps

  19. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_binaryRankOneMaps_coordinates line 252
  20. abbrev OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.FixedFunctionalNeighborFiber line 284

    Source documentation

    Vectors external to the starting image which give the same updated image.

    abbrev FixedFunctionalNeighborFiber (X : E →ₗ[ZMod 2] F)
    (a : E →ₗ[ZMod 2] ZMod 2) (y₀ : F) :=
…
  21. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.add_image_not_mem_range line 289
  22. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.range_update_add_kernel line 295

    Source documentation

    Kernel translations of the perturbation vector preserve its image.

    theorem range_update_add_kernel (X : E →ₗ[ZMod 2] F)
    (a : E →ₗ[ZMod 2] ZMod 2) (y : F) (z : a.ker) :
    (X + a.smulRight (y + X z)).range = (X + a.smulRight y).range := by
…
  23. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fixedFunctionalFiberMap line 315

    Source documentation

    The affine parametrization of a fixed-functional image fiber.

    def fixedFunctionalFiberMap (X : E →ₗ[ZMod 2] F)
    (a : E →ₗ[ZMod 2] ZMod 2) {y₀ : F} (hy₀ : y₀ ∉ X.range) :
    a.ker → FixedFunctionalNeighborFiber X a y₀ :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.FixedFunctionalNeighborFiber

  24. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fixedFunctionalFiberMap_injective line 321
  25. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fixedFunctionalFiberMap_surjective line 330
  26. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fixedFunctionalNeighborFiberEquiv line 360

    Source documentation

    Exact constant-multiplicity fiber over an updated subspace.

    def fixedFunctionalNeighborFiberEquiv (X : E →ₗ[ZMod 2] F)
    (hX : Function.Injective X) (a : E →ₗ[ZMod 2] ZMod 2)
    (ha : a ≠ 0) {y₀ : F} (hy₀ : y₀ ∉ X.range) :
    a.ker ≃ FixedFunctionalNeighborFiber X a y₀ :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.FixedFunctionalNeighborFiber

  27. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.card_fixedFunctionalNeighborFiber line 368
  28. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.card_fixedFunctionalNeighborFiber_pow line 374
  29. abbrev OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.OutsideNeighborFactors line 407
  30. abbrev OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.OutsideNeighborPairFiber line 410
  31. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.functional_eq_of_update_range_eq line 416

    Source documentation

    The common-parent intersection recovers the binary functional uniquely.

    theorem functional_eq_of_update_range_eq (X : E →ₗ[ZMod 2] F)
    (hX : Function.Injective X) {a b : E →ₗ[ZMod 2] ZMod 2}
    {y z : F} (hy : y ∉ X.range) (hz : z ∉ X.range)
    (h : (rankOneUpdate X a y).range = (rankOneUpdate X b z).range) :
    a = b := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdate

  32. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fixedToPairFiber line 424
  33. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fixedToPairFiber_injective line 429
  34. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fixedToPairFiber_surjective line 436
  35. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fixedFunctionalEquivPairFiber line 453

    Source documentation

    Every pair in a fixed neighbor fiber has the same functional.

    def fixedFunctionalEquivPairFiber (X : E →ₗ[ZMod 2] F)
    (hX : Function.Injective X) (a : E →ₗ[ZMod 2] ZMod 2)
    (ha : a ≠ 0) {y₀ : F} (hy₀ : y₀ ∉ X.range) :
    FixedFunctionalNeighborFiber X a y₀ ≃ OutsideNeighborPairFiber X a y₀ :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.FixedFunctionalNeighborFiber, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.OutsideNeighborPairFiber

  36. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.outsideNeighborPairFiberEquiv line 462

    Source documentation

    The full rank-one neighbor-sampling fiber is the functional kernel.

    def outsideNeighborPairFiberEquiv (X : E →ₗ[ZMod 2] F)
    (hX : Function.Injective X) (a : E →ₗ[ZMod 2] ZMod 2)
    (ha : a ≠ 0) {y₀ : F} (hy₀ : y₀ ∉ X.range) :
    a.ker ≃ OutsideNeighborPairFiber X a y₀ :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.OutsideNeighborPairFiber

  37. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.card_outsideNeighborPairFiber line 469
  38. abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryChartNeighbors line 499

    Source documentation

    Coordinate matrices adjacent to a fixed graph matrix.

    abbrev BinaryChartNeighbors (T : X →ₗ[ZMod 2] Y) :=
…
  39. abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryGraphChartNeighbors line 505

    Source documentation

    The actual adjacent subspaces that lie in the graph chart.

    abbrev BinaryGraphChartNeighbors (T : X →ₗ[ZMod 2] Y) :=
…
  40. def OAI.UniqueGamesTheorem.Inverse.MatrixChart.rankOneEquivChartNeighbors line 514

    Source documentation

    Difference from a fixed matrix is an exact bijection between rank-one maps and adjacent matrices. Subtraction also makes this construction valid without invoking characteristic-two simplification.

    def rankOneEquivChartNeighbors (T : X →ₗ[ZMod 2] Y) :
    BinaryRankOneMaps X Y ≃ BinaryChartNeighbors T where
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryRankOneMaps, OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryChartNeighbors

  41. def OAI.UniqueGamesTheorem.Inverse.MatrixChart.graphChartNeighbor line 530
  42. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.graphChartNeighbor_injective line 535
  43. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.graphChartNeighbor_surjective line 542
  44. def OAI.UniqueGamesTheorem.Inverse.MatrixChart.chartNeighborsEquivGraphNeighbors line 553
  45. def OAI.UniqueGamesTheorem.Inverse.MatrixChart.binaryFactorsEquivGraphNeighbors line 560

    Source documentation

    The complete nonzero-factor sampling equivalence, ending in actual Grassmann subspaces in the chart.

    noncomputable def binaryFactorsEquivGraphNeighbors (T : X →ₗ[ZMod 2] Y) :
    BinaryRankOneFactors X Y ≃ BinaryGraphChartNeighbors T :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryRankOneFactors, OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryGraphChartNeighbors

  46. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.binaryFactorsEquivGraphNeighbors_apply line 565
  47. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.binaryFactorsEquivGraphNeighbors_apply_add line 572

    Source documentation

    In characteristic two the same parametrization is addition of the rank-one perturbation used in the matrix test.

    theorem binaryFactorsEquivGraphNeighbors_apply_add (T : X →ₗ[ZMod 2] Y)
    (p : BinaryRankOneFactors X Y) :
    (binaryFactorsEquivGraphNeighbors T p).val =
      (T + p.1.val.smulRight p.2.val).graph := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryRankOneFactors, OAI.UniqueGamesTheorem.Inverse.MatrixChart.binaryFactorsEquivGraphNeighbors

  48. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.graphChartNeighbor_finrank line 585

    Source documentation

    Every neighbor in the chart has the required Grassmann dimension.

    theorem graphChartNeighbor_finrank (T : X →ₗ[ZMod 2] Y)
    (L : BinaryGraphChartNeighbors T) :
    Module.finrank (ZMod 2) L.val = Module.finrank (ZMod 2) X := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryGraphChartNeighbors

  49. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.graphChartNeighbor_ne_self line 593

    Source documentation

    The dimension condition excludes the starting vertex itself.

    theorem graphChartNeighbor_ne_self (T : X →ₗ[ZMod 2] Y)
    (L : BinaryGraphChartNeighbors T) : L.val ≠ T.graph := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryGraphChartNeighbors

  50. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_binaryGraphChartNeighbors line 600
  51. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_binaryGraphChartNeighbors_coordinates line 609
  52. abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.CoordinateMatrix line 630
  53. def OAI.UniqueGamesTheorem.Inverse.MatrixChart.graphChartNeighborsEmbedding line 634

    Source documentation

    Inclusion into actual full neighbors preserves the subspace.

    def graphChartNeighborsEmbedding (T : CoordinateMatrix ell m) :
    BinaryGraphChartNeighbors T ↪ GrassmannNeighbors T.graph where
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.CoordinateMatrix, OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryGraphChartNeighbors, OAI.UniqueGamesTheorem.Inverse.MatrixChart.GrassmannNeighbors

  54. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_grassmann_neighbors_graph line 643
  55. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.full_degree_eq_twice_chart_degree line 654

    Source documentation

    Exactly twice as many full neighbors as chart neighbors. This natural number identity also covers a zero-dimensional side.

    theorem full_degree_eq_twice_chart_degree (T : CoordinateMatrix ell m) :
    Nat.card (GrassmannNeighbors T.graph) =
      2 * Nat.card (BinaryGraphChartNeighbors T) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.CoordinateMatrix, OAI.UniqueGamesTheorem.Inverse.MatrixChart.GrassmannNeighbors, OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryGraphChartNeighbors

  56. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.chart_degree_ratio line 666

    Source documentation

    The neighbor sampling probability of remaining in the chart is one half when both dimensions are positive.

    theorem chart_degree_ratio (T : CoordinateMatrix ell m)
    (hell : 0 < ell) (hm : 0 < m) :
    (Nat.card (BinaryGraphChartNeighbors T) : ℚ) /
      (Nat.card (GrassmannNeighbors T.graph) : ℚ) = 1 / 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.CoordinateMatrix, OAI.UniqueGamesTheorem.Inverse.MatrixChart.BinaryGraphChartNeighbors, OAI.UniqueGamesTheorem.Inverse.MatrixChart.GrassmannNeighbors

  57. def OAI.UniqueGamesTheorem.Inverse.MatrixChart.grassmannNeighborsMapEquiv line 694

    Source documentation

    Ambient linear equivalence transports the actual neighbor subspaces.

    noncomputable def grassmannNeighborsMapEquiv
    {E F : Type*} [AddCommGroup E] [Module (ZMod 2) E]
    [AddCommGroup F] [Module (ZMod 2) F]
    (e : E ≃ₗ[ZMod 2] F) (L : Submodule (ZMod 2) E) :
    GrassmannNeighbors L ≃ GrassmannNeighbors (L.map e.toLinearMap) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.GrassmannNeighbors

  58. def OAI.UniqueGamesTheorem.Inverse.MatrixChart.kmsNeighborsEquiv line 711

    Source documentation

    Extrinsic submodule neighbors and the finite KMS neighbor predicate agree.

    def kmsNeighborsEquiv {n ell : Nat} (L : KMS.Vertex n ell) :
    GrassmannNeighbors L.val ≃ {W : KMS.Vertex n ell // KMS.Adjacent L W} where
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.MatrixChart.GrassmannNeighbors, OAI.UniqueGamesTheorem.Inverse.KMS.Adjacent

  59. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_full_neighbors line 726
  60. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_full_neighbors_twice line 742

    Source documentation

    Exactly two full Grassmann neighbors for every nonzero factor pair.

    theorem card_full_neighbors_twice {ell m : Nat} (M : Matrix (Fin ell) (Fin m) (ZMod 2)) :
    (KMS.neighbors (matrixVertex M)).card =
      2 * ((2 ^ ell - 1) * (2 ^ m - 1)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.neighbors, OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrixVertex

  61. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.dotFunctional_surjective line 769
  62. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.exists_matrix_interval_slice line 780
  63. theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.exists_bounded_matrix_interval_slice line 801

    Source documentation

    An interval order bound yields separate row and column budgets.

    theorem exists_bounded_matrix_interval_slice
    (A B : Submodule K ((ι → K) × (κ → K))) (r : Nat)
    (horder : Module.finrank K A +
      Module.finrank K (((ι → K) × (κ → K)) ⧸ B) ≤ r) :
    ∃ (n_r n_c : Nat) (d : Fin n_r → ι → K) (s : Fin n_r → κ → K)
      (t : Fin n_c → ι → K) (q : Fin n_c → κ → K),
      n_r ≤ r ∧ n_c ≤ r ∧
      ∀ M : Matrix ι κ K,
        (A ≤ matrixGraph M ∧ matrixGraph M ≤ B) ↔
          ((∀ i, d i ᵥ* M = s i) ∧ (∀ j, M *ᵥ q j = t j)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.matrixGraph