OAI/Computability/UniqueGames/Inverse/KMSBasisComparisonPseudorandomTupleMapLemmas.lean

GitHub source file

61 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.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.tupleBasis line 33
  2. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.tupleMapEquiv line 36
  3. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.tupleMap line 39
  4. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.tupleMap_range line 42
  5. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.tupleMap_basis line 46
  6. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.tupleMap_injective_iff line 50
  7. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.inLift_tupleMap_iff line 60
  8. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity_eq_expect line 77

    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.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.tupleMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.joinedTuple

  9. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.grassmann_pseudorandom_lift_expect line 88

    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.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.GrassmannPseudorandom, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.tupleMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonPseudorandom.joinedTuple

  10. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.lifted_expect_in_basis line 118

    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.UniqueGamesTheorem.Inverse.KMSAffineRestriction.affineCoordinates line 136

    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.UniqueGamesTheorem.Inverse.KMSAffineRestriction.affineCoordinates_apply line 142
  13. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.lifted_expect_shifted_basis line 148

    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. def OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.complementBasis line 191

    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) :=
…
  15. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.complementBasis_inl line 196
  16. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.complementBasis_inr line 202
  17. def OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.freeCenter line 209

    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 :=
…
  18. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.freeCenter_coe line 214
  19. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.translate_join_eq_constr line 221

    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) :
    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.UniqueGamesTheorem.Inverse.KMSAffineRestriction.complementBasis, OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.freeCenter

  20. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.affine_expect_of_complement line 247

    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
…
  21. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.affine_expect_bound line 277

    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
…
  22. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.affine_squared_expect_bound line 297

    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
…
  23. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fullStepRetention line 335

    Source documentation

    The complete rank-one update experiment at a specified starting map.

    def fullStepRetention {n ell : β„•} (S : Finset (KMS.Vertex n ell))
    (X : BasisMap n ell) : ℝ :=
…

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

  24. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRetention line 341

    Source documentation

    Start uniformly in the lifted set, then run the unconditioned update.

    def liftRetention {n ell : β„•} (S : Finset (KMS.Vertex n ell)) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex

  25. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.goodParametersEquiv line 345

    Source documentation

    Equivalence of the two explicit presentations of the good sampling event.

    def goodParametersEquiv {n ell : β„•} (X : BasisMap n ell) :
    goodParameters X ≃ OutsideNeighborFactors X where
…

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

  26. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.goodParameters_expect line 355

    Source documentation

    Good-event conditioning is the exact full-neighbor Grassmann retention.

    theorem goodParameters_expect {n ell : β„•} (S : Finset (KMS.Vertex n ell))
    (X : BasisMap n ell) (hX : Function.Injective X) :
    (goodParameters X).expect
      (fun p => liftedIndicator S (rankOneUpdate X p.1 p.2)) =
        KMS.relativeDensity S (KMS.neighbors (rangeVertex X hX)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.goodParameters, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftedIndicator, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdate, OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity, OAI.UniqueGamesTheorem.Inverse.KMS.neighbors, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rangeVertex

  27. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fullStepRetention_compare line 369

    Source documentation

    Quantitative local comparison, with a slightly smaller exceptional-mass bound than the stated KMS Lemma 2.7.

    theorem fullStepRetention_compare {n ell : β„•} (S : Finset (KMS.Vertex n ell))
    (X : BasisMap n ell) (hX : Function.Injective X) :
    |fullStepRetention S X -
      KMS.relativeDensity S (KMS.neighbors (rangeVertex X hX))| ≀
        ((2 : ℝ) ^ ell)⁻¹ + (2 : ℝ) ^ ell / (2 : ℝ) ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fullStepRetention, OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity, OAI.UniqueGamesTheorem.Inverse.KMS.neighbors, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rangeVertex

  28. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRange_retention_expect line 383

    Source documentation

    Choosing a uniform accepted ordered basis chooses a uniform element of the original Grassmann set.

    theorem liftRange_retention_expect {n ell : β„•} (S : Finset (KMS.Vertex n ell)) :
    (𝔼 X : lift S,
      KMS.relativeDensity S (KMS.neighbors (liftRange S X).val)) = KMS.retention S := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.lift, OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity, OAI.UniqueGamesTheorem.Inverse.KMS.neighbors, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRange, OAI.UniqueGamesTheorem.Inverse.KMS.retention

  29. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRetention_compare line 397

    Source documentation

    The actual full sampling-law comparison for the lifted Grassmann set.

    theorem liftRetention_compare {n ell : β„•} (S : Finset (KMS.Vertex n ell))
    (hS : S.Nonempty) :
    |liftRetention S - KMS.retention S| ≀
      ((2 : ℝ) ^ ell)⁻¹ + (2 : ℝ) ^ ell / (2 : ℝ) ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRetention, OAI.UniqueGamesTheorem.Inverse.KMS.retention

  30. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRetention_compare_kms line 413

    Source documentation

    The bound in the primary statement, with ordinary quotient notation instead of an integer exponent ell - n.

    theorem liftRetention_compare_kms {n ell : β„•} (S : Finset (KMS.Vertex n ell))
    (hS : S.Nonempty) :
    |liftRetention S - KMS.retention S| ≀
      ((2 : ℝ) ^ ell)⁻¹ + 2 * ((2 : ℝ) ^ ell / (2 : ℝ) ^ n) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRetention, OAI.UniqueGamesTheorem.Inverse.KMS.retention

  31. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftDensity line 421

    Source documentation

    The indicator's density in the full linear-map space.

    def liftDensity {n ell : β„•} (S : Finset (KMS.Vertex n ell)) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex

  32. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftDensity_eq_card line 424
  33. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftDensity_pos line 429
  34. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftDensity_mul_retention line 438

    Source documentation

    Fourier correlation uses the full ambient space. This identity is the exact conversion to the conditional-start retention and preserves density.

    theorem liftDensity_mul_retention {n ell : β„•} (S : Finset (KMS.Vertex n ell)) :
    liftDensity S * liftRetention S =
      𝔼 X : BasisMap n ell, liftedIndicator S X * fullStepRetention S X := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftDensity, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRetention, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftedIndicator, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fullStepRetention

  35. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fullStepRetention_eq_noise line 449

    Source documentation

    Swapping the independent factors matches the Fourier noise convention of first choosing a direction, then a functional, including both zero cases.

    theorem fullStepRetention_eq_noise {n ell : β„•} (S : Finset (KMS.Vertex n ell))
    (X : BasisMap n ell) :
    fullStepRetention S X =
      𝔼 y : KMS.Ambient n, 𝔼 a : Functional ell,
        liftedIndicator S (X + a.smulRight y) := by
…

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

  36. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRetention_le_of_correlation_le line 460

    Source documentation

    A proved ambient correlation bound converts directly to the conditional retention bound; positive density follows from the actual nonempty lift.

    theorem liftRetention_le_of_correlation_le {n ell : β„•}
    (S : Finset (KMS.Vertex n ell)) (hS : S.Nonempty) (ΞΆ : ℝ)
    (hc : (𝔼 X : BasisMap n ell,
      liftedIndicator S X * fullStepRetention S X) ≀ ΞΆ * liftDensity S) :
    liftRetention S ≀ ΞΆ := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftedIndicator, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.fullStepRetention, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftDensity, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftRetention

  37. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.LiftExpansionPrinciple line 483

    Source documentation

    The precise analytic obligation at the ordered-basis lift. Its constants are fixed before the tuple length, which is fixed before the ambient size.

    def LiftExpansionPrinciple : Prop :=
…
  38. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.exists_binary_ratio_threshold line 493

    Source documentation

    Elementary eventual decay, using Archimedean unboundedness of powers. No dimensional rate is hidden in a limit or a filter assumption.

    theorem exists_binary_ratio_threshold (c Ξ΅ : ℝ) (hΞ΅ : 0 < Ξ΅) :
    βˆƒ k : β„•, βˆ€ n : β„•, k ≀ n β†’ c / (2 : ℝ) ^ n ≀ Ξ΅ := by
…
  39. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.nonempty_of_relativeDensity_pos line 506

    Source documentation

    Positive relative density implies a nonempty intersection, even though relative density itself is defined to be zero on empty intervals.

    theorem nonempty_of_relativeDensity_pos {Ξ© : Type*} [DecidableEq Ξ©]
    (S I : Finset Ω) (h : 0 < KMS.relativeDensity S I) : (S ∩ I).Nonempty := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity

  40. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.expansion_of_liftExpansion line 514

    Source documentation

    The complete inverse implication from the explicit analytic lift theorem to the dimension-uniform Grassmann theorem required by the inverse.

    theorem expansion_of_liftExpansion (h : LiftExpansionPrinciple) :
    KMS.ExpansionPrinciple := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.LiftExpansionPrinciple, OAI.UniqueGamesTheorem.Inverse.KMS.ExpansionPrinciple

  41. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.familyLinearEquiv line 567

    Source documentation

    A finite family specifies exactly one linear map on its coordinate space.

    def familyLinearEquiv (n : β„•) (ΞΉ : Type*) [Fintype ΞΉ] :
    (ΞΉ β†’ KMS.Ambient n) ≃ₗ[KMS.F2] ((ΞΉ β†’ KMS.F2) β†’β‚—[KMS.F2] KMS.Ambient n) :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Ambient, OAI.UniqueGamesTheorem.Inverse.KMS.F2

  42. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.familyLinearEquiv_apply_basis line 571
  43. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.familyLinearEquiv_symm_apply line 576
  44. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.familyLinearEquiv_range line 580
  45. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.familyLinearEquiv_injective_iff line 586

    Source documentation

    Full rank of the corresponding map is exactly independence of the tuple.

    theorem familyLinearEquiv_injective_iff (n : β„•) (ΞΉ : Type*) [Fintype ΞΉ]
    (v : ΞΉ β†’ KMS.Ambient n) :
    Function.Injective (familyLinearEquiv n ΞΉ v) ↔ LinearIndependent KMS.F2 v := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Ambient, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.familyLinearEquiv, OAI.UniqueGamesTheorem.Inverse.KMS.F2

  46. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.family_expect line 597
  47. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.tupleLinearEquiv line 604
  48. def OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.tupleEquiv line 608
  49. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.basisMap_card line 611
  50. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.tupleLinearEquiv_apply_basis line 615
  51. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.tupleLinearEquiv_symm_apply line 620
  52. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.tupleLinearEquiv_range line 624
  53. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.tupleLinearEquiv_injective_iff line 628
  54. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.tuple_expect line 633

    Source documentation

    The complete uniform tuple law equals the complete uniform map law.

    theorem tuple_expect {n ell : β„•} {M : Type*} [AddCommMonoid M] [Module β„šβ‰₯0 M]
    (g : BasisMap n ell β†’ M) :
    (𝔼 v : Fin ell β†’ KMS.Ambient n, g (tupleLinearEquiv n ell v)) = 𝔼 X, g X :=
…

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

  55. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOne_tuple_coordinate line 640

    Source documentation

    On tuples, a rank-one map perturbation adds the same vector at coordinates selected by the corresponding binary functional.

    theorem rankOne_tuple_coordinate {n ell : β„•} (X : BasisMap n ell)
    (l : KMS.Ambient ell β†’β‚—[KMS.F2] KMS.F2) (v : KMS.Ambient n) (i : Fin ell) :
    (tupleLinearEquiv n ell).symm (X + l.smulRight v) i =
      (tupleLinearEquiv n ell).symm X i + l (Pi.basisFun KMS.F2 (Fin ell) i) β€’ v :=
…

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

  56. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.inLift_tuple_iff line 648

    Source documentation

    The lift tests precisely whether the tuple spans a selected Grassmann vertex; independence is forced by membership in the selected dimension.

    theorem inLift_tuple_iff {n ell : β„•} (S : Finset (KMS.Vertex n ell))
    (v : Fin ell β†’ KMS.Ambient n) :
    InLift S (tupleLinearEquiv n ell v) ↔
      βˆƒ L ∈ S, Submodule.span KMS.F2 (Set.range v) = L.val := by
…

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

  57. theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.linearIndependent_of_inLift_tuple line 654
  58. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.selector_energy_le line 684

    Source documentation

    The actual selector multiplicity on frequencies of rank at most d. This uses only the proved finite subspace count and Parseval.

    theorem selector_energy_le (d : β„•) (g : (E β†’β‚—[F2] F) β†’ ℝ)
    (hg : DegreeAtMost d g) :
    hybridSelectorEnergy d g ≀ (2 : ℝ) ^ (3 * d * d) * (𝔼 X, g X ^ 2) := by
…
  59. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.fourth_moment_le_of_uniform_hybrid_energy line 706

    Source documentation

    Generic closure of the fourth-moment estimate from a uniform bound on the actual hybrid derivatives. Its eventual KMS application must prove hH from the basis-invariant function and its local densities.

    theorem fourth_moment_le_of_uniform_hybrid_energy
    (d : β„•) (g : (E β†’β‚—[F2] F) β†’ ℝ) (hg : DegreeAtMost d g)
    (H : ℝ) (hH0 : 0 ≀ H)
    (hH : βˆ€ (A : Submodule F2 E) (B : Submodule F2 F) (T : E β†’β‚—[F2] F),
      order A B ≀ d β†’ (𝔼 N, hybridDerivative A B T g N ^ 2) ≀ H) :
    (𝔼 X, g X ^ 4) ≀ (2 : ℝ) ^ (103 * d * d) * H * (𝔼 X, g X ^ 2) := by
…
  60. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.rankComponent_degree line 760

    Source documentation

    Actual finite Fourier support of the component, with no rank-level inequality invoked.

    theorem rankComponent_degree (i : β„•) (f : (E β†’β‚—[F2] F) β†’ ℝ) :
    DerivativeDegree.DegreeAtMost i (rankComponent i f) := by
…
  61. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.rankComponent_fourth_moment_le_of_hybrid line 769

    Source documentation

    Generic fourth-moment closure for the literal KMS rank component.

    theorem rankComponent_fourth_moment_le_of_hybrid (i : β„•)
    (f : (E β†’β‚—[F2] F) β†’ ℝ) (H : ℝ) (hH0 : 0 ≀ H)
    (hH : βˆ€ (A : Submodule F2 E) (B : Submodule F2 F) (T : E β†’β‚—[F2] F),
      order A B ≀ i β†’
      (𝔼 N, Derivatives.hybridDerivative A B T (rankComponent i f) N ^ 2) ≀ H) :
    (𝔼 X, rankComponent i f X ^ 4) ≀
      (2 : ℝ) ^ (103 * i * i) * H * (𝔼 X, rankComponent i f X ^ 2) :=
…