OAI/Computability/UniqueGames/Inverse/KMSBasisComparisonLemmas.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

The ordered-basis lift of a Grassmann set

The ambient sample space contains every linear map, including singular maps. The lift accepts exactly maps whose range is one of the specified ell-dimensional subspaces. Thus dependence is rejected, rather than silently conditioning the ambient uniform distribution on independence.

  1. abbrev OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap line 30
  2. instance OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.basisMapFinite line 32
  3. instance OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.basisMapFintype line 36
  4. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.InLift line 39

    Source documentation

    Membership in the lift, expressed by the actual linear-map range.

    def InLift {n ell : ℕ} (S : Finset (KMS.Vertex n ell)) (X : BasisMap n ell) : Prop :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap

  5. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.lift line 43

    Source documentation

    The lifted finite set in the whole map space.

    def lift {n ell : ℕ} (S : Finset (KMS.Vertex n ell)) : Finset (BasisMap n ell) :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap

  6. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.mem_lift line 46
  7. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftedIndicator line 51

    Source documentation

    Real Boolean indicator, in the orientation used by the matrix Fourier transform.

    def liftedIndicator {n ell : ℕ} (S : Finset (KMS.Vertex n ell))
    (X : BasisMap n ell) : ℝ := if InLift S X then 1 else 0

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.InLift

  8. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftedIndicator_nonneg line 54
  9. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftedIndicator_le_one line 59
  10. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injective_of_inLift line 65

    Source documentation

    A map accepted by the lift has full column rank.

    theorem injective_of_inLift {n ell : ℕ} {S : Finset (KMS.Vertex n ell)}
    {X : BasisMap n ell} (h : InLift S X) : Function.Injective X := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.InLift

  11. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rangeVertex line 78

    Source documentation

    The actual Grassmann vertex represented by an injective map.

    def rangeVertex {n ell : ℕ} (X : BasisMap n ell) (hX : Function.Injective X) :
    KMS.Vertex n ell :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMS.Vertex

  12. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.inLift_iff_rangeVertex_mem line 84
  13. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.inLift_comp_iff line 95

    Source documentation

    A change of the ordered domain basis leaves the range unchanged.

    theorem inLift_comp_iff {n ell : ℕ} (S : Finset (KMS.Vertex n ell))
    (g : KMS.Ambient ell ≃ₗ[KMS.F2] KMS.Ambient ell) (X : BasisMap n ell) :
    InLift S (X.comp g.toLinearMap) ↔ InLift S X := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMS.Ambient, OAI.UniqueGamesTheorem.Inverse.KMS.F2, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.InLift

  14. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftedIndicator_basisInvariant line 102

    Source documentation

    The lift is basis-invariant in precisely the Fourier theorem's sense.

    theorem liftedIndicator_basisInvariant {n ell : ℕ} (S : Finset (KMS.Vertex n ell)) :
    KMSBasisInvariant.IsBasisInvariant (liftedIndicator S) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftedIndicator

  15. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fiberProductEquiv line 134

    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 :=
…
  16. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fiberProductEquiv_fst line 137
  17. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.expect_eq_of_uniform_fibers line 144

    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
…
  18. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.density_eq_of_uniform_fibers line 158

    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
…
  19. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.RangeFiber line 175

    Source documentation

    The actual fiber of injective maps over a specified range subspace.

    def RangeFiber (L : Submodule K F) :=
…
  20. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rangeFiberEquiv line 179

    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.UniqueGamesTheorem.Inverse.KMSBasisComparison.RangeFiber

  21. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rangeFiberEquivAut line 207

    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.UniqueGamesTheorem.Inverse.KMSBasisComparison.RangeFiber

  22. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rangeFiber_card line 216

    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.UniqueGamesTheorem.Inverse.KMSBasisComparison.RangeFiber

  23. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.vertexBasis line 223

    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.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMS.Ambient, OAI.UniqueGamesTheorem.Inverse.KMS.F2

  24. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.vertex_rangeFiber_card line 229

    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.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.RangeFiber, OAI.UniqueGamesTheorem.Inverse.KMS.Ambient

  25. abbrev OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.InjectiveBasisMap line 235

    Source documentation

    The sample space after explicitly conditioning on full column rank.

    abbrev InjectiveBasisMap (n ell : ℕ) :=
…
  26. instance OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injectiveBasisMapFintype line 238
  27. instance OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.basisAutomorphismFinite line 241
  28. instance OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.basisAutomorphismFintype line 247
  29. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injectiveRange line 250
  30. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injectiveRangeFiberEquiv line 255

    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.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.InjectiveBasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injectiveRange, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.RangeFiber, OAI.UniqueGamesTheorem.Inverse.KMS.Ambient

  31. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injectiveRangeFiberAut line 263
  32. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injectiveRange_expect line 270

    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.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.InjectiveBasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injectiveRange

  33. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injectiveRange_density line 278

    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.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.InjectiveBasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injectiveRange

  34. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.lift_nonempty_iff line 286
  35. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRange line 298

    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.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.lift

  36. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRangeFiberEquiv line 303
  37. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRangeFiberAut line 313
  38. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.lift_card line 320

    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.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.lift, OAI.UniqueGamesTheorem.Inverse.KMS.Ambient, OAI.UniqueGamesTheorem.Inverse.KMS.F2

  39. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.injectiveBasisMap_card line 326
  40. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.lift_density_factor line 336

    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.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.lift, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.InjectiveBasisMap

  41. abbrev OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.Functional line 367
  42. instance OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.functionalFinite line 369
  43. instance OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.functionalFintype line 373
  44. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.card_functional line 375
  45. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.card_ambient line 382
  46. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.goodParameters line 386

    Source documentation

    Actual good pairs in the unconditioned product sample space.

    def goodParameters {n ell : ℕ} (X : BasisMap n ell) :
    Finset (Functional ell × KMS.Ambient n) :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.Functional, OAI.UniqueGamesTheorem.Inverse.KMS.Ambient

  47. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.mem_goodParameters line 391
  48. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.card_range line 396
  49. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.card_goodParameters line 402

    Source documentation

    The exact good-event count, including the zero-dimensional boundary.

    theorem card_goodParameters {n ell : ℕ} (X : BasisMap n ell)
    (hX : Function.Injective X) :
    (goodParameters X).card = (2 ^ ell - 1) * (2 ^ n - 2 ^ ell) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.goodParameters

  50. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.badParameters_mass_le line 417

    Source documentation

    Exceptional mass is bounded by the sum of the two factor exceptions.

    theorem badParameters_mass_le {n ell : ℕ} (X : BasisMap n ell)
    (hX : Function.Injective X) :
    1 - ((goodParameters X).card : ℝ) /
        Fintype.card (Functional ell × KMS.Ambient n) ≤
      ((2 : ℝ) ^ ell)⁻¹ + (2 : ℝ) ^ ell / (2 : ℝ) ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.goodParameters, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.Functional, OAI.UniqueGamesTheorem.Inverse.KMS.Ambient

  51. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.badParameters_mass_le_compl line 435

    Source documentation

    The same estimate in the complement-cardinality form used for deleting the bad event from a finite expectation.

    theorem badParameters_mass_le_compl {n ell : ℕ} (X : BasisMap n ell)
    (hX : Function.Injective X) :
    (((Finset.univ \ goodParameters X).card : ℕ) : ℝ) /
        Fintype.card (Functional ell × KMS.Ambient n) ≤
      ((2 : ℝ) ^ ell)⁻¹ + (2 : ℝ) ^ ell / (2 : ℝ) ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.goodParameters, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.Functional, OAI.UniqueGamesTheorem.Inverse.KMS.Ambient

  52. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.outsideNeighborSample line 465

    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.UniqueGamesTheorem.Inverse.KMSBasisComparison.OutsideNeighborFactors, OAI.UniqueGamesTheorem.Inverse.MatrixChart.GrassmannNeighbors

  53. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.outsideNeighborSample_val line 470
  54. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.card_outsideNeighborSample_fiber line 477

    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.UniqueGamesTheorem.Inverse.MatrixChart.GrassmannNeighbors, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.OutsideNeighborFactors, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.outsideNeighborSample

  55. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.expect_outsideNeighborSample line 495

    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.UniqueGamesTheorem.Inverse.MatrixChart.GrassmannNeighbors, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.OutsideNeighborFactors, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.outsideNeighborSample