Product.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Projection constraints and independent products on the existing classical game API. A strategy receives only its own full question, even in a product game. The projection property is an actual uniqueness property of the acceptance predicate; it is not a premise asserting a repetition bound.

def OAI.MaxCutGames.Repetition.IsProjection line 26
Source documentation
The left answer determines at most one accepting right answer. Partial projection predicates are included, as are total projection maps.
```
def IsProjection (G : Game Q₁ Q₂ A₁ A₂) : Prop :=
…
```
theorem OAI.MaxCutGames.Repetition.IsProjection.of_accepts_iff line 30
theorem OAI.MaxCutGames.Repetition.IsProjection.repetition line 39
Source documentation
Parallel repetition preserves projection constraints, including at n = 0. There is no restriction that a repeated strategy act coordinatewise.
```
theorem IsProjection.repetition {G : Game Q₁ Q₂ A₁ A₂}
    (hG : IsProjection G) (n : Nat) : IsProjection (G.repetition n) := by
…
```
Mentions: OAI.MaxCutGames.Repetition.IsProjection
def OAI.MaxCutGames.Repetition.ofProjection line 49
Source documentation
Total projection maps give ordinary finite classical games. Question weights may be arbitrary nonnegative real weights summing to one.
```
def ofProjection (questions : FiniteDistribution (Q₁ × Q₂))
    (project : Q₁ → Q₂ → A₁ → A₂) : Game Q₁ Q₂ A₁ A₂ := by
…
```
theorem OAI.MaxCutGames.Repetition.ofProjection_accepts_iff line 54
theorem OAI.MaxCutGames.Repetition.ofProjection_isProjection line 61
def OAI.MaxCutGames.Repetition.productQuestionEquiv line 66
Source documentation
Regroup independently sampled question pairs into the two local questions.
```
def productQuestionEquiv :
    ((Q₁ × Q₂) × (R₁ × R₂)) ≃ ((Q₁ × R₁) × (Q₂ × R₂)) where
…
```
def OAI.MaxCutGames.Repetition.product line 75
Source documentation
Independent conjunction product. Each answer may depend on the full local pair of questions; locality is inherited from Game and Strategy.
```
def product (G : Game Q₁ Q₂ A₁ A₂) (H : Game R₁ R₂ B₁ B₂) :
    Game (Q₁ × R₁) (Q₂ × R₂) (A₁ × B₁) (A₂ × B₂) where
…
```
theorem OAI.MaxCutGames.Repetition.product_question_weight line 80
theorem OAI.MaxCutGames.Repetition.product_accepts_iff line 86
theorem OAI.MaxCutGames.Repetition.IsProjection.product line 93
def OAI.MaxCutGames.Repetition.productStrategy line 100
theorem OAI.MaxCutGames.Repetition.success_productStrategy line 106
Source documentation
The independent product of two strategies has exactly multiplicative success. This gives a lower bound for the maximum, not a decay upper bound.
```
theorem success_productStrategy (G : Game Q₁ Q₂ A₁ A₂) (H : Game R₁ R₂ B₁ B₂)
    (s : Strategy Q₁ Q₂ A₁ A₂) (t : Strategy R₁ R₂ B₁ B₂) :
    (product G H).success (productStrategy s t) = G.success s * H.success t := by
…
```
Mentions: OAI.MaxCutGames.Repetition.product, OAI.MaxCutGames.Repetition.productStrategy
theorem OAI.MaxCutGames.Repetition.mul_value_le_product_value line 123