Order prefixes (standalone form of the reverse-experiment

prefix sets)

def CommutingRepetition.ordPrefix {n : ℕ} {L : Finset (Fin n)} (π : Fin L.card ≃ ↥L) (j : ℕ) : Finset (Fin n)

The first j entries of an order of a block, as a set (the standalone form of AliceRevealDatum.revealPrefix / BobRevealDatum.revealPrefix, with a bare ℕ cut so that adjacent cuts share one definition).

Equations

• CommutingRepetition.ordPrefix π j = Finset.image (fun (t : Fin L.card) => ↑(π t)) {t : Fin L.card | ↑t < j}

theorem CommutingRepetition.ordPrefix_subset {n : ℕ} {L : Finset (Fin n)} (π : Fin L.card ≃ ↥L) (j : ℕ) : ordPrefix π j ⊆ L

theorem CommutingRepetition.ordPrefix_succ {n : ℕ} {L : Finset (Fin n)} (π : Fin L.card ≃ ↥L) (s : Fin L.card) : ordPrefix π (↑s + 1) = insert (↑(π s)) (ordPrefix π ↑s)

theorem CommutingRepetition.notMem_ordPrefix_self {n : ℕ} {L : Finset (Fin n)} (π : Fin L.card ≃ ↥L) (s : Fin L.card) : ↑(π s) ∉ ordPrefix π ↑s

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

theorem CommutingRepetition.sum_prod_mu_eq_one {n : ℕ} {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) : ∑ xw : Fin n → X, ∑ yw : Fin n → Y, ∏ j : Fin n, μ (xw j) (yw j) = 1

The full product prior over both question words has total mass one when the base law does.

Revealed-set effect facts

theorem CommutingRepetition.TracialStrategy.setEffectA_congr {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 R₀ : Finset (Fin n)) (μ : X → Y → ℝ) {x x' : Fin n → X} {y y' : Fin n → Y} (zA : Fin n → A) (hx : ∀ j ∈ R₀, x j = x' j) (hy : ∀ j ∉ R₀, y j = y' j) : S.setEffectA D R₀ μ x y zA = S.setEffectA D R₀ μ x' y' zA

setEffectA reads its xref only on the revealed set and its yref only off it.

theorem CommutingRepetition.TracialStrategy.setEffectB_congr {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 R₀ : Finset (Fin n)) (μ : X → Y → ℝ) {x x' : Fin n → X} {y y' : Fin n → Y} (zB : Fin n → B) (hx : ∀ j ∉ R₀, x j = x' j) (hy : ∀ j ∈ R₀, y j = y' j) : S.setEffectB D R₀ μ x y zB = S.setEffectB D R₀ μ x' y' zB

Mirror congruence for setEffectB.

theorem CommutingRepetition.TracialStrategy.setEffectA_univ {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 → ℝ) (x : Fin n → X) (y : Fin n → Y) (zA : Fin n → A) : S.setEffectA D Finset.univ μ x y zA = S.coreEffectA D x zA

At the fully revealed set the revealed-set effect is the core effect: the weight is the point mass at the reference word.

theorem CommutingRepetition.TracialStrategy.setEffectB_univ {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 → ℝ) (x : Fin n → X) (y : Fin n → Y) (zB : Fin n → B) : S.setEffectB D Finset.univ μ x y zB = S.coreEffectB D y zB

Mirror univ collapse for setEffectB.

theorem CommutingRepetition.TracialStrategy.re_pairing_weightedAvg_left {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)) {ι : Type u_1} [Fintype ι] (wgt : ι → ℝ) (f : ι → S.M.A) (K : S.M.A) : (S.M.τ (star S.σ * (weightedAvg wgt f * S.σ * K))).re = (∑ i : ι, wgt i)⁻¹ * ∑ i : ι, wgt i * (S.M.τ (star S.σ * (f i * S.σ * K))).re

Scalar expansion of a weightedAvg in the left slot of the trace pairing. Junk-safe through Lean's 0⁻¹ = 0.

theorem CommutingRepetition.TracialStrategy.re_pairing_weightedAvg_right {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)) {ι : Type u_1} [Fintype ι] (wgt : ι → ℝ) (f : ι → S.M.A) (H : S.M.A) : (S.M.τ (star S.σ * (H * S.σ * weightedAvg wgt f))).re = (∑ i : ι, wgt i)⁻¹ * ∑ i : ι, wgt i * (S.M.τ (star S.σ * (H * S.σ * f i))).re

Scalar expansion of a weightedAvg in the right slot.

noncomputable def CommutingRepetition.TracialStrategy.pairSum {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)) (D : Finset (Fin n)) (μ : X → Y → ℝ) (W : (Fin n → X) → (Fin n → Y) → ℝ) (zAf : Fin n → A) (zBf : Fin n → B) (SA SB : Finset (Fin n)) : ℝ

The D-measurable-weighted prior pairing of the two revealed-set effects at a pair of revealed sets. The covering-pair tower collapse (pairSum_eq_core below) states its independence of the sets.

Equations

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

theorem CommutingRepetition.TracialStrategy.pairSum_insertA {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) → ℝ) (hWx : ∀ (x x' : Fin n → X) (y : Fin n → Y), agreesOn D x x' → W x y = W x' y) (zAf : Fin n → A) (zBf : Fin n → B) (SA SB : Finset (Fin n)) (hDA : D ⊆ SA) (c : Fin n) (hcA : c ∉ SA) (hcB : c ∈ SB) : S.pairSum D μ W zAf zBf SA SB = S.pairSum D μ W zAf zBf (insert c SA) SB

One tower step on the Alice side: revealing one more coordinate to Alice does not change the prior pairing, provided the coordinate is already revealed to Bob.

theorem CommutingRepetition.TracialStrategy.pairSum_insertB {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) → ℝ) (hWy : ∀ (x : Fin n → X) (y y' : Fin n → Y), agreesOn D y y' → W x y = W x y') (zAf : Fin n → A) (zBf : Fin n → B) (SA SB : Finset (Fin n)) (hDB : D ⊆ SB) (c : Fin n) (hcB : c ∉ SB) (hcA : c ∈ SA) : S.pairSum D μ W zAf zBf SA SB = S.pairSum D μ W zAf zBf SA (insert c SB)

One tower step on the Bob side (mirror).

theorem CommutingRepetition.TracialStrategy.pairSum_eq_core {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) → ℝ) (hWx : ∀ (x x' : Fin n → X) (y : Fin n → Y), agreesOn D x x' → W x y = W x' y) (hWy : ∀ (x : Fin n → X) (y y' : Fin n → Y), agreesOn D y y' → W x y = W x y') (zAf : Fin n → A) (zBf : Fin n → B) (SA SB : Finset (Fin n)) (hDA : D ⊆ SA) (hDB : D ⊆ SB) (hcov : SA ∪ SB = Finset.univ) : S.pairSum D μ W zAf zBf SA SB = ∑ xw : Fin n → X, ∑ yw : Fin n → Y, (∏ j : Fin n, μ (xw j) (yw j)) * (W xw yw * (S.M.τ (star S.σ * (S.coreEffectA D xw zAf * S.σ * S.coreEffectB D yw zBf))).re)

The covering-pair tower collapse: for any pair of revealed sets containing the core and jointly covering every coordinate, the D-measurable-weighted prior pairing of the revealed-set effects equals the corresponding core-effect pairing (eq p-q-m through the tower property; the general form of the review-#15 trap-5 telescope).

The core-mass normalization bound

theorem CommutingRepetition.TracialStrategy.sum_coreEffectA_ext {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)) (xw : Fin n → X) (ext : (↥D → A) → Fin n → A) (hext : ∀ (zD : ↥D → A) (j : Fin n) (hj : j ∈ D), ext zD j = zD ⟨j, hj⟩) : ∑ zD : ↥D → A, S.coreEffectA D xw (ext zD) = 1

The core answer assignments tile the full answer words: summing the core effect over every core assignment (canonically extended) recovers the POVM total.

theorem CommutingRepetition.TracialStrategy.sum_coreEffectB_ext {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)) (yw : Fin n → Y) (ext : (↥D → B) → Fin n → B) (hext : ∀ (zD : ↥D → B) (j : Fin n) (hj : j ∈ D), ext zD j = zD ⟨j, hj⟩) : ∑ zD : ↥D → B, S.coreEffectB D yw (ext zD) = 1

Mirror tiling for Bob.

theorem CommutingRepetition.TracialStrategy.coreMass_raw_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)) (μ : 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) (extA : (↥D → A) → Fin n → A) (hextA : ∀ (zD : ↥D → A) (j : Fin n) (hj : j ∈ D), extA zD j = zD ⟨j, hj⟩) (extB : (↥D → B) → Fin n → B) (hextB : ∀ (zD : ↥D → B) (j : Fin n) (hj : j ∈ D), extB zD j = zD ⟨j, hj⟩) : ∑ 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.M.τ (star S.σ * (S.coreEffectA D xw (extA zD.1) * S.σ * S.coreEffectB D yw (extB zD.2)))).re ≤ 1

The weighted core mass is at most one (needed to give the alignment bound's right side its sign): with a [0,1]-valued weight, the weighted core-correlation mass is at most τ(σ*σ) = 1.

Canonical label builders

Local copies of the Costs.lean canonicalization maps (keepOn, keepOff, extendCoreA/B, aLabel, bLabel), with definitionally identical bodies, so that the alignment-bound helpers below can be stated before Costs.lean elaborates; the bridge in Costs.lean is rfl.

noncomputable def CommutingRepetition.mkKeepOn {n : ℕ} {α : Type} [Nonempty α] (R₀ : Finset (Fin n)) (wd : Fin n → α) : Fin n → α

Local copy of keepOn (definitionally equal).

Equations

• CommutingRepetition.mkKeepOn R₀ wd j = if j ∈ R₀ then wd j else Classical.arbitrary α

noncomputable def CommutingRepetition.mkKeepOff {n : ℕ} {α : Type} [Nonempty α] (R₀ : Finset (Fin n)) (wd : Fin n → α) : Fin n → α

Local copy of keepOff (definitionally equal).

Equations

• CommutingRepetition.mkKeepOff R₀ wd j = if j ∈ R₀ then Classical.arbitrary α else wd j

noncomputable def CommutingRepetition.mkExtA {n : ℕ} {A : Type} [Nonempty A] (D : Finset (Fin n)) (zD : ↥D → A) : Fin n → A

Local copy of extendCoreA (definitionally equal).

Equations

• CommutingRepetition.mkExtA D zD j = if h : j ∈ D then zD ⟨j, h⟩ else Classical.arbitrary A

noncomputable def CommutingRepetition.mkExtB {n : ℕ} {B : Type} [Nonempty B] (D : Finset (Fin n)) (zD : ↥D → B) : Fin n → B

Local copy of extendCoreB (definitionally equal).

Equations

• CommutingRepetition.mkExtB D zD j = if h : j ∈ D then zD ⟨j, h⟩ else Classical.arbitrary B

noncomputable def CommutingRepetition.mkALabel {n : ℕ} {X Y A : Type} [Nonempty X] [Nonempty Y] [Nonempty A] (D R₀ : Finset (Fin n)) (xw : Fin n → X) (yw : Fin n → Y) (zD : ↥D → A) : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → A)

Local copy of the canonical Alice label aLabel (definitionally equal; the codomain is the unfolding of the ALabel abbreviation).

Equations

• CommutingRepetition.mkALabel D R₀ xw yw zD = (R₀, CommutingRepetition.mkKeepOn R₀ xw, CommutingRepetition.mkKeepOff R₀ yw, CommutingRepetition.mkExtA D zD)

noncomputable def CommutingRepetition.mkBLabel {n : ℕ} {X Y B : Type} [Nonempty X] [Nonempty Y] [Nonempty B] (D R₀ : Finset (Fin n)) (xw : Fin n → X) (yw : Fin n → Y) (zD : ↥D → B) : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → B)

Local copy of the canonical Bob label bLabel (definitionally equal).

Equations

• CommutingRepetition.mkBLabel D R₀ xw yw zD = (R₀, CommutingRepetition.mkKeepOff R₀ xw, CommutingRepetition.mkKeepOn R₀ yw, CommutingRepetition.mkExtB D zD)

theorem CommutingRepetition.mkKeepOn_eq_on {n : ℕ} {α : Type} [Nonempty α] (R₀ : Finset (Fin n)) (wd : Fin n → α) {j : Fin n} (hj : j ∈ R₀) : mkKeepOn R₀ wd j = wd j

theorem CommutingRepetition.mkKeepOff_eq_off {n : ℕ} {α : Type} [Nonempty α] (R₀ : Finset (Fin n)) (wd : Fin n → α) {j : Fin n} (hj : j ∉ R₀) : mkKeepOff R₀ wd j = wd j

theorem CommutingRepetition.mkALabel_congr {n : ℕ} {X Y A : Type} [Fintype X] [Fintype Y] [Fintype A] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [Nonempty X] [Nonempty Y] [Nonempty A] (D R₀ : Finset (Fin n)) {xw xw' : Fin n → X} {yw yw' : Fin n → Y} (zD : ↥D → A) (hx : ∀ j ∈ R₀, xw j = xw' j) (hy : ∀ j ∉ R₀, yw j = yw' j) : mkALabel D R₀ xw yw zD = mkALabel D R₀ xw' yw' zD

The Alice label reads its xw only on R₀ and its yw only off R₀.

theorem CommutingRepetition.mkBLabel_congr {n : ℕ} {X Y B : Type} [Fintype X] [Fintype Y] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty B] (D R₀ : Finset (Fin n)) {xw xw' : Fin n → X} {yw yw' : Fin n → Y} (zD : ↥D → B) (hx : ∀ j ∉ R₀, xw j = xw' j) (hy : ∀ j ∈ R₀, yw j = yw' j) : mkBLabel D R₀ xw yw zD = mkBLabel D R₀ xw' yw' zD

The Bob label reads its xw only off R₀ and its yw only on R₀.

Weight positivity, effect positivity, canonical reads

theorem CommutingRepetition.setWeightX_nonneg {n : ℕ} {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] [Nonempty X] [Nonempty Y] (S₀ : Finset (Fin n)) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (xref : Fin n → X) (yref : Fin n → Y) (w : Fin n → X) : 0 ≤ setWeightX S₀ μ xref yref w

theorem CommutingRepetition.setWeightY_nonneg {n : ℕ} {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] [Nonempty X] [Nonempty Y] (S₀ : Finset (Fin n)) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (xref : Fin n → X) (yref v : Fin n → Y) : 0 ≤ setWeightY S₀ μ xref yref v

theorem CommutingRepetition.TracialStrategy.setEffectA_isPosElem {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 R₀ : Finset (Fin n)) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (xref : Fin n → X) (yref : Fin n → Y) (zA : Fin n → A) : IsPosElem (S.setEffectA D R₀ μ xref yref zA)

Revealed-set effects are algebraically positive (Alice).

theorem CommutingRepetition.TracialStrategy.setEffectB_isPosElem {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 R₀ : Finset (Fin n)) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (xref : Fin n → X) (yref : Fin n → Y) (zB : Fin n → B) : IsPosElem (S.setEffectB D R₀ μ xref yref zB)

Revealed-set effects are algebraically positive (Bob).

theorem CommutingRepetition.TracialStrategy.setEffectA_canon {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 R₀ : Finset (Fin n)) (μ : X → Y → ℝ) (xw : Fin n → X) (yw : Fin n → Y) (zA : Fin n → A) : S.setEffectA D R₀ μ (mkKeepOn R₀ xw) (mkKeepOff R₀ yw) zA = S.setEffectA D R₀ μ xw yw zA

Canonicalized reference words read back to the raw words (Alice).

theorem CommutingRepetition.TracialStrategy.setEffectB_canon {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 R₀ : Finset (Fin n)) (μ : X → Y → ℝ) (xw : Fin n → X) (yw : Fin n → Y) (zB : Fin n → B) : S.setEffectB D R₀ μ (mkKeepOff R₀ xw) (mkKeepOn R₀ yw) zB = S.setEffectB D R₀ μ xw yw zB

Canonicalized reference words read back to the raw words (Bob).

Word splitting along a coordinate block

def CommutingRepetition.wordSplit {n : ℕ} (L : Finset (Fin n)) (α : Type) : (Fin n → α) ≃ (↥L → α) × ({ j : Fin n // j ∉ L } → α)

Split a word into its values on a block L and off it.

Equations

• CommutingRepetition.wordSplit L α = Equiv.piEquivPiSubtypeProd (fun (j : Fin n) => j ∈ L) fun (x : Fin n) => α

theorem CommutingRepetition.wordSplit_symm_mem {n : ℕ} (L : Finset (Fin n)) (α : Type) (ω : ↥L → α) (g : { j : Fin n // j ∉ L } → α) {j : Fin n} (hj : j ∈ L) : (wordSplit L α).symm (ω, g) j = ω ⟨j, hj⟩

theorem CommutingRepetition.wordSplit_symm_notMem {n : ℕ} (L : Finset (Fin n)) (α : Type) (ω : ↥L → α) (g : { j : Fin n // j ∉ L } → α) {j : Fin n} (hj : j ∉ L) : (wordSplit L α).symm (ω, g) j = g ⟨j, hj⟩

theorem CommutingRepetition.sum_wordSplit {n : ℕ} {α : Type} [Fintype α] {V : Type u_1} [AddCommMonoid V] (L : Finset (Fin n)) (F : (Fin n → α) → V) : ∑ xw : Fin n → α, F xw = ∑ ω : ↥L → α, ∑ g : { j : Fin n // j ∉ L } → α, F ((wordSplit L α).symm (ω, g))

Reindex a word sum through the block split.

theorem CommutingRepetition.prod_wordSplit {n : ℕ} (L : Finset (Fin n)) (f : Fin n → ℝ) : ∏ j : Fin n, f j = (∏ c : ↥L, f ↑c) * ∏ c : { j : Fin n // j ∉ L }, f ↑c

Split a full-coordinate product along the block.

theorem CommutingRepetition.prod_mu_wordSplit {n : ℕ} {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] [Nonempty X] [Nonempty Y] (L : Finset (Fin n)) (μ : X → Y → ℝ) (yw : Fin n → Y) (ω : ↥L → X) (g : { j : Fin n // j ∉ L } → X) : ∏ j : Fin n, μ ((wordSplit L X).symm (ω, g) j) (yw j) = (∏ c : ↥L, μ (ω c) (yw ↑c)) * ∏ c : { j : Fin n // j ∉ L }, μ (g c) (yw ↑c)

The product prior through a split Alice word.

theorem CommutingRepetition.prod_mu_wordSplit' {n : ℕ} {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] [Nonempty X] [Nonempty Y] (L : Finset (Fin n)) (μ : X → Y → ℝ) (xw : Fin n → X) (ω : ↥L → Y) (g : { j : Fin n // j ∉ L } → Y) : ∏ j : Fin n, μ (xw j) ((wordSplit L Y).symm (ω, g) j) = (∏ c : ↥L, μ (xw ↑c) (ω c)) * ∏ c : { j : Fin n // j ∉ L }, μ (xw ↑c) (g c)

The product prior through a split Bob word (mirror).

theorem CommutingRepetition.sum_prod_pi_subtype {n : ℕ} {α : Type} [Fintype α] (L : Finset (Fin n)) (f : ↥L → α → ℝ) : ∑ ω : ↥L → α, ∏ c : ↥L, f c (ω c) = ∏ c : ↥L, ∑ v : α, f c v

Fubini for a product over a block: total conditional mass.