OAI/Computability/MaxCut/Games/KMSBasisComparisonPseudorandomTupleMap.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

The restricted tuple law is the actual linear-map lift law in coordinates, with all singular tuples still present in the uniform denominator.

  1. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.tupleBasis line 17
  2. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.tupleMapEquiv line 20
  3. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.tupleMap line 23
  4. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.tupleMap_range line 26
  5. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.tupleMap_basis line 30
  6. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.tupleMap_injective_iff line 34
  7. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.inLift_tupleMap_iff line 44
  8. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity_eq_expect line 61

    Source documentation

    The tuple density equals the normalized expectation of the actual lift's indicator on the prescribed basis-coordinate restriction.

    theorem restrictedLiftDensity_eq_expect (S : Finset (Vertex n (q + t)))
    (Q : Fin q ā†’ Ambient n) (W : Submodule F2 (Ambient n)) :
    restrictedLiftDensity S Q W =
      š”¼ z : Fin t ā†’ W, liftedIndicator S (tupleMap (joinedTuple Q W z)) := by
ā€¦

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity, OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.tupleMap, OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.joinedTuple

  9. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.grassmann_pseudorandom_lift_expect line 72

    Source documentation

    KMS Lemma 2.8 in the actual linear-map coordinates, with the stronger Īµ bound supplied by exact equal-size completion fibers.

    theorem grassmann_pseudorandom_lift_expect {r : ā„•} {Īµ : ā„}
    (S : Finset (Vertex n (q + t))) (hS : GrassmannPseudorandom S r Īµ)
    (hĪµ : 0 ā‰¤ Īµ) (Q : Fin q ā†’ Ambient n) (W : Submodule F2 (Ambient n))
    (hbudget : q + (n - Module.finrank F2 W) ā‰¤ r) :
    (š”¼ z : Fin t ā†’ W, liftedIndicator S (tupleMap (joinedTuple Q W z))) ā‰¤ Īµ := by
ā€¦

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.GrassmannPseudorandom, OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.tupleMap, OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.joinedTuple

  10. theorem OAI.MaxCutGames.Inverse.KMSAffineRestriction.lifted_expect_in_basis line 98

    Source documentation

    The independent tuple law has the same bound in every basis of the domain. The indicator depends only on the actual range of the constructed map.

    theorem lifted_expect_in_basis (S : Finset (Vertex n ell))
    (hS : GrassmannPseudorandom S r Īµ) (hĪµ : 0 ā‰¤ Īµ)
    (b : Module.Basis (Fin q āŠ• Fin t) F2 (Ambient ell))
    (Q : Fin q ā†’ Ambient n) (W : Submodule F2 (Ambient n))
    (hbudget : q + (n - Module.finrank F2 W) ā‰¤ r) :
    (š”¼ z : Fin t ā†’ W, liftedIndicator S (b.constr F2 (joinedTuple Q W z))) ā‰¤ Īµ := by
ā€¦
  11. def OAI.MaxCutGames.Inverse.KMSAffineRestriction.affineCoordinates line 116

    Source documentation

    Coordinates of a uniform linear map, translated by a fixed linear map, are still exactly uniform. This also covers zero-dimensional free domains.

    def affineCoordinates {E W : Type*}
    [AddCommGroup E] [Module F2 E] [AddCommGroup W] [Module F2 W]
    (b : Module.Basis (Fin t) F2 E) (T : E ā†’ā‚—[F2] W) :
    (E ā†’ā‚—[F2] W) ā‰ƒ (Fin t ā†’ W) :=
ā€¦
  12. theorem OAI.MaxCutGames.Inverse.KMSAffineRestriction.affineCoordinates_apply line 122
  13. theorem OAI.MaxCutGames.Inverse.KMSAffineRestriction.lifted_expect_shifted_basis line 128

    Source documentation

    Actual uniform affine free-coordinate noise satisfies the tuple bound.

    theorem lifted_expect_shifted_basis {E0 : Type*}
    [AddCommGroup E0] [Module F2 E0]
    (S : Finset (Vertex n ell)) (hS : GrassmannPseudorandom S r Īµ) (hĪµ : 0 ā‰¤ Īµ)
    (b : Module.Basis (Fin q āŠ• Fin t) F2 (Ambient ell))
    (Q : Fin q ā†’ Ambient n) (W : Submodule F2 (Ambient n))
    [Fintype (E0 ā†’ā‚—[F2] W)]
    (b0 : Module.Basis (Fin t) F2 E0) (T0 : E0 ā†’ā‚—[F2] W)
    (hbudget : q + (n - Module.finrank F2 W) ā‰¤ r) :
    (š”¼ H : E0 ā†’ā‚—[F2] W, liftedIndicator S
      (b.constr F2 (joinedTuple Q W (fun i => T0 (b0 i) + H (b0 i))))) ā‰¤ Īµ := by
ā€¦
  14. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionComplement.exists_bounded_complement_of_linearMap line 165

    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
ā€¦
  15. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionComplement.exists_bounded_complement line 186

    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
ā€¦
  16. abbrev OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.localVanishing line 218

    Source documentation

    The original vanishing subspace viewed inside the chosen large summand.

    abbrev localVanishing (D U : Submodule F2 E) : Submodule F2 U :=
ā€¦
  17. def OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.splitLeft line 222

    Source documentation

    The constrained component of an actual quotient parameter.

    def splitLeft (D U : Submodule F2 E) (W : Submodule F2 F)
    (A : Parameter D W) : Parameter (localVanishing D U) W :=
ā€¦

    Mentions: OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.localVanishing

  18. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.splitLeft_apply line 231
  19. def OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.splitRight line 237

    Source documentation

    The free component of an actual quotient parameter.

    def splitRight (D Eā‚€ : Submodule F2 E) (W : Submodule F2 F)
    (A : Parameter D W) : Eā‚€ ā†’ā‚—[F2] W :=
ā€¦
  20. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.splitRight_apply line 241
  21. def OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.joinMap line 246

    Source documentation

    Assemble the two components before quotienting by D.

    def joinMap (D U Eā‚€ : Submodule F2 E) (W : Submodule F2 F)
    (hc : IsCompl U Eā‚€) (B : Parameter (localVanishing D U) W)
    (C : Eā‚€ ā†’ā‚—[F2] W) : E ā†’ā‚—[F2] W :=
ā€¦

    Mentions: OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.localVanishing

  22. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.joinMap_apply_left line 252
  23. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.joinMap_apply_right line 258
  24. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.joinMap_vanishes line 264
  25. def OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.join line 277

    Source documentation

    The actual quotient parameter reconstructed from both independent pieces.

    def join (D U Eā‚€ : Submodule F2 E) (W : Submodule F2 F)
    (hDU : D ā‰¤ U) (hc : IsCompl U Eā‚€)
    (B : Parameter (localVanishing D U) W) (C : Eā‚€ ā†’ā‚—[F2] W) : Parameter D W :=
ā€¦

    Mentions: OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.localVanishing

  26. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.join_apply line 282
  27. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.join_embed_apply_left line 287
  28. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.join_embed_apply_right line 294
  29. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.splitLeft_join line 300
  30. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.splitRight_join line 309
  31. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.join_split line 317
  32. def OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.splitEquiv line 331

    Source documentation

    Linear equivalence of the full restriction domain with the constrained component and the free complementary component.

    def splitEquiv (D U Eā‚€ : Submodule F2 E) (W : Submodule F2 F)
    (hDU : D ā‰¤ U) (hc : IsCompl U Eā‚€) :
    Parameter D W ā‰ƒā‚—[F2]
      (Parameter (localVanishing D U) W Ɨ (Eā‚€ ā†’ā‚—[F2] W)) where
ā€¦

    Mentions: OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.localVanishing

  33. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.splitEquiv_symm_apply line 355
  34. instance OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.freeFintype line 360
  35. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.expect_join line 369

    Source documentation

    Exact product uniform sampling on the original quotient-map parameters.

    theorem expect_join [Finite E] [Finite F]
    (D U Eā‚€ : Submodule F2 E) (W : Submodule F2 F)
    (hDU : D ā‰¤ U) (hc : IsCompl U Eā‚€) (f : Parameter D W ā†’ ā„) :
    (š”¼ A : Parameter D W, f A) =
      š”¼ B : Parameter (localVanishing D U) W,
        š”¼ C : Eā‚€ ā†’ā‚—[F2] W, f (join D U Eā‚€ W hDU hc B C) := by
ā€¦

    Mentions: OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.localVanishing, OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.join

  36. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.expect_restrict line 384

    Source documentation

    The same exact split for the observable on the actual affine restriction.

    theorem expect_restrict [Finite E] [Finite F]
    (D U Eā‚€ : Submodule F2 E) (W : Submodule F2 F)
    (hDU : D ā‰¤ U) (hc : IsCompl U Eā‚€) (T : E ā†’ā‚—[F2] F)
    (f : (E ā†’ā‚—[F2] F) ā†’ ā„) :
    (š”¼ A : Parameter D W, restrict f D W T A) =
      š”¼ B : Parameter (localVanishing D U) W,
        š”¼ C : Eā‚€ ā†’ā‚—[F2] W, f (translate D W T (join D U Eā‚€ W hDU hc B C)) :=
ā€¦

    Mentions: OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.localVanishing, OAI.MaxCutGames.Inverse.KMSAffineRestrictionSplit.join

  37. def OAI.MaxCutGames.Inverse.KMSAffineRestriction.complementBasis line 413

    Source documentation

    Basis obtained from a genuine complementary domain decomposition.

    def complementBasis (U E0 : Submodule F2 (Ambient ell)) (hc : IsCompl U E0)
    (bU : Module.Basis (Fin q) F2 U) (b0 : Module.Basis (Fin t) F2 E0) :
    Module.Basis (Fin q āŠ• Fin t) F2 (Ambient ell) :=
ā€¦
  38. theorem OAI.MaxCutGames.Inverse.KMSAffineRestriction.complementBasis_inl line 418
  39. theorem OAI.MaxCutGames.Inverse.KMSAffineRestriction.complementBasis_inr line 424
  40. def OAI.MaxCutGames.Inverse.KMSAffineRestriction.freeCenter line 431

    Source documentation

    The affine center restricted to directions whose images already lie in W.

    def freeCenter (E0 : Submodule F2 (Ambient ell)) (W : Submodule F2 (Ambient n))
    (T : BasisMap n ell) (hE0 : E0 ā‰¤ LinearMap.ker (W.mkQ.comp T)) : E0 ā†’ā‚—[F2] W :=
ā€¦
  41. theorem OAI.MaxCutGames.Inverse.KMSAffineRestriction.freeCenter_coe line 436
  42. theorem OAI.MaxCutGames.Inverse.KMSAffineRestriction.translate_join_eq_constr line 443

    Source documentation

    Exact pointwise identity for the actual affine slice after splitting its parameters. The fixed prefix includes the affine intercept.

    theorem translate_join_eq_constr
    (D U E0 : Submodule F2 (Ambient ell)) (W : Submodule F2 (Ambient n))
    (hDU : D ā‰¤ U) (hc : IsCompl U E0) (T : BasisMap n ell)
    (hE0 : E0 ā‰¤ LinearMap.ker (W.mkQ.comp T))
    (bU : Module.Basis (Fin q) F2 U) (b0 : Module.Basis (Fin t) F2 E0)
    (B : Parameter (localVanishing D U) W) (C : E0 ā†’ā‚—[F2] W) :
    MaxCutGames.Fourier.MatrixRestrictions.translate D W T (join D U E0 W hDU hc B C) =
      (complementBasis U E0 hc bU b0).constr F2
        (joinedTuple
          (fun i => T (bU i) + (B ((localVanishing D U).mkQ (bU i)) : Ambient n)) W
          (fun i => freeCenter E0 W T hE0 (b0 i) + C (b0 i))) := by
ā€¦

    Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.translate, OAI.MaxCutGames.Inverse.KMSAffineRestriction.complementBasis, OAI.MaxCutGames.Inverse.KMSAffineRestriction.freeCenter

  43. theorem OAI.MaxCutGames.Inverse.KMSAffineRestriction.affine_expect_of_complement line 469

    Source documentation

    A bounded adapted prefix controls the entire affine restriction law.

    theorem affine_expect_of_complement {r : ā„•} {Īµ : ā„}
    (S : Finset (Vertex n ell)) (hS : GrassmannPseudorandom S r Īµ) (hĪµ : 0 ā‰¤ Īµ)
    (D U E0 : Submodule F2 (Ambient ell)) (W : Submodule F2 (Ambient n))
    (hDU : D ā‰¤ U) (hc : IsCompl U E0) (T : BasisMap n ell)
    (hE0 : E0 ā‰¤ LinearMap.ker (W.mkQ.comp T))
    (hbudget : Module.finrank F2 U + (n - Module.finrank F2 W) ā‰¤ r) :
    (š”¼ A : Parameter D W, restrict (liftedIndicator S) D W T A) ā‰¤ Īµ := by
ā€¦
  44. theorem OAI.MaxCutGames.Inverse.KMSAffineRestriction.affine_expect_bound line 499

    Source documentation

    Every actual affine restriction of order d is sparse if all Grassmann intervals of complexity at most 2d are sparse. Both sampling factors remain uniform on their full finite spaces.

    theorem affine_expect_bound {d : ā„•} {Īµ : ā„}
    (S : Finset (Vertex n ell)) (hS : GrassmannPseudorandom S (2 * d) Īµ)
    (hĪµ : 0 ā‰¤ Īµ) (D : Submodule F2 (Ambient ell))
    (W : Submodule F2 (Ambient n)) (T : BasisMap n ell)
    (horder : order D W ā‰¤ d) :
    (š”¼ A : Parameter D W, restrict (liftedIndicator S) D W T A) ā‰¤ Īµ := by
ā€¦
  45. theorem OAI.MaxCutGames.Inverse.KMSAffineRestriction.affine_squared_expect_bound line 519

    Source documentation

    The normalized squared restriction norm is exactly the same sparse probability because the full-rank lift is Boolean.

    theorem affine_squared_expect_bound {d : ā„•} {Īµ : ā„}
    (S : Finset (Vertex n ell)) (hS : GrassmannPseudorandom S (2 * d) Īµ)
    (hĪµ : 0 ā‰¤ Īµ) (D : Submodule F2 (Ambient ell))
    (W : Submodule F2 (Ambient n)) (T : BasisMap n ell)
    (horder : order D W ā‰¤ d) :
    (š”¼ A : Parameter D W, (restrict (liftedIndicator S) D W T A) ^ 2) ā‰¤ Īµ := by
ā€¦
  46. def OAI.MaxCutGames.Inverse.KMSAffineRestrictionPresentation.parameterEquiv line 558

    Source documentation

    Change from surjective/injective presentation coordinates to the actual quotient-domain and subspace-target parameter.

    def parameterEquiv (L : E ā†’ā‚—[F2] D) (hL : Function.Surjective L)
    (J : C ā†’ā‚—[F2] F) (hJ : Function.Injective J) :
    (D ā†’ā‚—[F2] C) ā‰ƒā‚—[F2] Parameter L.ker J.range :=
ā€¦
  47. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionPresentation.parameterEquiv_apply_mk line 564
  48. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionPresentation.embed_parameterEquiv line 570

    Source documentation

    The embedded quotient parameter is the original two-sided composition.

    @[simp] theorem embed_parameterEquiv (L : E ā†’ā‚—[F2] D)
    (hL : Function.Surjective L) (J : C ā†’ā‚—[F2] F)
    (hJ : Function.Injective J) (X : D ā†’ā‚—[F2] C) :
    embed L.ker J.range (parameterEquiv L hL J hJ X) = J.comp (X.comp L) := by
ā€¦

    Mentions: OAI.MaxCutGames.Inverse.KMSAffineRestrictionPresentation.parameterEquiv

  49. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionPresentation.translate_parameterEquiv line 578
  50. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionPresentation.expect_presentation line 586

    Source documentation

    Exact uniform expectation in any presentation of the actual restriction.

    theorem expect_presentation [Finite E] [Finite F] [Fintype (D ā†’ā‚—[F2] C)]
    (L : E ā†’ā‚—[F2] D) (hL : Function.Surjective L)
    (J : C ā†’ā‚—[F2] F) (hJ : Function.Injective J)
    (T : E ā†’ā‚—[F2] F) (f : (E ā†’ā‚—[F2] F) ā†’ ā„) :
    (š”¼ X : D ā†’ā‚—[F2] C, f (T + J.comp (X.comp L))) =
      š”¼ A : Parameter L.ker J.range, restrict f L.ker J.range T A := by
ā€¦
  51. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionPresentation.expect_presentation_sq line 597

    Source documentation

    In particular, the normalized squared restriction norms coincide.

    theorem expect_presentation_sq [Finite E] [Finite F] [Fintype (D ā†’ā‚—[F2] C)]
    (L : E ā†’ā‚—[F2] D) (hL : Function.Surjective L)
    (J : C ā†’ā‚—[F2] F) (hJ : Function.Injective J)
    (T : E ā†’ā‚—[F2] F) (f : (E ā†’ā‚—[F2] F) ā†’ ā„) :
    (š”¼ X : D ā†’ā‚—[F2] C, f (T + J.comp (X.comp L)) ^ 2) =
      š”¼ A : Parameter L.ker J.range, (restrict f L.ker J.range T A) ^ 2 :=
ā€¦
  52. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionPresentation.order_add_dimensions line 607

    Source documentation

    The intrinsic restriction order is exactly the dimensions lost by the surjective input and injective output presentations.

    theorem order_add_dimensions [FiniteDimensional F2 E] [FiniteDimensional F2 F]
    (L : E ā†’ā‚—[F2] D) (hL : Function.Surjective L)
    (J : C ā†’ā‚—[F2] F) (hJ : Function.Injective J) :
    order L.ker J.range + Module.finrank F2 D + Module.finrank F2 C =
      Module.finrank F2 E + Module.finrank F2 F := by
ā€¦
  53. theorem OAI.MaxCutGames.Inverse.KMSAffineRestrictionPresentation.order_le_of_dimensions line 621

    Source documentation

    The sum-of-dimensions budget used in the fourth-moment statement implies the actual quotient/subspace restriction budget, without truncated subtraction.

    theorem order_le_of_dimensions [FiniteDimensional F2 E] [FiniteDimensional F2 F]
    (L : E ā†’ā‚—[F2] D) (hL : Function.Surjective L)
    (J : C ā†’ā‚—[F2] F) (hJ : Function.Injective J) (r : ā„•)
    (h : Module.finrank F2 E + Module.finrank F2 F ā‰¤
      Module.finrank F2 D + Module.finrank F2 C + r) :
    order L.ker J.range ā‰¤ r := by
ā€¦
  54. theorem OAI.MaxCutGames.Inverse.KMSAffineRestriction.lifted_affineDensityBound line 644

    Source documentation

    This supplies the local-density input of the genuine analytic induction from the actual lifted Grassmann indicator, with the exact order-two loss.

    theorem lifted_affineDensityBound {n ell d : ā„•} {Īµ : ā„}
    (S : Finset (Vertex n ell)) (hS : GrassmannPseudorandom S (2 * d) Īµ)
    (hĪµ : 0 ā‰¤ Īµ) : KMSFourthMoment.AffineDensityBound d Īµ (liftedIndicator S) := by
ā€¦

    Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound

  55. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonAffineDensity.lifted_expect_in_basis_of_tuple line 680

    Source documentation

    The tuple hypothesis bounds the lift in every domain basis: the lift depends only on the range, which is the span of the same prescribed tuple.

    theorem lifted_expect_in_basis_of_tuple (S : Finset (Vertex n ell))
    (hS : TuplePseudorandom S r Īµ)
    (b : Module.Basis (Fin q āŠ• Fin t) F2 (Ambient ell))
    (Q : Fin q ā†’ Ambient n) (W : Submodule F2 (Ambient n))
    (hbudget : q + (n - Module.finrank F2 W) ā‰¤ r) :
    (š”¼ z : Fin t ā†’ W, liftedIndicator S (b.constr F2 (joinedTuple Q W z))) ā‰¤ Īµ := by
ā€¦
  56. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonAffineDensity.lifted_expect_shifted_basis_of_tuple line 698

    Source documentation

    Translation of the free coordinates retains the full uniform tuple law.

    theorem lifted_expect_shifted_basis_of_tuple {E0 : Type*}
    [AddCommGroup E0] [Module F2 E0]
    (S : Finset (Vertex n ell)) (hS : TuplePseudorandom S r Īµ)
    (b : Module.Basis (Fin q āŠ• Fin t) F2 (Ambient ell))
    (Q : Fin q ā†’ Ambient n) (W : Submodule F2 (Ambient n))
    [Fintype (E0 ā†’ā‚—[F2] W)]
    (b0 : Module.Basis (Fin t) F2 E0) (T0 : E0 ā†’ā‚—[F2] W)
    (hbudget : q + (n - Module.finrank F2 W) ā‰¤ r) :
    (š”¼ H : E0 ā†’ā‚—[F2] W, liftedIndicator S
      (b.constr F2 (joinedTuple Q W (fun i => T0 (b0 i) + H (b0 i))))) ā‰¤ Īµ := by
ā€¦
  57. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonAffineDensity.affine_expect_of_complement_of_tuple line 720

    Source documentation

    The adapted prefix contains all directions whose affine center lies outside W. After splitting, each fixed constrained parameter gives an allowed arbitrary prefix, and all free coordinates remain uniform in W.

    theorem affine_expect_of_complement_of_tuple
    (S : Finset (Vertex n ell)) (hS : TuplePseudorandom S r Īµ)
    (D U E0 : Submodule F2 (Ambient ell)) (W : Submodule F2 (Ambient n))
    (hDU : D ā‰¤ U) (hc : IsCompl U E0) (T : BasisMap n ell)
    (hE0 : E0 ā‰¤ LinearMap.ker (W.mkQ.comp T))
    (hbudget : Module.finrank F2 U + (n - Module.finrank F2 W) ā‰¤ r) :
    (š”¼ A : Parameter D W, restrict (liftedIndicator S) D W T A) ā‰¤ Īµ := by
ā€¦
  58. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonAffineDensity.affine_expect_bound_of_tuple line 748

    Source documentation

    Order d affine restrictions require at most 2d tuple restriction budget.

    theorem affine_expect_bound_of_tuple {d : ā„•}
    (S : Finset (Vertex n ell)) (hS : TuplePseudorandom S (2 * d) Īµ)
    (D : Submodule F2 (Ambient ell)) (W : Submodule F2 (Ambient n))
    (T : BasisMap n ell) (horder : order D W ā‰¤ d) :
    (š”¼ A : Parameter D W, restrict (liftedIndicator S) D W T A) ā‰¤ Īµ := by
ā€¦
  59. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonAffineDensity.affine_squared_expect_bound_of_tuple line 766

    Source documentation

    Booleanity turns the exact restriction probability into its squared norm.

    theorem affine_squared_expect_bound_of_tuple {d : ā„•}
    (S : Finset (Vertex n ell)) (hS : TuplePseudorandom S (2 * d) Īµ)
    (D : Submodule F2 (Ambient ell)) (W : Submodule F2 (Ambient n))
    (T : BasisMap n ell) (horder : order D W ā‰¤ d) :
    (š”¼ A : Parameter D W, (restrict (liftedIndicator S) D W T A) ^ 2) ā‰¤ Īµ := by
ā€¦
  60. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonAffineDensity.lifted_affineDensityBound_of_tuple line 782

    Source documentation

    Directly discharge the fourth-moment affine density input from the literal tuple pseudorandomness input of the ordered-basis expansion theorem.

    theorem lifted_affineDensityBound_of_tuple {d : ā„•}
    (S : Finset (Vertex n ell)) (hS : TuplePseudorandom S (2 * d) Īµ) :
    KMSFourthMoment.AffineDensityBound d Īµ (liftedIndicator S) := by
ā€¦

    Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound