OAI/Computability/MaxCut/Games/KMSMomentConstants.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

Explicit dimension-independent constants for the new KMS mixed-energy argument and the generic A5 aggregation. The eventual expansion theorem only uses positivity and finiteness of these constants, so no rank cutoff exception or comparison with an earlier rank-level constant is needed.

  1. def OAI.MaxCutGames.Inverse.KMSMomentConstants.fourthMomentConstant line 16

    Source documentation

    The constant after the genuine mixed-energy estimate and A5 aggregation.

    def fourthMomentConstant (r : ℕ) : ℝ := 2 ^ (109 * r * r + 2 * r)
  2. theorem OAI.MaxCutGames.Inverse.KMSMomentConstants.fourthMomentConstant_pos line 18
  3. theorem OAI.MaxCutGames.Inverse.KMSMomentConstants.fourthMomentConstant_nonneg line 22
  4. theorem OAI.MaxCutGames.Inverse.KMSMomentConstants.mixedRankConstant_eq line 26

    Source documentation

    The closed mixed estimate's literal constant has a quadratic exponent.

    theorem mixedRankConstant_eq (r : ℕ) :
    mixedRankConstant r = (2 : ℝ) ^ (6 * r * r + 2 * r) := by
…
  5. theorem OAI.MaxCutGames.Inverse.KMSMomentConstants.a5_mul_mixedRankConstant line 34

    Source documentation

    Multiplying by the actual selector-count and A5 constant is exact.

    theorem a5_mul_mixedRankConstant (r : ℕ) :
    (2 : ℝ) ^ (103 * r * r) * mixedRankConstant r = fourthMomentConstant r := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSMomentConstants.fourthMomentConstant

  6. theorem OAI.MaxCutGames.Inverse.KMSMomentConstants.fourthMomentConstant_mono line 41
  7. theorem OAI.MaxCutGames.Inverse.KMSMomentConstants.a5_mixed_bound line 51

    Source documentation

    The complete numerical closure, retaining the density and projection energy factors in the order used by the expansion interface.

    theorem a5_mixed_bound {i r : ℕ} (hi : i ≤ r) (ε η : ℝ)
    (hε : 0 ≤ ε) (hη : 0 ≤ η) :
    (2 : ℝ) ^ (103 * i * i) * (mixedRankConstant i * ε) * η ≤
      fourthMomentConstant r * η * ε := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSMomentConstants.fourthMomentConstant

  8. def OAI.MaxCutGames.Inverse.KMS.relativeDensity line 76

    Source documentation

    Relative density, with value zero when the conditioning set is empty.

    def relativeDensity (S I : Finset Ω) : ℝ :=
…
  9. theorem OAI.MaxCutGames.Inverse.KMS.inter_chart_eq line 81

    Source documentation

    Restricting the denominator to a chart containing the set preserves the numerator. This is the exact finite-set step used after Grassmann expansion.

    theorem inter_chart_eq (S I C : Finset Ω) (hSC : S ⊆ C) :
    S ∩ (I ∩ C) = S ∩ I := by
…
  10. theorem OAI.MaxCutGames.Inverse.KMS.chart_inter_nonempty line 93

    Source documentation

    A nonempty part of the set in an interval witnesses that the chart and interval meet. No positive denominator is silently assumed.

    theorem chart_inter_nonempty (S I C : Finset Ω) (hSC : S ⊆ C)
    (hSI : (S ∩ I).Nonempty) : (I ∩ C).Nonempty := by
…
  11. theorem OAI.MaxCutGames.Inverse.KMS.relativeDensity_le_chart line 101

    Source documentation

    Intersecting a nonempty conditioning interval with a chart containing the set can only increase its relative density.

    theorem relativeDensity_le_chart (S I C : Finset Ω) (hSC : S ⊆ C)
    (hIC : (I ∩ C).Nonempty) :
    relativeDensity S I ≤ relativeDensity S (I ∩ C) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMS.relativeDensity

  12. theorem OAI.MaxCutGames.Inverse.KMS.density_bound_passes_to_chart line 112

    Source documentation

    The quantitative density conclusion passes to the matrix chart without losing any factor.

    theorem density_bound_passes_to_chart (S I C : Finset Ω) (hSC : S ⊆ C)
    (hSI : (S ∩ I).Nonempty) {α : ℝ} (hα : α ≤ relativeDensity S I) :
    (I ∩ C).Nonempty ∧ α ≤ relativeDensity S (I ∩ C) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMS.relativeDensity

  13. abbrev OAI.MaxCutGames.Inverse.KMS.F2 line 120
  14. abbrev OAI.MaxCutGames.Inverse.KMS.Ambient line 121
  15. def OAI.MaxCutGames.Inverse.KMS.Vertex line 124

    Source documentation

    Actual ell-dimensional subspaces of the ambient binary vector space.

    def Vertex (n ell : ℕ) :=
…
  16. instance OAI.MaxCutGames.Inverse.KMS.vertexFinite line 127
  17. instance OAI.MaxCutGames.Inverse.KMS.vertexFintype line 134
  18. def OAI.MaxCutGames.Inverse.KMS.Adjacent line 138

    Source documentation

    A neighbor is distinct and meets the vertex in a hyperplane. The explicit distinctness also makes the definition harmless at dimension zero.

    def Adjacent {n ell : ℕ} (L M : Vertex n ell) : Prop :=
…

    Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex

  19. def OAI.MaxCutGames.Inverse.KMS.neighbors line 141
  20. def OAI.MaxCutGames.Inverse.KMS.retention line 145

    Source documentation

    Uniform start in S, followed by a uniform Grassmann neighbor.

    def retention {n ell : ℕ} (S : Finset (Vertex n ell)) : ℝ :=
…

    Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex

  21. def OAI.MaxCutGames.Inverse.KMS.interval line 149

    Source documentation

    The actual interval A ≤ L ≤ B among the ell-dimensional vertices.

    def interval {n ell : ℕ} (A B : Submodule F2 (Ambient n)) :
    Finset (Vertex n ell) :=
…

    Mentions: OAI.MaxCutGames.Inverse.KMS.F2, OAI.MaxCutGames.Inverse.KMS.Ambient, OAI.MaxCutGames.Inverse.KMS.Vertex

  22. def OAI.MaxCutGames.Inverse.KMS.ExpansionPrinciple line 157

    Source documentation

    The parameter order needed from KMS, including a nonempty dense interval. OPEN: no inhabitant of this proposition is supplied. In particular r and alpha must be fixed before ell, and the ambient threshold may then depend on ell. A bound with alpha = 2^(-ell) does not meet this interface.

    def ExpansionPrinciple : Prop :=
…
  23. abbrev OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap line 184
  24. instance OAI.MaxCutGames.Inverse.KMSBasisComparison.basisMapFinite line 186
  25. instance OAI.MaxCutGames.Inverse.KMSBasisComparison.basisMapFintype line 190
  26. def OAI.MaxCutGames.Inverse.KMSBasisComparison.InLift line 193

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

  27. def OAI.MaxCutGames.Inverse.KMSBasisComparison.lift line 197

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

  28. theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.mem_lift line 200
  29. def OAI.MaxCutGames.Inverse.KMSBasisComparison.liftedIndicator line 205

    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.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.InLift

  30. theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.liftedIndicator_nonneg line 208
  31. theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.liftedIndicator_le_one line 213
  32. theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.injective_of_inLift line 219

    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.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.InLift

  33. def OAI.MaxCutGames.Inverse.KMSBasisComparison.rangeVertex line 232

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

  34. theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.inLift_iff_rangeVertex_mem line 238
  35. theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.inLift_comp_iff line 249

    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.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMS.Ambient, OAI.MaxCutGames.Inverse.KMS.F2, OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.InLift

  36. theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.liftedIndicator_basisInvariant line 256

    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.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftedIndicator

  37. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.nat_card_eq_sum_fibers line 275

    Source documentation

    Decompose a finite domain by its exact fibers.

    theorem nat_card_eq_sum_fibers (f : X → Y) :
    Nat.card X = ∑ y : Y, Nat.card {x : X // f x = y} := by
…
  38. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.nat_card_event_eq_sum_fibers line 280

    Source documentation

    The event count is the sum of the same fibers over the event.

    theorem nat_card_event_eq_sum_fibers (f : X → Y) (p : Y → Prop) :
    Nat.card {x : X // p (f x)} =
      ∑ y : {y : Y // p y}, Nat.card {x : X // f x = y.val} := by
…
  39. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.uniformFiber_card_ratio line 293

    Source documentation

    Constant fibers give an exact density identity, including an empty target. The nonzero fiber size is established geometrically for restricted bases.

    theorem uniformFiber_card_ratio (f : X → Y) (p : Y → Prop)
    (c : ℕ) (hc : 0 < c)
    (hf : ∀ y, Nat.card {x : X // f x = y} = c) :
    (Nat.card {x : X // p (f x)} : ℝ) / Nat.card X =
      (Nat.card {y : Y // p y} : ℝ) / Nat.card Y := by
…
  40. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.subtype_event_ratio_le line 312

    Source documentation

    Sampling from a larger finite space and accepting only a subset never increases the density of an event within that subset. Empty subsets are handled explicitly, so this statement makes no hidden nonemptiness assumption.

    theorem subtype_event_ratio_le {Z : Type*} [Fintype Z] (D : Z → Prop)
    (p : {z : Z // D z} → Prop) :
    (Nat.card {z : {z : Z // D z} // p z} : ℝ) / Nat.card Z ≤
      (Nat.card {z : {z : Z // D z} // p z} : ℝ) / Nat.card {z : Z // D z} := by
…
  41. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.exists_restricted_completion line 341

    Source documentation

    Restricted completion of an independent frame. The original vectors need not belong to W; only the newly chosen vectors are required to do so.

    theorem exists_restricted_completion {n q t : ℕ}
    (Q : Fin q → Ambient n) (W L : Submodule F2 (Ambient n))
    (hQ : LinearIndependent F2 Q)
    (hQL : Submodule.span F2 (Set.range Q) ≤ L)
    (hLW : L ≤ Submodule.span F2 (Set.range Q) ⊔ W)
    (hL : Module.finrank F2 L = q + t) :
    ∃ z : Fin t → W,
      LinearIndependent F2 (Sum.elim Q (fun i => (z i : Ambient n))) ∧
        Submodule.span F2
          (Set.range (Sum.elim Q (fun i => (z i : Ambient n)))) = L := by
…
  42. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion line 421

    Source documentation

    Ordered completions in W of Q to an independent spanning tuple for L.

    def RestrictedCompletion (Q : Fin q → V) (W L : Submodule K V) :=
…
  43. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionBasis line 429

    Source documentation

    A completion, regarded as a basis of the resulting subspace.

    def completionBasis (z : RestrictedCompletion (t := t) Q W L) :
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion

  44. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionBasis_coe line 433
  45. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionOfBasis line 439

    Source documentation

    Recover a restricted completion from a basis having the prescribed prefix.

    def completionOfBasis (b : Module.Basis (Fin q ⊕ Fin t) K L)
    (hQ : ∀ i, (b (Sum.inl i) : V) = Q i)
    (hW : ∀ i, (b (Sum.inr i) : V) ∈ W) :
    RestrictedCompletion (t := t) Q W L := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion

  46. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv line 461

    Source documentation

    The unique basis change carrying the first completion to the second.

    def completionSpanEquiv
    (x : RestrictedCompletion (t := t) Q W L)
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion

  47. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv_basis line 466
  48. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv_symm line 472
  49. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv_sub_mem line 479

    Source documentation

    Changing the completion changes every vector by an element of W.

    theorem completionSpanEquiv_sub_mem
    (x : RestrictedCompletion (t := t) Q W L)
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion

  50. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv_mem_iff line 500

    Source documentation

    The basis change preserves membership in W, without requiring Q ⊆ W.

    theorem completionSpanEquiv_mem_iff
    (x : RestrictedCompletion (t := t) Q W L)
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion

  51. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.transportCompletion line 512

    Source documentation

    Transport every restricted completion along one fixed basis change.

    def transportCompletion
    (x : RestrictedCompletion (t := t) Q W L)
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion

  52. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.transportCompletion_coe line 530
  53. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.transportCompletion_inverse line 537
  54. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.restrictedCompletionEquiv line 554

    Source documentation

    All nonempty restricted-completion fibers are equivalent.

    def restrictedCompletionEquiv
    (x : RestrictedCompletion (t := t) Q W L)
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion

  55. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.restrictedCompletionCard_eq line 564

    Source documentation

    Equal fiber cardinality follows from the explicit completion equivalence.

    theorem restrictedCompletionCard_eq
    (x : RestrictedCompletion (t := t) Q W L)
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion

  56. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.prefixSpan line 587
  57. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.joinedTuple line 590
  58. abbrev OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.IndependentCompletion line 594
  59. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionVertex line 597
  60. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.prefix_le_completion line 602
  61. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completion_le_sup line 609
  62. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completion_mem_interval line 621
  63. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.prefix_independent line 627
  64. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.interval_complexity_le line 633

    Source documentation

    The restriction's Grassmann interval satisfies the same total complexity budget. This uses only W ≤ span Q ⊔ W, never the false assumption Q ⊆ W.

    theorem interval_complexity_le (Q : Fin q → Ambient n) (W : Submodule F2 (Ambient n))
    (hQ : LinearIndependent F2 Q) :
    Module.finrank F2 (prefixSpan Q) +
      (n - Module.finrank F2 ↥(prefixSpan Q ⊔ W : Submodule F2 (Ambient n))) ≤
        q + (n - Module.finrank F2 W) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.prefixSpan

  65. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.GrassmannPseudorandom line 647
  66. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionEvent line 653
  67. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity line 659

    Source documentation

    The denominator counts all remaining tuples drawn uniformly from W. Dependent completions are rejected, without conditioning away their mass.

    def restrictedLiftDensity (S : Finset (Vertex n (q + t)))
    (Q : Fin q → Ambient n) (W : Submodule F2 (Ambient n)) : ℝ :=
…
  68. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.TuplePseudorandom line 664
  69. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity_eq_zero_of_dependent line 670
  70. abbrev OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.IntervalVertex line 680
  71. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionIntervalVertex line 683
  72. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionFiberEquiv line 687
  73. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.interval_completion_nonempty line 697
  74. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.completionEventEquiv line 706
  75. def OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.intervalEventEquiv line 715
  76. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.independent_density_eq_interval line 727

    Source documentation

    The uniform law on successful completions is exactly the uniform Grassmann interval law, even when the fixed prefix is not contained in W.

    theorem independent_density_eq_interval (S : Finset (Vertex n (q + t)))
    (Q : Fin q → Ambient n) (W : Submodule F2 (Ambient n))
    (hQ : LinearIndependent F2 Q)
    (z₀ : IndependentCompletion (t := t) Q W) :
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.IndependentCompletion

  77. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity_le_interval line 758

    Source documentation

    The unconditioned restricted lift has density at most that of its exact Grassmann interval. Unlike a union-bound argument, no independence-error term is needed because dependent tuples are rejected by the lift.

    theorem restrictedLiftDensity_le_interval (S : Finset (Vertex n (q + t)))
    (Q : Fin q → Ambient n) (W : Submodule F2 (Ambient n))
    (hQ : LinearIndependent F2 Q) :
    restrictedLiftDensity S Q W ≤
      relativeDensity S (interval (prefixSpan Q) (prefixSpan Q ⊔ W)) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity, OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.prefixSpan

  78. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.grassmann_pseudorandom_restricted line 776

    Source documentation

    The full KMS restriction transfer, with the stronger exact ε bound.

    theorem grassmann_pseudorandom_restricted {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) :
    restrictedLiftDensity S Q W ≤ ε := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.GrassmannPseudorandom, OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity

  79. theorem OAI.MaxCutGames.Inverse.KMSBasisComparisonPseudorandom.grassmann_pseudorandom_lift line 788