Reindexing.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Coordinate reindexing for actual finite distributions and repeated games. The joint questions are iid across coordinates; coordinate-success events need not be independent. Strategies permute each player's local questions and answers, so the resulting strategies remain local.

def OAI.MaxCutGames.Foundations.Games.FiniteDistribution.reindexEquiv line 21
theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.pushforward_equiv line 27
theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.table_const_reindex line 45
theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.iid_reindex line 58

theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_reindex_of_weight line 70

Source documentation

Weighted finite change of «variables»; no independence hypothesis.

theorem probability_reindex_of_weight {Ω Γ : Type*} [Fintype Ω] [Fintype Γ]
    (μ : FiniteDistribution Ω) (ν : FiniteDistribution Γ) (e : Ω ≃ Γ)
    (hweight : ∀ x, ν.weight (e x) = μ.weight x) (event : Γ → Bool) :
    ν.probability event = μ.probability (fun x => event (e x)) := by
…

Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution

def OAI.MaxCutGames.Foundations.Games.Game.questionReindexEquiv line 89

def OAI.MaxCutGames.Foundations.Games.Game.reindexStrategy line 95

Source documentation

Each player only permutes that player's own questions and answers.

def reindexStrategy {n m : Nat} (e : Fin m ≃ Fin n)
    (s : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂)) :
    Strategy (Fin m → Q₁) (Fin m → Q₂) (Fin m → A₁) (Fin m → A₂) :=
…

Mentions: OAI.MaxCutGames.Foundations.Games.Strategy

theorem OAI.MaxCutGames.Foundations.Games.Game.repetition_question_weight_reindex line 102
Source documentation
Simultaneous coordinate permutation preserves the actual joint question weight.
```
theorem repetition_question_weight_reindex (G : Game Q₁ Q₂ A₁ A₂)
    {n m : Nat} (e : Fin m ≃ Fin n)
    (q : (Fin n → Q₁) × (Fin n → Q₂)) :
    (G.repetition m).questions.weight (questionReindexEquiv e q) =
      (G.repetition n).questions.weight q := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Foundations.Games.Game.questionReindexEquiv
theorem OAI.MaxCutGames.Foundations.Games.Game.repetition_questions_reindex line 113
theorem OAI.MaxCutGames.Foundations.Games.Game.coordinateWin_reindex line 127
Source documentation
Coordinate successes transform pointwise; they are not assumed independent.
```
theorem coordinateWin_reindex (G : Game Q₁ Q₂ A₁ A₂)
    {n m : Nat} (e : Fin m ≃ Fin n)
    (s : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (i : Fin m) (q : (Fin n → Q₁) × (Fin n → Q₂)) :
    G.coordinateWin (reindexStrategy e s) i (questionReindexEquiv e q) =
      G.coordinateWin s (e i) q := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Foundations.Games.Strategy, OAI.MaxCutGames.Foundations.Games.Game.reindexStrategy, OAI.MaxCutGames.Foundations.Games.Game.questionReindexEquiv
theorem OAI.MaxCutGames.Foundations.Games.Game.selectedWins_reindex line 145
theorem OAI.MaxCutGames.Foundations.Games.Game.selectedSuccess_reindex line 166
Source documentation
The actual selected-success probability is invariant under the same relabeling.
```
theorem selectedSuccess_reindex (G : Game Q₁ Q₂ A₁ A₂)
    {n m : Nat} (e : Fin m ≃ Fin n)
    (s : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (S : Finset (Fin m)) :
    G.selectedSuccess (reindexStrategy e s) S =
      G.selectedSuccess s (S.map e.toEmbedding) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Foundations.Games.Strategy, OAI.MaxCutGames.Foundations.Games.Game.reindexStrategy
theorem OAI.MaxCutGames.Foundations.Games.Game.repetition_success_reindex line 182
Source documentation
Full repetition success is a special case, including zero repetitions.
```
theorem repetition_success_reindex (G : Game Q₁ Q₂ A₁ A₂)
    {n m : Nat} (e : Fin m ≃ Fin n)
    (s : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂)) :
    (G.repetition m).success (reindexStrategy e s) =
      (G.repetition n).success s := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Foundations.Games.Strategy, OAI.MaxCutGames.Foundations.Games.Game.success, OAI.MaxCutGames.Foundations.Games.Game.reindexStrategy