Canonical reference words in the one-sided weights

theorem CommutingRepetition.setWeightX_canon {n : ℕ} {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] [Nonempty X] [Nonempty Y] (R₀ : Finset (Fin n)) (μ : X → Y → ℝ) (xw : Fin n → X) (yw : Fin n → Y) : setWeightX R₀ μ (keepOn R₀ xw) (keepOff R₀ yw) = setWeightX R₀ μ xw yw

theorem CommutingRepetition.setWeightY_canon {n : ℕ} {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] [Nonempty X] [Nonempty Y] (R₀ : Finset (Fin n)) (μ : X → Y → ℝ) (xw : Fin n → X) (yw : Fin n → Y) : setWeightY R₀ μ (keepOff R₀ xw) (keepOn R₀ yw) = setWeightY R₀ μ xw yw

theorem CommutingRepetition.sum_comm4 {α β γ δ : Type} [Fintype α] [Fintype β] [Fintype γ] [Fintype δ] (F : α → β → γ → δ → ℝ) : ∑ a : α, ∑ b : β, ∑ c : γ, ∑ d : δ, F a b c d = ∑ c : γ, ∑ d : δ, ∑ a : α, ∑ b : β, F a b c d

Moving the last two of four finite sums to the front.

Payoff-weighted pairings

noncomputable def CommutingRepetition.TracialStrategy.coreSucc {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (V : X → Y → A → B → ℝ) (D : Finset (Fin n)) (i : Fin n) (x : X) (y : Y) (xw : Fin n → X) (yw : Fin n → Y) (zD : (↥D → A) × (↥D → B)) : ℝ

The word-level payoff-weighted core correlation at live payoff V(·,·∣x,y) read at coordinate i.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommutingRepetition.TracialStrategy.refinedPayoff {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (D : Finset (Fin n)) (i : Fin n) (x : X) (y : Y) (s : ALabel n X Y A) (t : BLabel n X Y B) : ℝ

The refined pairing mass at a pair of labels, weighted by the live payoff.

Equations

• S.refinedPayoff μ V D i x y s t = ∑ as : Fin n → A, ∑ bs : Fin n → B, V x y (as i) (bs i) * (S.M.τ (star S.σ * (S.refinedA D μ s as * S.σ * S.refinedB D μ t bs))).re

theorem CommutingRepetition.TracialStrategy.refinedPayoff_nonneg {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hV0 : ∀ (x : X) (y : Y) (a : A) (b : B), 0 ≤ V x y a b) (D : Finset (Fin n)) (i : Fin n) (x : X) (y : Y) (s : ALabel n X Y A) (t : BLabel n X Y B) : 0 ≤ S.refinedPayoff μ V D i x y s t

theorem CommutingRepetition.TracialStrategy.refinedPayoff_le {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hV1 : ∀ (x : X) (y : Y) (a : A) (b : B), V x y a b ≤ 1) (D : Finset (Fin n)) (i : Fin n) (x : X) (y : Y) (s : ALabel n X Y A) (t : BLabel n X Y B) : S.refinedPayoff μ V D i x y s t ≤ (S.M.τ (star S.σ * (S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2 * S.σ * S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2))).re

The payoff-weighted refined mass is at most the total branch mass.

theorem CommutingRepetition.TracialStrategy.re_pairing_refined {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (μ : X → Y → ℝ) (D : Finset (Fin n)) (s : ALabel n X Y A) (t : BLabel n X Y B) (as : Fin n → A) (bs : Fin n → B) : (S.M.τ (star S.σ * (S.refinedA D μ s as * S.σ * S.refinedB D μ t bs))).re = (∑ w : Fin n → X, setWeightX s.1 μ s.2.1 s.2.2.1 w)⁻¹ * (∑ v : Fin n → Y, setWeightY t.1 μ t.2.1 t.2.2.1 v)⁻¹ * ∑ w : Fin n → X, ∑ v : Fin n → Y, setWeightX s.1 μ s.2.1 s.2.2.1 w * setWeightY t.1 μ t.2.1 t.2.2.1 v * if agreesOn D as s.2.2.2 ∧ agreesOn D bs t.2.2.2 then S.correlation w v as bs else 0

The pairing of two refined effects at one answer pair.

theorem CommutingRepetition.TracialStrategy.priorWeight_refinedPayoff {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (r : RevealDatum n D) (xw : Fin n → X) (yw : Fin n → Y) (zD : (↥D → A) × (↥D → B)) : (∑ xw' : Fin n → X, ∑ yw' : Fin n → Y, priorWeight r μ xw yw xw' yw') * S.refinedPayoff μ V D r.i (xw r.i) (yw r.i) (aLabel D (insert r.i r.CX) xw yw zD.1) (bLabel D (insert r.i r.CY) xw yw zD.2) = ∑ xw' : Fin n → X, ∑ yw' : Fin n → Y, priorWeight r μ xw yw xw' yw' * S.coreSucc V D r.i (xw r.i) (yw r.i) xw' yw' zD

The tower identity for the payoff-weighted refined pairing (the refined form of branch_probability_core): the conditioned-prior mass times the refined pairing at the canonical labels is the prior-weighted sum of the word-level payoff-weighted correlations over the fiber.

The ideal answer pairing of the package

theorem CommutingRepetition.TracialStrategy.re_pairing_setEffect {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (s : ALabel n X Y A) (t : BLabel n X Y B) : (S.M.τ (star S.σ * (S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2 * S.σ * S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2))).re = ‖R.branch S.σ s t‖ ^ 2

The branch mass is the revealed-set pairing (branch_norm at the refined family's totals).

theorem CommutingRepetition.TracialStrategy.refinedPayoff_eq_zero {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hV0 : ∀ (x : X) (y : Y) (a : A) (b : B), 0 ≤ V x y a b) (hV1 : ∀ (x : X) (y : Y) (a : A) (b : B), V x y a b ≤ 1) (i : Fin n) (x : X) (y : Y) (s : ALabel n X Y A) (t : BLabel n X Y B) (hb : R.branch S.σ s t = 0) : S.refinedPayoff μ V D i x y s t = 0

Off the support of the branch, the payoff-weighted refined mass vanishes.

noncomputable def CommutingRepetition.TracialStrategy.idealPayoff {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (h : PostTuple n X Y A B D) (x : X) (y : Y) : ℝ

The payoff of the package's ideal answer law at a history and live questions (the summand of PreroundedStrategy.idealSuccess).

Equations

• S.idealPayoff μ V R h x y = ∑ a : A, ∑ b : B, V x y a b * CommutingRepetition.tracialPairLaw R.N (S.uVec μ R) (S.Apov μ R) (S.Bpov μ R) (h, x) (h, y) a b

noncomputable def CommutingRepetition.TracialStrategy.idealPayoffFlat {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (u : PostTuple n X Y A B D × X × Y) : ℝ

The same, on flattened tuples.

Equations

• S.idealPayoffFlat μ V R u = S.idealPayoff μ V R u.1 u.2.1 u.2.2

theorem CommutingRepetition.TracialStrategy.idealPayoff_eq {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (h : PostTuple n X Y A B D) (x : X) (y : Y) (hb : R.branch S.σ (labelA D h x) (labelB D h y) ≠ 0) : S.idealPayoff μ V R h x y = S.refinedPayoff μ V D h.1.i x y (labelA D h x) (labelB D h y) / ‖R.branch S.σ (labelA D h x) (labelB D h y)‖ ^ 2

The ideal payoff on a nonzero branch is the refined payoff-weighted mass divided by the branch mass (eq ideal-answer-law, coarse-grained).

The tower identity on posterior tuples

noncomputable def CommutingRepetition.TracialStrategy.tupleSucc {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (t : PostTuple n X Y A B D) : ℝ

The posterior-weighted refined payoff at a tuple's canonical labels.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommutingRepetition.TracialStrategy.tupleCore {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (t : PostTuple n X Y A B D) : ℝ

The posterior-weighted word-level payoff-weighted core correlation.

Equations

• One or more equations did not get rendered due to their size.

theorem CommutingRepetition.TracialStrategy.posteriorQ_mul_idealPayoff {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hV0 : ∀ (x : X) (y : Y) (a : A) (b : B), 0 ≤ V x y a b) (hV1 : ∀ (x : X) (y : Y) (a : A) (b : B), V x y a b ≤ 1) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (t : PostTuple n X Y A B D) : S.posteriorQ R D μ w p t * S.idealPayoffFlat μ V R (flattenPost t) = S.tupleSucc μ V w p t

The posterior mass times the ideal payoff at the flattened tuple: the branch mass cancels.

theorem CommutingRepetition.TracialStrategy.tupleSucc_fiber {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hwD : ∀ (xw xw' : Fin n → X) (yw yw' : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), agreesOn D xw xw' → agreesOn D yw yw' → w xw yw zA zB = w xw' yw' zA zB) (p : ℝ) (t : PostTuple n X Y A B D) : (∑ t' : PostTuple n X Y A B D, if flattenPost t' = flattenPost t then S.tupleSucc μ V w p t' else 0) = ∑ t' : PostTuple n X Y A B D, if flattenPost t' = flattenPost t then S.tupleCore μ V w p t' else 0

The tower property on a flattening fiber: the fiber sums of the refined-payoff and core-success tuple weights agree (priorWeight_refinedPayoff with the labels constant on the fiber).

theorem CommutingRepetition.TracialStrategy.sum_flatQ_idealPayoff {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hV0 : ∀ (x : X) (y : Y) (a : A) (b : B), 0 ≤ V x y a b) (hV1 : ∀ (x : X) (y : Y) (a : A) (b : B), V x y a b ≤ 1) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hwD : ∀ (xw xw' : Fin n → X) (yw yw' : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), agreesOn D xw xw' → agreesOn D yw yw' → w xw yw zA zB = w xw' yw' zA zB) (p : ℝ) : ∑ u : PostTuple n X Y A B D × X × Y, S.flatQ R D μ w p u * S.idealPayoffFlat μ V R u = ∑ t : PostTuple n X Y A B D, S.tupleCore μ V w p t

The ideal success of the package, on posterior tuples: the Q-average of the ideal payoff is the posterior-weighted word-level payoff-weighted core correlation.

Regrouping by the live coordinate

noncomputable def CommutingRepetition.TracialStrategy.liveSucc {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (i : Fin n) : ℝ

The payoff-weighted core success read at live coordinate i: ∑_{x,y} Πμ ∑_z w_D(z) · coreSucc_i.

Equations

• S.liveSucc μ V w i = ∑ xw : Fin n → X, ∑ yw : Fin n → Y, (∏ j : Fin n, μ (xw j) (yw j)) * ∑ zD : (↥D → A) × (↥D → B), w xw yw zD.1 zD.2 * S.coreSucc V D i (xw i) (yw i) xw yw zD

theorem CommutingRepetition.TracialStrategy.sum_tupleCore {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (V : X → Y → A → B → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) : ∑ t : PostTuple n X Y A B D, S.tupleCore μ V w p t = 1 / p * ∑ r : RevealDatum n D, r.revealLaw * S.liveSucc μ V w r.i

theorem CommutingRepetition.RevealDatum.sum_revealLaw_mul {n : ℕ} {D : Finset (Fin n)} (f : Fin n → ℝ) : ∑ r : RevealDatum n D, r.revealLaw * f r.i = ∑ i ∈ Finset.univ \ D, 1 / ↑(n - D.card) * f i

A reveal-law average of a function of the live coordinate is the uniform average over the non-core coordinates (revealLaw_sum_fiber).