Order prefixes: the full block and position sums

theorem CommutingRepetition.ordPrefix_card {n : ℕ} {L : Finset (Fin n)} (π : Fin L.card ≃ ↥L) : ordPrefix π L.card = L

theorem CommutingRepetition.sum_ordPositions {n : ℕ} {L : Finset (Fin n)} (π : Fin L.card ≃ ↥L) (f : Fin n → ℝ) : ∑ k : Fin L.card, f ↑(π k) = ∑ j ∈ L, f j

A sum over the positions of an order is a sum over the block.

theorem CommutingRepetition.AliceBase.SA_union_LYp {n : ℕ} {D : Finset (Fin n)} (b : AliceBase n D) : b.SA ∪ b.LYp = Finset.univ

theorem CommutingRepetition.AliceBase.SB_sdiff_SA {n : ℕ} {D : Finset (Fin n)} (b : AliceBase n D) : b.SB \ b.SA = b.LYp

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

The Alice question marginal μ_X.

Equations

• CommutingRepetition.TracialStrategy.margX μ x = ∑ y : Y, μ x y

theorem CommutingRepetition.TracialStrategy.margX_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) (x : X) : 0 ≤ margX μ x

theorem CommutingRepetition.TracialStrategy.mu_le_margX {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 ≤ margX μ x

theorem CommutingRepetition.TracialStrategy.sum_margX {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) : ∑ x : X, margX μ x = 1

The Bob-block conditional bound (eqs bob-block-conditioning-budget,

bob-block-chain-rule)

theorem CommutingRepetition.TracialStrategy.sum_prodPrior {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)} (μ : X → Y → ℝ) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) : ∑ s : CoreTuple n X Y A B D, prodPrior D μ s = (↑(Fintype.card A) * ↑(Fintype.card B)) ^ D.card

The total prior mass over core tuples is the number of core words.

theorem CommutingRepetition.TracialStrategy.cardZ_pos {n : ℕ} {A B : Type} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {D : Finset (Fin n)} : 0 < (↑(Fintype.card A) * ↑(Fintype.card B)) ^ D.card

theorem CommutingRepetition.TracialStrategy.blockBound {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 = SX \ SY) (π : Fin L.card ≃ ↥L) : ∑ s : CoreTuple n X Y A B D, S.corePost D μ w p s * (Real.log (classMass SX Finset.univ (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)) / margX μ (s.1 ↑(π k)))) ≤ Real.log p⁻¹ + ↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B))

The block conditional bound: at a fixed Alice set SX and a Bob background SY covering the rest, the core-posterior expectation of the log-ratio of the class masses at the full Bob word against the background, minus the product-prior conditional, is at most t₀ + s₀ — the chain rule D(ℚ⁰_{class} ‖ P_{class}) − D(ℚ⁰_{background} ‖ P_{background}), the first term bounded pointwise by log(1/p) and the second by Gibbs.

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

noncomputable def CommutingRepetition.TracialStrategy.histLogA {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 second chain term at datum r: log ℚ⁰(y_i ∣ X_{{i}∪C_X}, Y_{C_Y}, Z) − log μ(y_i ∣ x_i).

Equations

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

theorem CommutingRepetition.TracialStrategy.cutSumHist_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.SB (b.SA ∪ ordPrefix b.πY (↑k + 1)) (S.corePost D μ w p) s / classMass b.SB (b.SA ∪ ordPrefix b.πY ↑k) (S.corePost D μ w p) s) - Real.log (μ (s.1 ↑(b.πY k)) (s.2.1 ↑(b.πY k)) / margX μ (s.1 ↑(b.πY k)))) ≤ Real.log p⁻¹ + ↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B))

Per-base telescoped bound (eq bob-block-chain-rule): at a fixed Bob base the cut sum of the conditional log-ratios telescopes to the full-block conditional, bounded by t₀ + s₀.

theorem CommutingRepetition.TracialStrategy.secondTermA_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.histLogA μ w p r s ≤ 2 * (Real.log p⁻¹ + ↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B))) / (↑n - ↑D.card)

The second chain term is at most 2(t₀ + s₀)/m (eqs bob-block-conditioning-budget through second-history-chain-term): the reveal datum re-read as (Bob base, interior cut), the size-biased law (2/m)·β, the cut sum telescoped per base.

The flattened laws: histories, live marginals, and the first chain

term

noncomputable def CommutingRepetition.TracialStrategy.histX {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) (x : X) : ℝ

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

Equations

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

noncomputable def CommutingRepetition.TracialStrategy.liveX {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) (x : X) : ℝ

ℚ(i, X_i = x) = ∑_{h : h.i = i} ℚ(h, x).

Equations

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

theorem CommutingRepetition.TracialStrategy.condQA_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) (x : X) (h : PostTuple n X Y A B D) : S.condQA R D μ w p i₀ x h = if h.1.i = i₀ then S.histX R D μ w p h x / S.liveX R D μ w p i₀ x else 0

theorem CommutingRepetition.TracialStrategy.flatJA_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.flatJA R D μ w p u = (↑(n - D.card))⁻¹ * μ u.2.1 u.2.2 * (S.histX R D μ w p u.1 u.2.1 / S.liveX R D μ w p u.1.1.i u.2.1)

theorem CommutingRepetition.TracialStrategy.histX_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) (x : X) : 0 ≤ S.histX R D μ w p h x

theorem CommutingRepetition.TracialStrategy.flatQ_le_histX {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.histX R D μ w p h x

theorem CommutingRepetition.TracialStrategy.liveX_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) (x : X) : 0 ≤ S.liveX R D μ w p i₀ x

theorem CommutingRepetition.TracialStrategy.histX_le_liveX {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) : S.histX R D μ w p h x ≤ S.liveX R D μ w p h.1.i x

theorem CommutingRepetition.TracialStrategy.liveX_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) (x : X) : S.liveX R D μ w p i₀ x = 0

Live-coordinate mass vanishes on the core.

theorem CommutingRepetition.TracialStrategy.sum_flatQ_group {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 → X → ℝ) : ∑ u : PostTuple n X Y A B D × X × Y, S.flatQ R D μ w p u * F u.1.1.i u.2.1 = ∑ i₀ : Fin n, ∑ x : X, S.liveX R D μ w p i₀ x * F i₀ x

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

noncomputable def CommutingRepetition.TracialStrategy.coreMargX {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 : ℝ) (xw : Fin n → X) : ℝ

The Alice question marginal of the core posterior.

Equations

• S.coreMargX μ w p xw = ∑ q : (Fin n → Y) × (↥D → A) × (↥D → B), S.corePost D μ w p (xw, q)

theorem CommutingRepetition.TracialStrategy.coreMargX_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) (xw : Fin n → X) : 0 ≤ S.coreMargX μ w p xw

theorem CommutingRepetition.TracialStrategy.sum_coreMargX {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) : ∑ xw : Fin n → X, S.coreMargX μ w p xw = 1

theorem CommutingRepetition.TracialStrategy.coreMargX_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) (xw : Fin n → X) : S.coreMargX μ w p xw ≤ p⁻¹ * ∏ j : Fin n, margX μ (xw j)

ℚ⁰_X ≤ p⁻¹ · μ_X^{⊗n} (the conditioning budget for the question marginal).

theorem CommutingRepetition.TracialStrategy.sum_corePost_coord {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) (x : X) : (∑ s : CoreTuple n X Y A B D, if s.1 i₀ = x then S.corePost D μ w p s else 0) = HistoryKL.coordMarginal (S.coreMargX μ w p) i₀ x

The core marginal at a coordinate, as a coordinate marginal of ℚ⁰_X.

theorem CommutingRepetition.TracialStrategy.firstTermA_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.liveX R D μ w p u.1.1.i u.2.1 * ↑(n - D.card) / margX μ u.2.1) ≤ Real.log p⁻¹ / (↑n - ↑D.card)

The first chain term is at most t₀/m (eq first-history-chain-term): the live marginal is m⁻¹ times the core question marginal, and the marginals tensorize against μ_X.

theorem CommutingRepetition.TracialStrategy.secondTermA_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 * margX μ u.2.1 / (S.histX R D μ w p u.1 u.2.1 * μ 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.histLogA μ w p r s

The second chain term in core form: the ℚ-expectation of log(ℚ(h,x,y) μ_X(x) / (ℚ(h,x) μ(x,y))) is the reveal-law average of the core integrand histLogA.

The Alice conjunct: absolute continuity, subnormalization, log split

theorem CommutingRepetition.TracialStrategy.flatJA_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.flatJA R D μ w p u

theorem CommutingRepetition.TracialStrategy.flatQ_eq_zero_of_mu {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 : ℝ) (u : PostTuple n X Y A B D × X × Y) (hu : μ u.2.1 u.2.2 = 0) : S.flatQ R D μ w p u = 0

A vanishing live-question factor kills the flattened posterior.

theorem CommutingRepetition.TracialStrategy.flatQ_eq_zero_of_flatJA {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.flatJA R D μ w p u = 0) : S.flatQ R D μ w p u = 0

theorem CommutingRepetition.TracialStrategy.sum_flatJA_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.flatJA R D μ w p u ≤ 1

J_A is subnormalized: its total mass is m⁻¹ ∑_x μ_X(x) · #{i ∉ D : ℚ(i, x) > 0} ≤ 1.

theorem CommutingRepetition.TracialStrategy.logSplitA {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.flatJA R D μ w p u) = S.flatQ R D μ w p u * Real.log (S.flatQ R D μ w p u * margX μ u.2.1 / (S.histX R D μ w p u.1 u.2.1 * μ u.2.1 u.2.2)) + S.flatQ R D μ w p u * Real.log (S.liveX R D μ w p u.1.1.i u.2.1 * ↑(n - D.card) / margX μ u.2.1)

The pointwise log split (eq JA-chain-rule): log(ℚ/J_A) is the conditional live-answer term plus the live-question term.

theorem CommutingRepetition.TracialStrategy.logSumA_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.flatJA 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 Alice conjunct: the ℚ-weighted log-ratio against the defaultless J_A is at most (3t₀ + 2s₀)/m. Consumed at assembly (node 1.2.11) where the sampler's law dominates J_A up to a rounding factor.

theorem CommutingRepetition.TracialStrategy.klA_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.flatJA R D μ w p) ≤ (3 * Real.log p⁻¹ + 2 * (↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B)))) / (↑n - ↑D.card)

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