KMSBasisComparisonNeighborsFiberFunctional.lean`

77 declarations, 0 contain sorry, 0 declared as axioms

Binary linear functionals are determined by their kernels. The statement includes the zero functional; no choice of a nonzero normalization is needed. Injective linear images retain the same uniqueness property.

theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.binary_functional_eq_of_ker_eq line 19
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.MaxCutGames.Inverse.KMSBasisComparison.binary_functional_eq_of_map_ker_eq line 35
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
…
```
abbrev OAI.MaxCutGames.Inverse.KMSBasisComparison.OutsideNeighborFactors line 56
abbrev OAI.MaxCutGames.Inverse.KMSBasisComparison.OutsideNeighborPairFiber line 59

theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.functional_eq_of_update_range_eq line 65

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.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdate

def OAI.MaxCutGames.Inverse.KMSBasisComparison.fixedToPairFiber line 73
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.fixedToPairFiber_injective line 78
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.fixedToPairFiber_surjective line 85
def OAI.MaxCutGames.Inverse.KMSBasisComparison.fixedFunctionalEquivPairFiber line 102
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.MaxCutGames.Inverse.KMSBasisComparison.FixedFunctionalNeighborFiber, OAI.MaxCutGames.Inverse.KMSBasisComparison.OutsideNeighborPairFiber
def OAI.MaxCutGames.Inverse.KMSBasisComparison.outsideNeighborPairFiberEquiv line 111
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.MaxCutGames.Inverse.KMSBasisComparison.OutsideNeighborPairFiber
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.card_outsideNeighborPairFiber line 118
def OAI.MaxCutGames.Inverse.KMSBasisComparison.fiberProductEquiv line 147
Source documentation
Trivializing equal-size fibers identifies the full sample space with a product; the first coordinate remains the original quotient map.
```
def fiberProductEquiv (f : X → Y) (e : ∀ y, {x : X // f x = y} ≃ G) : X ≃ Y × G :=
…
```
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.fiberProductEquiv_fst line 150
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.expect_eq_of_uniform_fibers line 157
Source documentation
Uniform sampling pushes forward to uniform sampling whenever every fiber is equivalent to the same nonempty finite type. This applies to real and rational expectations alike.
```
theorem expect_eq_of_uniform_fibers [Fintype X] [Fintype Y] [Fintype G]
    [Nonempty G] {M : Type*} [AddCommMonoid M] [Module ℚ≥0 M]
    (f : X → Y) (e : ∀ y, {x : X // f x = y} ≃ G) (g : Y → M) :
    (𝔼 x, g (f x)) = 𝔼 y, g y := by
…
```

theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.density_eq_of_uniform_fibers line 171

Source documentation

Exact rational finite-set density transfer; no asymptotic or probability normalization is hidden in the fiber comparison.

theorem density_eq_of_uniform_fibers [Fintype X] [Fintype Y] [Fintype G]
    [Nonempty G] (f : X → Y) (e : ∀ y, {x : X // f x = y} ≃ G)
    (S : Finset Y) :
    (((Finset.univ.filter fun x => f x ∈ S).card : ℚ) / Fintype.card X) =
      (S.card : ℚ) / Fintype.card Y := by
…

def OAI.MaxCutGames.Inverse.KMSBasisComparison.RangeFiber line 188
Source documentation
The actual fiber of injective maps over a specified range subspace.
```
def RangeFiber (L : Submodule K F) :=
…
```
def OAI.MaxCutGames.Inverse.KMSBasisComparison.rangeFiberEquiv line 192
Source documentation
A range fiber is the set of linear equivalences onto that range.
```
def rangeFiberEquiv (L : Submodule K F) : RangeFiber (E := E) L ≃ (E ≃ₗ[K] L) where
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparison.RangeFiber
def OAI.MaxCutGames.Inverse.KMSBasisComparison.rangeFiberEquivAut line 220
Source documentation
After choosing one basis of a subspace, its ordered-basis fiber is exactly the domain's automorphism group.
```
def rangeFiberEquivAut {L : Submodule K F} (e : E ≃ₗ[K] L) :
    RangeFiber (E := E) L ≃ (E ≃ₗ[K] E) :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparison.RangeFiber
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.rangeFiber_card line 229
Source documentation
The size of a range fiber is independent of the selected subspace.
```
theorem rangeFiber_card {L : Submodule K F} (e : E ≃ₗ[K] L) :
    Nat.card (RangeFiber (E := E) L) = Nat.card (E ≃ₗ[K] E) :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparison.RangeFiber
def OAI.MaxCutGames.Inverse.KMSBasisComparison.vertexBasis line 236
Source documentation
Every Grassmann vertex admits an ordered basis of the prescribed domain.
```
def vertexBasis {n ell : ℕ} (L : KMS.Vertex n ell) :
    KMS.Ambient ell ≃ₗ[KMS.F2] L.val :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMS.Ambient, OAI.MaxCutGames.Inverse.KMS.F2
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.vertex_rangeFiber_card line 242
Source documentation
The concrete binary Grassmann range fiber has exactly as many elements as the automorphism group of the fixed ell-dimensional domain.
```
theorem vertex_rangeFiber_card {n ell : ℕ} (L : KMS.Vertex n ell) :
    Nat.card (RangeFiber (E := KMS.Ambient ell) L.val) =
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.RangeFiber, OAI.MaxCutGames.Inverse.KMS.Ambient
abbrev OAI.MaxCutGames.Inverse.KMSBasisComparison.InjectiveBasisMap line 248
Source documentation
The sample space after explicitly conditioning on full column rank.
```
abbrev InjectiveBasisMap (n ell : ℕ) :=
…
```
instance OAI.MaxCutGames.Inverse.KMSBasisComparison.injectiveBasisMapFintype line 251
instance OAI.MaxCutGames.Inverse.KMSBasisComparison.basisAutomorphismFinite line 254
instance OAI.MaxCutGames.Inverse.KMSBasisComparison.basisAutomorphismFintype line 260
def OAI.MaxCutGames.Inverse.KMSBasisComparison.injectiveRange line 263
def OAI.MaxCutGames.Inverse.KMSBasisComparison.injectiveRangeFiberEquiv line 268
Source documentation
The fiber of the actual range-vertex map is the injective range fiber defined above. Both injectivity and the subspace equality are preserved.
```
def injectiveRangeFiberEquiv {n ell : ℕ} (L : KMS.Vertex n ell) :
    {X : InjectiveBasisMap n ell // injectiveRange X = L} ≃
      RangeFiber (E := KMS.Ambient ell) L.val where
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.InjectiveBasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.injectiveRange, OAI.MaxCutGames.Inverse.KMSBasisComparison.RangeFiber, OAI.MaxCutGames.Inverse.KMS.Ambient
def OAI.MaxCutGames.Inverse.KMSBasisComparison.injectiveRangeFiberAut line 276
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.injectiveRange_expect line 283
Source documentation
Exact uniform pushforward from injective binary maps to Grassmann vertices. The statement holds also at an empty Grassmannian.
```
theorem injectiveRange_expect {n ell : ℕ} {M : Type*}
    [AddCommMonoid M] [Module ℚ≥0 M] (g : KMS.Vertex n ell → M) :
    (𝔼 X : InjectiveBasisMap n ell, g (injectiveRange X)) = 𝔼 L, g L := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.InjectiveBasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.injectiveRange
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.injectiveRange_density line 291
Source documentation
Rational density transfer with the injective-map denominator made explicit.
```
theorem injectiveRange_density {n ell : ℕ} (S : Finset (KMS.Vertex n ell)) :
    (((Finset.univ.filter fun X : InjectiveBasisMap n ell => injectiveRange X ∈ S).card : ℚ) /
      Fintype.card (InjectiveBasisMap n ell)) =
      (S.card : ℚ) / Fintype.card (KMS.Vertex n ell) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.InjectiveBasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.injectiveRange
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.lift_nonempty_iff line 299
def OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRange line 311
Source documentation
The range quotient restricted to the lifted event itself.
```
def liftRange {n ell : ℕ} (S : Finset (KMS.Vertex n ell))
    (X : lift S) : S :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.lift
def OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRangeFiberEquiv line 316
def OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRangeFiberAut line 326
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.lift_card line 333
Source documentation
Every selected Grassmann vertex contributes exactly the same number of ordered bases to the full matrix-space lift.
```
theorem lift_card {n ell : ℕ} (S : Finset (KMS.Vertex n ell)) :
    (lift S).card = S.card *
      Fintype.card (KMS.Ambient ell ≃ₗ[KMS.F2] KMS.Ambient ell) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.lift, OAI.MaxCutGames.Inverse.KMS.Ambient, OAI.MaxCutGames.Inverse.KMS.F2
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.injectiveBasisMap_card line 339
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.lift_density_factor line 349
Source documentation
The density within all maps is the Grassmann density times the full-rank probability. In particular the full-rank factor must not be dropped when the lift is used as a function on the ambient Fourier space.
```
theorem lift_density_factor {n ell : ℕ} (S : Finset (KMS.Vertex n ell))
    (hS : S.Nonempty) :
    ((lift S).card : ℚ) / Fintype.card (BasisMap n ell) =
      ((Fintype.card (InjectiveBasisMap n ell) : ℚ) / Fintype.card (BasisMap n ell)) *
        ((S.card : ℚ) / Fintype.card (KMS.Vertex n ell)) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.lift, OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.InjectiveBasisMap
def OAI.MaxCutGames.Inverse.KMSBasisComparison.outsideNeighborSample line 375
Source documentation
The full-neighbor sampler on its exact good-event factor space.
```
def outsideNeighborSample (X : E →ₗ[ZMod 2] F) (hX : Function.Injective X)
    (p : OutsideNeighborFactors X) : MatrixChart.GrassmannNeighbors X.range :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparison.OutsideNeighborFactors, OAI.MaxCutGames.Inverse.MatrixChart.GrassmannNeighbors
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.outsideNeighborSample_val line 380
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.card_outsideNeighborSample_fiber line 387
Source documentation
Every full Grassmann neighbor has exactly the same number of original factor pairs. The number is the size of one codimension-one kernel.
```
theorem card_outsideNeighborSample_fiber [Fintype E]
    (X : E →ₗ[ZMod 2] F) (hX : Function.Injective X)
    (W : MatrixChart.GrassmannNeighbors X.range) :
    Nat.card {p : OutsideNeighborFactors X // outsideNeighborSample X hX p = W} =
      2 ^ (Module.finrank (ZMod 2) E - 1) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.MatrixChart.GrassmannNeighbors, OAI.MaxCutGames.Inverse.KMSBasisComparison.OutsideNeighborFactors, OAI.MaxCutGames.Inverse.KMSBasisComparison.outsideNeighborSample
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.expect_outsideNeighborSample line 405
Source documentation
Uniform neighbor law for any real observable. There is no chart restriction, hidden conditioning, or additional loss in this identity.
```
theorem expect_outsideNeighborSample [Fintype E] [Fintype F]
    [Fintype (E →ₗ[ZMod 2] ZMod 2)]
    (X : E →ₗ[ZMod 2] F) (hX : Function.Injective X)
    [Fintype (MatrixChart.GrassmannNeighbors X.range)]
    (g : MatrixChart.GrassmannNeighbors X.range → ℝ) :
    (𝔼 p : OutsideNeighborFactors X, g (outsideNeighborSample X hX p)) =
      𝔼 W : MatrixChart.GrassmannNeighbors X.range, g W := by
…
```
Mentions: OAI.MaxCutGames.Inverse.MatrixChart.GrassmannNeighbors, OAI.MaxCutGames.Inverse.KMSBasisComparison.OutsideNeighborFactors, OAI.MaxCutGames.Inverse.KMSBasisComparison.outsideNeighborSample
abbrev OAI.MaxCutGames.Inverse.MatrixChart.BinaryChartNeighbors line 436
Source documentation
Coordinate matrices adjacent to a fixed graph matrix.
```
abbrev BinaryChartNeighbors (T : X →ₗ[ZMod 2] Y) :=
…
```
abbrev OAI.MaxCutGames.Inverse.MatrixChart.BinaryGraphChartNeighbors line 442
Source documentation
The actual adjacent subspaces that lie in the graph chart.
```
abbrev BinaryGraphChartNeighbors (T : X →ₗ[ZMod 2] Y) :=
…
```
def OAI.MaxCutGames.Inverse.MatrixChart.rankOneEquivChartNeighbors line 451
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.MaxCutGames.Inverse.MatrixChart.BinaryRankOneMaps, OAI.MaxCutGames.Inverse.MatrixChart.BinaryChartNeighbors
def OAI.MaxCutGames.Inverse.MatrixChart.graphChartNeighbor line 468
theorem OAI.MaxCutGames.Inverse.MatrixChart.graphChartNeighbor_injective line 473
theorem OAI.MaxCutGames.Inverse.MatrixChart.graphChartNeighbor_surjective line 480
def OAI.MaxCutGames.Inverse.MatrixChart.chartNeighborsEquivGraphNeighbors line 491
def OAI.MaxCutGames.Inverse.MatrixChart.binaryFactorsEquivGraphNeighbors line 498
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.MaxCutGames.Inverse.MatrixChart.BinaryRankOneFactors, OAI.MaxCutGames.Inverse.MatrixChart.BinaryGraphChartNeighbors
theorem OAI.MaxCutGames.Inverse.MatrixChart.binaryFactorsEquivGraphNeighbors_apply line 503
theorem OAI.MaxCutGames.Inverse.MatrixChart.binaryFactorsEquivGraphNeighbors_apply_add line 510
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.MaxCutGames.Inverse.MatrixChart.BinaryRankOneFactors, OAI.MaxCutGames.Inverse.MatrixChart.binaryFactorsEquivGraphNeighbors
theorem OAI.MaxCutGames.Inverse.MatrixChart.graphChartNeighbor_finrank line 523
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.MaxCutGames.Inverse.MatrixChart.BinaryGraphChartNeighbors
theorem OAI.MaxCutGames.Inverse.MatrixChart.graphChartNeighbor_ne_self line 531
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.MaxCutGames.Inverse.MatrixChart.BinaryGraphChartNeighbors
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_binaryGraphChartNeighbors line 538
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_binaryGraphChartNeighbors_coordinates line 547
abbrev OAI.MaxCutGames.Inverse.MatrixChart.CoordinateMatrix line 564
def OAI.MaxCutGames.Inverse.MatrixChart.graphChartNeighborsEmbedding line 568
Source documentation
Inclusion into actual full neighbors preserves the subspace.
```
def graphChartNeighborsEmbedding (T : CoordinateMatrix ell m) :
    BinaryGraphChartNeighbors T ↪ GrassmannNeighbors T.graph where
…
```
Mentions: OAI.MaxCutGames.Inverse.MatrixChart.CoordinateMatrix, OAI.MaxCutGames.Inverse.MatrixChart.BinaryGraphChartNeighbors, OAI.MaxCutGames.Inverse.MatrixChart.GrassmannNeighbors
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_grassmann_neighbors_graph line 577
theorem OAI.MaxCutGames.Inverse.MatrixChart.full_degree_eq_twice_chart_degree line 588
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.MaxCutGames.Inverse.MatrixChart.CoordinateMatrix, OAI.MaxCutGames.Inverse.MatrixChart.GrassmannNeighbors, OAI.MaxCutGames.Inverse.MatrixChart.BinaryGraphChartNeighbors
theorem OAI.MaxCutGames.Inverse.MatrixChart.chart_degree_ratio line 600
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.MaxCutGames.Inverse.MatrixChart.CoordinateMatrix, OAI.MaxCutGames.Inverse.MatrixChart.BinaryGraphChartNeighbors, OAI.MaxCutGames.Inverse.MatrixChart.GrassmannNeighbors
abbrev OAI.MaxCutGames.Inverse.MatrixChart.matrixGraph line 628
theorem OAI.MaxCutGames.Inverse.MatrixChart.mem_matrixGraph line 632
theorem OAI.MaxCutGames.Inverse.MatrixChart.matrixGraph_injective line 638
abbrev OAI.MaxCutGames.Inverse.MatrixChart.dotFunctional line 645
Source documentation
A coordinate vector as a linear functional, for the standard dot pairing.
```
abbrev dotFunctional (x : ι → K) : (ι → K) →ₗ[K] K := dotProductBilin K K x
```
theorem OAI.MaxCutGames.Inverse.MatrixChart.dotFunctional_injective line 647
theorem OAI.MaxCutGames.Inverse.MatrixChart.dotFunctional_comp_vecMulLinear line 654
Source documentation
Transposing the chart map sends a column specification to its dot functional.
```
theorem dotFunctional_comp_vecMulLinear (M : Matrix ι κ K) (q : κ → K) :
    (dotFunctional q).comp M.vecMulLinear = dotFunctional (M *ᵥ q) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.MatrixChart.dotFunctional
theorem OAI.MaxCutGames.Inverse.MatrixChart.column_equation_iff line 661

theorem OAI.MaxCutGames.Inverse.MatrixChart.matrix_interval_iff_slice line 667

Source documentation

Exact concrete row-and-column slice corresponding to an interval.

theorem matrix_interval_iff_slice {ρ σ : Type*}
    (d : ρ → ι → K) (s : ρ → κ → K)
    (t : σ → ι → K) (q : σ → κ → K) (M : Matrix ι κ K) :
    lowerRows d s ≤ matrixGraph M ∧
        matrixGraph M ≤ upperColumns (fun j => dotFunctional (t j))
          (fun j => dotFunctional (q j)) ↔
      (∀ i, d i ᵥ* M = s i) ∧ (∀ j, M *ᵥ q j = t j) := by
…

Mentions: OAI.MaxCutGames.Inverse.MatrixChart.lowerRows, OAI.MaxCutGames.Inverse.MatrixChart.matrixGraph, OAI.MaxCutGames.Inverse.MatrixChart.upperColumns, OAI.MaxCutGames.Inverse.MatrixChart.dotFunctional

theorem OAI.MaxCutGames.Inverse.MatrixChart.finrank_matrixGraph line 679
Source documentation
The graph always has the row dimension, including degenerate zero dimensions.
```
theorem finrank_matrixGraph (M : Matrix ι κ K) :
    Module.finrank K (matrixGraph M) = Fintype.card ι := by
…
```
Mentions: OAI.MaxCutGames.Inverse.MatrixChart.matrixGraph
def OAI.MaxCutGames.Inverse.MatrixChart.coordinateJoin line 695
Source documentation
Concatenate the two coordinate blocks of the chart ambient space.
```
def coordinateJoin (K : Type*) [Field K] (ell m : Nat) :
    ((Fin ell → K) × (Fin m → K)) ≃ₗ[K] (Fin (ell + m) → K) :=
…
```
def OAI.MaxCutGames.Inverse.MatrixChart.matrixVertex line 701
Source documentation
A matrix as an actual Grassmann vertex on ell + m binary coordinates.
```
def matrixVertex {ell m : Nat} (M : Matrix (Fin ell) (Fin m) (ZMod 2)) :
    KMS.Vertex (ell + m) ell :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex
theorem OAI.MaxCutGames.Inverse.MatrixChart.matrixVertex_injective line 706
theorem OAI.MaxCutGames.Inverse.MatrixChart.finrank_matrixVertex_intersection line 713
theorem OAI.MaxCutGames.Inverse.MatrixChart.adjacent_matrixVertex_iff line 728
Source documentation
Exact correspondence with the KMS adjacency predicate, including its explicit inequality requirement.
```
theorem adjacent_matrixVertex_iff {ell m : Nat}
    (M N : Matrix (Fin ell) (Fin m) (ZMod 2)) :
    KMS.Adjacent (matrixVertex M) (matrixVertex N) ↔
      Module.finrank (ZMod 2) (LinearMap.range (M.vecMulLinear - N.vecMulLinear)) = 1 := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Adjacent, OAI.MaxCutGames.Inverse.MatrixChart.matrixVertex
def OAI.MaxCutGames.Inverse.MatrixChart.matrixChart line 754
Source documentation
The finite matrix chart in the Grassmann vertex type.
```
def matrixChart (ell m : Nat) : Finset (KMS.Vertex (ell + m) ell) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex
theorem OAI.MaxCutGames.Inverse.MatrixChart.mem_matrixChart line 758
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_matrixChart line 764