OAI/Computability/UniqueGames/Games/FactorizationLemmas.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

The finite product algebra of dependency breaking.

Revealing one endpoint of each independently sampled question pair turns the remaining question weight into a product of two separate functions, one for each player. Further separate restrictions on the players' answers preserve this product. The final theorem normalizes the displayed weights, rather than assuming conditional independence as an abstract hypothesis.

  1. def OAI.UniqueGamesTheorem.Foundations.Repetition.revealedProductWeight line 41

    Source documentation

    mask i = false reveals the first question, and true the second.

    def revealedProductWeight (weight : ι → α → β → ℝ) (mask : ι → Bool)
    (fixedLeft : ι → α) (fixedRight : ι → β) (x : ι → α) (y : ι → β) : ℝ :=
…
  2. def OAI.UniqueGamesTheorem.Foundations.Repetition.revealedLeftWeight line 47
  3. def OAI.UniqueGamesTheorem.Foundations.Repetition.revealedRightWeight line 52
  4. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealedProductWeight_factorizes line 60

    Source documentation

    Exact factorization after fixing the selected endpoint at every position. No assumption on coordinate alphabets or probabilities is needed for this identity, so it applies separately at every fixed outside question tuple.

    theorem revealedProductWeight_factorizes (weight : ι → α → β → ℝ) (mask : ι → Bool)
    (fixedLeft : ι → α) (fixedRight : ι → β) (x : ι → α) (y : ι → β) :
    revealedProductWeight weight mask fixedLeft fixedRight x y =
      revealedLeftWeight weight mask fixedLeft fixedRight x *
        revealedRightWeight weight mask fixedLeft fixedRight y := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.revealedProductWeight, OAI.UniqueGamesTheorem.Foundations.Repetition.revealedLeftWeight, OAI.UniqueGamesTheorem.Foundations.Repetition.revealedRightWeight

  5. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealedProductWeight_local_restrictions line 75

    Source documentation

    Local answer tests are separate functions of the complete local question vectors. Multiplying by both tests leaves a product of two local weights.

    theorem revealedProductWeight_local_restrictions
    (weight : ι → α → β → ℝ) (mask : ι → Bool)
    (fixedLeft : ι → α) (fixedRight : ι → β)
    (leftTest : (ι → α) → ℝ) (rightTest : (ι → β) → ℝ)
    (x : ι → α) (y : ι → β) :
    revealedProductWeight weight mask fixedLeft fixedRight x y * leftTest x * rightTest y =
      (revealedLeftWeight weight mask fixedLeft fixedRight x * leftTest x) *
      (revealedRightWeight weight mask fixedLeft fixedRight y * rightTest y) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.revealedProductWeight, OAI.UniqueGamesTheorem.Foundations.Repetition.revealedLeftWeight, OAI.UniqueGamesTheorem.Foundations.Repetition.revealedRightWeight

  6. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.productWeight_mass line 88
  7. def OAI.UniqueGamesTheorem.Foundations.Repetition.normalizedWeight line 94
  8. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.normalizedWeight_isProbability line 97
  9. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.normalized_productWeight line 107

    Source documentation

    Normalizing an actual product weight gives the product of its separately normalized marginals. This is the finite conditional-independence identity.

    theorem normalized_productWeight (left : X → ℝ) (right : Y → ℝ)
    (hleft : 0 < ∑ x, left x) (hright : 0 < ∑ y, right y) (xy : X × Y) :
    normalizedWeight (fun z : X × Y => left z.1 * right z.2) xy =
      normalizedWeight left xy.1 * normalizedWeight right xy.2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.normalizedWeight

  10. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.normalized_rectangle_restriction line 117

    Source documentation

    Conditioning a product law on separate local events keeps the two factors independent, with each conditioned on its own event.

    theorem normalized_rectangle_restriction
    (left : X → ℝ) (right : Y → ℝ) (leftTest : X → ℝ) (rightTest : Y → ℝ)
    (hleft : 0 < ∑ x, left x * leftTest x)
    (hright : 0 < ∑ y, right y * rightTest y) (xy : X × Y) :
    normalizedWeight
      (fun z : X × Y => left z.1 * right z.2 * leftTest z.1 * rightTest z.2) xy =
      normalizedWeight (fun x => left x * leftTest x) xy.1 *
      normalizedWeight (fun y => right y * rightTest y) xy.2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.normalizedWeight

  11. def OAI.UniqueGamesTheorem.Foundations.Repetition.normalizeOr line 152
  12. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.sum_mul_normalizeOr line 160
  13. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.local_completion_recombination line 177

    Source documentation

    Exact reconstruction from two separately normalized local completion laws, valid even when either unnormalized row has mass zero.

    theorem local_completion_recombination
    (left : X → ℝ) (right : Y → ℝ)
    (hl : ∀ x, 0 ≤ left x) (hr : ∀ y, 0 ≤ right y)
    (defaultLeft : FiniteDistribution X) (defaultRight : FiniteDistribution Y)
    (c : ℝ) (x : X) (y : Y) :
    (c * (∑ z, left z) * (∑ z, right z)) *
      ((normalizeOr left hl defaultLeft).weight x *
        (normalizeOr right hr defaultRight).weight y) = c * left x * right y := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.normalizeOr

  14. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.factorized_completion_row line 192

    Source documentation

    The row mass appearing in reconstruction is the actual sum of product weights, not an assumed marginal identity.

    theorem factorized_completion_row
    (left : X → ℝ) (right : Y → ℝ)
    (hl : ∀ x, 0 ≤ left x) (hr : ∀ y, 0 ≤ right y)
    (defaultLeft : FiniteDistribution X) (defaultRight : FiniteDistribution Y)
    (c : ℝ) (xy : X × Y) :
    (∑ z : X × Y, c * left z.1 * right z.2) *
      ((normalizeOr left hl defaultLeft).product
        (normalizeOr right hr defaultRight)).weight xy = c * left xy.1 * right xy.2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.normalizeOr

  15. def OAI.UniqueGamesTheorem.Foundations.Games.Game.localEmbeddingLaw line 231
  16. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.success_le_value_add_embedding_distance line 241

    Source documentation

    Any finite shared-randomness local embedding yields a valid base-game strategy after the seed is fixed. Total variation pays exactly for changing the resulting question distribution to the desired one.

    theorem success_le_value_add_embedding_distance
    (G : Game Q₁ Q₂ A₁ A₂) (H : Game R₁ R₂ B₁ B₂)
    (seedLaw : FiniteDistribution Seed)
    (left : Seed → Q₁ → R₁) (right : Seed → Q₂ → R₂)
    (answerLeft : Seed → Q₁ → B₁ → A₁)
    (answerRight : Seed → Q₂ → B₂ → A₂)
    (acceptance : ∀ seed x y a b,
      H.accepts (left seed x) (right seed y) a b = true →
      G.accepts x y (answerLeft seed x a) (answerRight seed y b) = true)
    (strategy : Strategy R₁ R₂ B₁ B₂) :
    H.success strategy ≤ G.value +
      H.questions.totalVariation (G.localEmbeddingLaw seedLaw left right) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Game, OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution, OAI.UniqueGamesTheorem.Foundations.Games.Strategy

  17. def OAI.UniqueGamesTheorem.Foundations.Games.Game.coordinateGame line 271

    Source documentation

    A single tested coordinate under an arbitrary full-tuple question law.

    def coordinateGame (G : Game Q₁ Q₂ A₁ A₂) {n : Nat} (coordinate : Fin n)
    (law : FiniteDistribution ((Fin n → Q₁) × (Fin n → Q₂))) :
    Game (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Game, OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution

  18. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.coordinate_probability_le_value_add_embedding_distance line 280

    Source documentation

    The strategy-extraction step used for a surviving coordinate after conditioning on successes at other coordinates. It preserves full local question dependence and uses no independence assumption on the target law.

    theorem coordinate_probability_le_value_add_embedding_distance
    (G : Game Q₁ Q₂ A₁ A₂) {n : Nat} (coordinate : Fin n)
    (law : FiniteDistribution ((Fin n → Q₁) × (Fin n → Q₂)))
    (seedLaw : FiniteDistribution Seed)
    (left : Seed → Q₁ → Fin n → Q₁) (right : Seed → Q₂ → Fin n → Q₂)
    (left_preserves : ∀ seed x, left seed x coordinate = x)
    (right_preserves : ∀ seed y, right seed y coordinate = y)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂)) :
    law.probability (G.coordinateWin strategy coordinate) ≤ G.value +
      law.totalVariation (G.localEmbeddingLaw seedLaw left right) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Game, OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution, OAI.UniqueGamesTheorem.Foundations.Games.Strategy

  19. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.coordinate_probability_le_value_of_approximate_embeddings line 298

    Source documentation

    Finite samplers may have an arbitrarily small exhaustion error. Passing to the limit in the numerical bound does not require an infinite seed or a claim that any finite sampler terminates with probability one.

    theorem coordinate_probability_le_value_of_approximate_embeddings
    {SeedFamily : Nat → Type*} [∀ t, Fintype (SeedFamily t)]
    (G : Game Q₁ Q₂ A₁ A₂) {n : Nat} (coordinate : Fin n)
    (law : FiniteDistribution ((Fin n → Q₁) × (Fin n → Q₂)))
    (seedLaw : (t : Nat) → FiniteDistribution (SeedFamily t))
    (left : (t : Nat) → SeedFamily t → Q₁ → Fin n → Q₁)
    (right : (t : Nat) → SeedFamily t → Q₂ → Fin n → Q₂)
    (left_preserves : ∀ t seed x, left t seed x coordinate = x)
    (right_preserves : ∀ t seed y, right t seed y coordinate = y)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (distance : ℝ)
    (close : ∀ η : ℝ, 0 < η → ∃ t,
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Game, OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution, OAI.UniqueGamesTheorem.Foundations.Games.Strategy

  20. def OAI.UniqueGamesTheorem.Foundations.Repetition.ProfileCorrection.seedQuestionMarginal line 337
  21. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.ProfileCorrection.seedQuestionMarginal_isProbability line 340
  22. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.ProfileCorrection.seedQuestionMarginal_first line 351
  23. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.ProfileCorrection.totalVariation_triangle line 356
  24. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.ProfileCorrection.left_profile_correction line 365
  25. def OAI.UniqueGamesTheorem.Foundations.Repetition.revealEndpoint line 426
  26. def OAI.UniqueGamesTheorem.Foundations.Repetition.revealLaw line 430

    Source documentation

    Independently reveal either endpoint with probability one half.

    def revealLaw (μ : FiniteDistribution (X × Y)) :
    FiniteDistribution ((X × Y) × (X ⊕ Y)) :=
…
  27. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealLaw_weight line 435
  28. def OAI.UniqueGamesTheorem.Foundations.Repetition.revealFirstLaw line 445
  29. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealFirstLaw_weight line 450
  30. def OAI.UniqueGamesTheorem.Foundations.Repetition.revealFallback line 456

    Source documentation

    The default row still preserves the displayed endpoint if that endpoint has zero probability in the base question law.

    def revealFallback (μ : FiniteDistribution (X × Y)) (r : X ⊕ Y) :
    FiniteDistribution (X × Y) :=
…
  31. def OAI.UniqueGamesTheorem.Foundations.Repetition.revealProfile line 462
  32. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealProfile_inl_support line 466
  33. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealProfile_inr_support line 478
  34. def OAI.UniqueGamesTheorem.Foundations.Repetition.revealInputLaw line 490
  35. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealInputLaw_weight line 493
  36. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.reveal_profile_recombination line 501

    Source documentation

    The conditional product representation is proved from the sampled law, including reveal values with zero probability.

    theorem reveal_profile_recombination (μ : FiniteDistribution (X × Y))
    (r : X ⊕ Y) (q : X × Y) :
    (revealInputLaw μ).weight r * (revealProfile μ r).weight q =
      (revealLaw μ).weight (q,r) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.revealInputLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.revealProfile, OAI.UniqueGamesTheorem.Foundations.Repetition.revealLaw

  37. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.reveal_profile_inl_recombination line 508
  38. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.reveal_profile_inr_recombination line 515
  39. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealInputLaw_inl line 522
  40. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealInputLaw_inr line 530
  41. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealProfile_inl_diagonal line 537
  42. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealProfile_inr_diagonal line 559
  43. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealLaw_sum_left line 585
  44. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealLaw_sum_right line 590
  45. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealLaw_forget line 595
  46. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.reveal_product_factorization line 607

    Source documentation

    A conditional product of independently revealed coordinates has its exact point weight. This is the product identity used by the information bound, derived from the single-coordinate sampled distribution.

    theorem reveal_product_factorization {ι : Type*} [Fintype ι]
    (μ : FiniteDistribution (X × Y)) (r : ι → X ⊕ Y) (q : ι → X × Y) :
    (∏ i, (revealInputLaw μ).weight (r i)) *
      (∏ i, (revealProfile μ (r i)).weight (q i)) =
        ∏ i, (revealLaw μ).weight (q i,r i) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.revealInputLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.revealProfile, OAI.UniqueGamesTheorem.Foundations.Repetition.revealLaw

  47. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.reveal_product_forget line 617
  48. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.reveal_product_expectation line 636

    Source documentation

    Marginalizing the reveal variables restores the original independent question law for every observable, including the selected-win likelihood.

    theorem reveal_product_expectation {ι : Type*} [Fintype ι] [DecidableEq ι]
    (μ : FiniteDistribution (X × Y)) (f : (ι → X × Y) → ℝ) :
    (∑ r : ι → X ⊕ Y,
      (∏ i, (revealInputLaw μ).weight (r i)) *
        ∑ q : ι → X × Y, (∏ i, (revealProfile μ (r i)).weight (q i)) * f q) =
      ∑ q : ι → X × Y, (∏ i, μ.weight (q i)) * f q := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.revealInputLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.revealProfile

  49. def OAI.UniqueGamesTheorem.Foundations.Repetition.logTwo line 659
  50. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.logTwo_one line 661
  51. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.logTwo_inv_le_of_half_pow_le line 663
  52. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.contraction_step line 676

    Source documentation

    A nonzero step below the cutoff contracts by (1+v)/2.

    theorem contraction_step {v ell : ℝ} {n m : ℕ} {p next : ℝ}
    (hv0 : 0 ≤ v) (hv1 : v < 1) (hell : 1 ≤ ell)
    (hm : 1 ≤ m) (hmn : m < n) (hp : 0 ≤ p)
    (hmono : next ≤ p)
    (hprev : p ≤ ((1 + v) / 2) ^ m)
    (hcut : 2700 * (m : ℝ) * ell ≤ (1 - v) ^ 2 * ((n : ℝ) - m))
    (hstep : next ≤ p * (v + 15 * Real.sqrt
      (((m : ℝ) * ell + logTwo (1 / p)) / ((n : ℝ) - m)))) :
    next ≤ ((1 + v) / 2) ^ (m + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.logTwo

  53. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.initial_step line 716

    Source documentation

    The m=0 case does not use the estimate m+1 ≤ 2*m*ell.

    theorem initial_step {v ell next : ℝ} {n : ℕ}
    (hstep : next ≤ 1 * (v + 15 * Real.sqrt
      (((0 : ℝ) * ell + logTwo (1 / 1)) / ((n : ℝ) - 0)))) :
    next ≤ v := by simpa using hstep

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.logTwo

  54. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.cutoff_step line 722

    Source documentation

    A real cutoff gives a valid step at every integer strictly below it.

    theorem cutoff_step {v ell : ℝ} {n m : ℕ}
    (hv0 : 0 ≤ v) (hv1 : v < 1) (hell : 1 ≤ ell)
    (hm : (m : ℝ) < (n : ℝ) * (1 - v) ^ 2 / (2925 * ell)) :
    2700 * (m : ℝ) * ell ≤ (1 - v) ^ 2 * ((n : ℝ) - m) := by
…
  55. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.cutoff_le_length line 734
  56. def OAI.UniqueGamesTheorem.Foundations.Repetition.ScalarRecurrence line 743

    Source documentation

    The explicit recurrence obtained from a 15*sqrt embedding error.

    def ScalarRecurrence (p : ℕ → ℝ) (n : ℕ) (v ell : ℝ) : Prop :=
…
  57. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.decay_to_cutoff line 749

    Source documentation

    Induction to the ceiling of the real cutoff repairs the integer-rounding omission in the printed scalar proof.

    theorem decay_to_cutoff (p : ℕ → ℝ) (n : ℕ) {v ell : ℝ}
    (hv0 : 0 ≤ v) (hv1 : v < 1) (hell : 1 ≤ ell)
    (hp0 : p 0 = 1) (hpnonneg : ∀ m, 0 ≤ p m)
    (hpmono : Antitone p) (hrec : ScalarRecurrence p n v ell) :
    p n ≤ ((1 + v) / 2) ^
      ((n : ℝ) * (1 - v) ^ 2 / (2925 * ell)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.ScalarRecurrence

  58. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.block_contraction line 787

    Source documentation

    The loss in one real-power block is cubic in the initial gap.

    theorem block_contraction {v : ℝ} (hv0 : 0 ≤ v) (hv1 : v < 1) :
    ((1 + v) / 2) ^ ((1 - v) ^ 2 / 2925 : ℝ) ≤
      1 - (1 - v) ^ 3 / 5850 := by
…
  59. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.scalar_bound_6000 line 802

    Source documentation

    Numerical endpoint of Holenstein's recurrence, with the published constant 6000. This theorem assumes only a concrete scalar recurrence, not any game value bound. The derivation of that recurrence for games is separate.

    theorem scalar_bound_6000 (p : ℕ → ℝ) (n : ℕ) {v ell : ℝ}
    (hv0 : 0 ≤ v) (hv1 : v < 1) (hell : 1 ≤ ell)
    (hp0 : p 0 = 1) (hpnonneg : ∀ m, 0 ≤ p m)
    (hpmono : Antitone p) (hrec : ScalarRecurrence p n v ell) :
    p n ≤ (1 - (1 - v) ^ 3 / 6000) ^ ((n : ℝ) / ell) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.ScalarRecurrence

  60. def OAI.UniqueGamesTheorem.Foundations.Repetition.incidenceRate line 825
  61. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.incidenceRate_pos line 827
  62. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.incidenceRate_lt_one line 829
  63. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.incidenceRate_fourth line 832

    Source documentation

    Exact rational arithmetic verifies the fourth-power comparison.

    theorem incidenceRate_fourth :
    1 - (1 / 192 : ℝ) ^ 3 / 6000 ≤ incidenceRate ^ 4 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.incidenceRate

  64. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.incidence_rate_comparison line 838

    Source documentation

    Converting the real exponent n/4 to an integral power loses only the explicit slack already built into incidenceRate.

    theorem incidence_rate_comparison (n : ℕ) :
    (1 - (1 / 192 : ℝ) ^ 3 / 6000) ^ ((n : ℝ) / 4) ≤ incidenceRate ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.incidenceRate

  65. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.scalar_incidence_bound line 851

    Source documentation

    The incidence-game rate follows from its concrete scalar recurrence. The game-to-recurrence proof is deliberately not hidden in this statement.

    theorem scalar_incidence_bound (p : ℕ → ℝ) (n : ℕ) {v : ℝ}
    (hv : v ≤ 1 - (1 / 192 : ℝ))
    (hp0 : p 0 = 1) (hpnonneg : ∀ m, 0 ≤ p m)
    (hpmono : Antitone p) (hrec : ScalarRecurrence p n v 4) :
    p n ≤ incidenceRate ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.ScalarRecurrence, OAI.UniqueGamesTheorem.Foundations.Repetition.incidenceRate