noncomputable def CommutingRepetition.TracialStrategy.margY {X Y : Type} [Fintype X] (μ : X → Y → ℝ) (y : Y) : ℝ

The Bob question marginal μ_Y.

Equations

• CommutingRepetition.TracialStrategy.margY μ y = ∑ x : X, μ x y

theorem CommutingRepetition.TracialStrategy.margY_nonneg {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] [Nonempty X] [Nonempty Y] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (y : Y) : 0 ≤ margY μ y

theorem CommutingRepetition.TracialStrategy.mu_le_margY {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] [Nonempty X] [Nonempty Y] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (x : X) (y : Y) : μ x y ≤ margY μ y

theorem CommutingRepetition.TracialStrategy.sum_margY {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] [Nonempty X] [Nonempty Y] (μ : X → Y → ℝ) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) : ∑ y : Y, margY μ y = 1

theorem CommutingRepetition.TracialStrategy.classMass_prodPrior_univ_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] {D : Finset (Fin n)} (SX SY : Finset (Fin n)) (hcov : SX ∪ SY = Finset.univ) (μ : X → Y → ℝ) (s : CoreTuple n X Y A B D) (hμY : ∀ j ∈ SY \ SX, ∑ x : X, μ x (s.2.1 j) ≠ 0) : classMass Finset.univ SY (prodPrior D μ) s = classMass SX SY (prodPrior D μ) s * ∏ j ∈ SY \ SX, μ (s.1 j) (s.2.1 j) / ∑ x : X, μ x (s.2.1 j)

The prior class-mass ratio with the Alice set enlarged to everything: the pinned-to-marginal ratios on SY \ SX.

theorem CommutingRepetition.TracialStrategy.blockBoundB {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 → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (hw1 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), w xw yw zA zB ≤ 1) {p : ℝ} (hp : p = S.coreMass D μ w) (hppos : 0 < p) (SX SY : Finset (Fin n)) (hcov : SX ∪ SY = Finset.univ) (L : Finset (Fin n)) (hL : L = SY \ SX) (π : Fin L.card ≃ ↥L) : ∑ s : CoreTuple n X Y A B D, S.corePost D μ w p s * (Real.log (classMass Finset.univ SY (S.corePost D μ w p) s / classMass SX SY (S.corePost D μ w p) s) - ∑ k : Fin L.card, Real.log (μ (s.1 ↑(π k)) (s.2.1 ↑(π k)) / margY μ (s.2.1 ↑(π k)))) ≤ Real.log p⁻¹ + ↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B))

The block conditional bound, Bob side: Bob's set fixed, Alice's enlarged to everything against the background SX.

The second chain term (Bob side): the Alice reverse experiment

noncomputable def CommutingRepetition.TracialStrategy.histLogB {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [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 → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (r : RevealDatum n D) (s : CoreTuple n X Y A B D) : ℝ

The integrand of the Bob-side second chain term at datum r: log ℚ⁰(x_i ∣ X_{C_X}, Y_{{i}∪C_Y}, Z) − log μ(x_i ∣ y_i).

Equations

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

theorem CommutingRepetition.TracialStrategy.cutSumHistB_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)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (hw1 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), w xw yw zA zB ≤ 1) {p : ℝ} (hp : p = S.coreMass D μ w) (hppos : 0 < p) (b : AliceBase n D) : ∑ k : Fin (Dᶜ \ ↑b.fst).card, ∑ s : CoreTuple n X Y A B D, S.corePost D μ w p s * (Real.log (classMass (b.SA ∪ ordPrefix b.πY (↑k + 1)) b.SB (S.corePost D μ w p) s / classMass (b.SA ∪ ordPrefix b.πY ↑k) b.SB (S.corePost D μ w p) s) - Real.log (μ (s.1 ↑(b.πY k)) (s.2.1 ↑(b.πY k)) / margY μ (s.2.1 ↑(b.πY k)))) ≤ Real.log p⁻¹ + ↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B))

Per-base telescoped bound, Bob side: Alice's set grows along the Bob-block order at a fixed Alice base.

theorem CommutingRepetition.TracialStrategy.secondTermB_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)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (hw1 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), w xw yw zA zB ≤ 1) {p : ℝ} (hp : p = S.coreMass D μ w) (hppos : 0 < p) (hm : D.card < n) : ∑ r : RevealDatum n D, r.revealLaw * ∑ s : CoreTuple n X Y A B D, S.corePost D μ w p s * S.histLogB μ w p r s ≤ 2 * (Real.log p⁻¹ + ↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B))) / (↑n - ↑D.card)

The Bob-side second chain term is at most 2(t₀ + s₀)/m: the reveal datum as (Alice base, interior cut), the size-biased law (2/m)·β.

The flattened laws, Bob side

noncomputable def CommutingRepetition.TracialStrategy.histY {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (D : Finset (Fin n)) (μ : X → Y → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (h : PostTuple n X Y A B D) (y : Y) : ℝ

ℚ(h, y) = ∑_x ℚ(h, x, y).

Equations

• S.histY R D μ w p h y = ∑ x : X, S.flatQ R D μ w p (h, x, y)

noncomputable def CommutingRepetition.TracialStrategy.liveY {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (D : Finset (Fin n)) (μ : X → Y → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (i₀ : Fin n) (y : Y) : ℝ

ℚ(i, Y_i = y).

Equations

• S.liveY R D μ w p i₀ y = ∑ h : CommutingRepetition.TracialStrategy.PostTuple n X Y A B D, if h.1.i = i₀ then S.histY R D μ w p h y else 0

theorem CommutingRepetition.TracialStrategy.condQB_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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (μ : X → Y → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (i₀ : Fin n) (y : Y) (h : PostTuple n X Y A B D) : S.condQB R D μ w p i₀ y h = if h.1.i = i₀ then S.histY R D μ w p h y / S.liveY R D μ w p i₀ y else 0

theorem CommutingRepetition.TracialStrategy.flatJB_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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (μ : X → Y → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (u : PostTuple n X Y A B D × X × Y) : S.flatJB R D μ w p u = (↑(n - D.card))⁻¹ * μ u.2.1 u.2.2 * (S.histY R D μ w p u.1 u.2.2 / S.liveY R D μ w p u.1.1.i u.2.2)

theorem CommutingRepetition.TracialStrategy.histY_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)) {D : Finset (Fin n)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) {p : ℝ} (hppos : 0 < p) (h : PostTuple n X Y A B D) (y : Y) : 0 ≤ S.histY R D μ w p h y

theorem CommutingRepetition.TracialStrategy.flatQ_le_histY {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) {p : ℝ} (hppos : 0 < p) (h : PostTuple n X Y A B D) (x : X) (y : Y) : S.flatQ R D μ w p (h, x, y) ≤ S.histY R D μ w p h y

theorem CommutingRepetition.TracialStrategy.liveY_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)) {D : Finset (Fin n)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) {p : ℝ} (hppos : 0 < p) (i₀ : Fin n) (y : Y) : 0 ≤ S.liveY R D μ w p i₀ y

theorem CommutingRepetition.TracialStrategy.histY_le_liveY {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) {p : ℝ} (hppos : 0 < p) (h : PostTuple n X Y A B D) (y : Y) : S.histY R D μ w p h y ≤ S.liveY R D μ w p h.1.i y

theorem CommutingRepetition.TracialStrategy.liveY_eq_zero_of_mem {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (μ : X → Y → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (i₀ : Fin n) (hi₀ : i₀ ∈ D) (y : Y) : S.liveY R D μ w p i₀ y = 0

theorem CommutingRepetition.TracialStrategy.sum_flatQ_histY {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (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) : ∑ x : X, S.flatQ R D μ w p (histCore t, x, t.2.2.1 t.1.i) = t.1.revealLaw * classMass t.1.CX (insert t.1.i t.1.CY) (S.corePost D μ w p) t.2

(F2, Bob) The flattened posterior summed over the live Alice question.

theorem CommutingRepetition.TracialStrategy.sum_flatQ_liveY {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (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 : ℝ) (i₀ : Fin n) (y : Y) : (∑ h : PostTuple n X Y A B D, if h.1.i = i₀ then ∑ x : X, S.flatQ R D μ w p (h, x, y) else 0) = (∑ r : RevealDatum n D, if r.i = i₀ then r.revealLaw else 0) * ∑ s : CoreTuple n X Y A B D, if s.2.1 i₀ = y then S.corePost D μ w p s else 0

(F3, Bob) The flattened posterior mass of a live coordinate and live Bob question.

theorem CommutingRepetition.TracialStrategy.sum_flatQ_groupY {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (μ : X → Y → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (F : Fin n → Y → ℝ) : ∑ u : PostTuple n X Y A B D × X × Y, S.flatQ R D μ w p u * F u.1.1.i u.2.2 = ∑ i₀ : Fin n, ∑ y : Y, S.liveY R D μ w p i₀ y * F i₀ y

Sums over the flattened space grouped by the live coordinate and the live Bob question.

noncomputable def CommutingRepetition.TracialStrategy.coreMargY {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 → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (yw : Fin n → Y) : ℝ

The Bob question marginal of the core posterior.

Equations

• S.coreMargY μ w p yw = ∑ xw : Fin n → X, ∑ zD : (↥D → A) × (↥D → B), S.corePost D μ w p (xw, yw, zD)

theorem CommutingRepetition.TracialStrategy.coreMargY_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)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) {p : ℝ} (hppos : 0 < p) (yw : Fin n → Y) : 0 ≤ S.coreMargY μ w p yw

theorem CommutingRepetition.TracialStrategy.sum_corePost_triple {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] {D : Finset (Fin n)} (f : CoreTuple n X Y A B D → ℝ) : ∑ s : CoreTuple n X Y A B D, f s = ∑ xw : Fin n → X, ∑ yw : Fin n → Y, ∑ zD : (↥D → A) × (↥D → B), f (xw, yw, zD)

The core posterior as a triple sum.

theorem CommutingRepetition.TracialStrategy.sum_coreMargY {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 → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) {p : ℝ} (hp : p = S.coreMass D μ w) (hppos : 0 < p) : ∑ yw : Fin n → Y, S.coreMargY μ w p yw = 1

theorem CommutingRepetition.TracialStrategy.coreMargY_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)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (hw1 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), w xw yw zA zB ≤ 1) {p : ℝ} (hppos : 0 < p) (yw : Fin n → Y) : S.coreMargY μ w p yw ≤ p⁻¹ * ∏ j : Fin n, margY μ (yw j)

ℚ⁰_Y ≤ p⁻¹ · μ_Y^{⊗n}.

theorem CommutingRepetition.TracialStrategy.sum_corePost_coordY {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 → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (i₀ : Fin n) (y : Y) : (∑ s : CoreTuple n X Y A B D, if s.2.1 i₀ = y then S.corePost D μ w p s else 0) = HistoryKL.coordMarginal (S.coreMargY μ w p) i₀ y

theorem CommutingRepetition.TracialStrategy.firstTermB_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)) {D : Finset (Fin n)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (hw1 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), w xw yw zA zB ≤ 1) (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 : ℝ} (hp : p = S.coreMass D μ w) (hppos : 0 < p) (hm : D.card < n) : ∑ u : PostTuple n X Y A B D × X × Y, S.flatQ R D μ w p u * Real.log (S.liveY R D μ w p u.1.1.i u.2.2 * ↑(n - D.card) / margY μ u.2.2) ≤ Real.log p⁻¹ / (↑n - ↑D.card)

The Bob-side first chain term is at most t₀/m.

theorem CommutingRepetition.TracialStrategy.secondTermB_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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (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 : ℝ} (hppos : 0 < p) : ∑ u : PostTuple n X Y A B D × X × Y, S.flatQ R D μ w p u * Real.log (S.flatQ R D μ w p u * margY μ u.2.2 / (S.histY R D μ w p u.1 u.2.2 * μ u.2.1 u.2.2)) = ∑ r : RevealDatum n D, r.revealLaw * ∑ s : CoreTuple n X Y A B D, S.corePost D μ w p s * S.histLogB μ w p r s

The Bob-side second chain term in core form.

The Bob conjunct

theorem CommutingRepetition.TracialStrategy.flatJB_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)) {D : Finset (Fin n)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) {p : ℝ} (hppos : 0 < p) (u : PostTuple n X Y A B D × X × Y) : 0 ≤ S.flatJB R D μ w p u

theorem CommutingRepetition.TracialStrategy.flatQ_eq_zero_of_flatJB {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (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 : ℝ} (hppos : 0 < p) (hm : D.card < n) (u : PostTuple n X Y A B D × X × Y) (hu : S.flatJB R D μ w p u = 0) : S.flatQ R D μ w p u = 0

theorem CommutingRepetition.TracialStrategy.sum_flatJB_le_one {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) (R : ResolverArena S.M Ffam Gfam) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) {p : ℝ} (hppos : 0 < p) (hm : D.card < n) : ∑ u : PostTuple n X Y A B D × X × Y, S.flatJB R D μ w p u ≤ 1

J_B is subnormalized.

theorem CommutingRepetition.TracialStrategy.logSplitB {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (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 : ℝ} (hppos : 0 < p) (hm : D.card < n) (u : PostTuple n X Y A B D × X × Y) : S.flatQ R D μ w p u * Real.log (S.flatQ R D μ w p u / S.flatJB R D μ w p u) = S.flatQ R D μ w p u * Real.log (S.flatQ R D μ w p u * margY μ u.2.2 / (S.histY R D μ w p u.1 u.2.2 * μ u.2.1 u.2.2)) + S.flatQ R D μ w p u * Real.log (S.liveY R D μ w p u.1.1.i u.2.2 * ↑(n - D.card) / margY μ u.2.2)

The pointwise log split, Bob side.

theorem CommutingRepetition.TracialStrategy.logSumB_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)) {D : Finset (Fin n)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (hw1 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), w xw yw zA zB ≤ 1) (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 : ℝ} (hp : p = S.coreMass D μ w) (hppos : 0 < p) (hm : D.card < n) : ∑ u : PostTuple n X Y A B D × X × Y, S.flatQ R D μ w p u * Real.log (S.flatQ R D μ w p u / S.flatJB R D μ w p u) ≤ (3 * Real.log p⁻¹ + 2 * (↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B)))) / (↑n - ↑D.card)

The log-sum form of the Bob conjunct: the ℚ-weighted log-ratio against the defaultless J_B is at most (3t₀ + 2s₀)/m. Consumed at assembly (node 1.2.11) where the sampler's law dominates J_B up to a rounding factor.

theorem CommutingRepetition.TracialStrategy.klB_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)) {D : Finset (Fin n)} {Af Bf : Type} [Fintype Af] [Fintype Bf] {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (hw1 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), w xw yw zA zB ≤ 1) (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 : ℝ} (hp : p = S.coreMass D μ w) (hppos : 0 < p) (hm : D.card < n) : Pinsker.finiteRelativeEntropy (S.flatQ R D μ w p) (S.flatJB R D μ w p) ≤ (3 * Real.log p⁻¹ + 2 * (↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B)))) / (↑n - ↑D.card)

The Bob conjunct of history_relative_entropy: D(ℚ ‖ J_B) ≤ (3t₀ + 2s₀)/m.