Documentation

MIPRE.Background.LIDT.Co.Commutativity.ScalarApproximation.PaperChainBasic.Reindexing

Section 11 commutativity: reindexing utilities for the evaluated-slice paper chain #

Finite-reindexing and evaluated-family identities used by the paper-faithful scalar approximation chain: the counterpart of Commutativity/ScalarApproximation/PaperChainBasic/Reindexing.lean under MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The two evaluated-family identities are state-free and hold over any C*-algebra 𝔓 with its order. ev_leftTensor_mul_middle_finset_sum takes the symmetric model S where the vendored lemma takes the state ψ, in the same position, and is stated with S.L and S.R; its proof is the keystone's leftTensor_finset_sum and ev_finset_sum.

Not ported #

Every declaration of the vendored file has a counterpart here.

References #

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

source
theorem MIPRE.LIDT.Co.Commutativity.evaluatedPointFamily_total_eq_G_total {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hG : ∀ (x : MIPStarRE.LDT.Fq params), G x = (family.meas x).toSubMeas) (u : MIPStarRE.LDT.Point params.next) :
(evaluatedPointFamily params family u).total = (G (MIPStarRE.LDT.pointHeight params u)).total

The evaluated point family has the same total as the underlying slice measurement G at the sampled height.

This unfolds evaluatedPointFamily as postprocessing of family.meas y; the postprocessing total is unchanged, and hG identifies the slice with G y.

source
theorem MIPRE.LIDT.Co.Commutativity.ev_leftTensor_mul_middle_finset_sum {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} (s : Finset α) (S : SymModel 𝔓 K) (A C R D : 𝔓) (B : α → 𝔓) :
S.ev (S.L ((A * ∑ x ∈ s, B x) * C * R) * S.R D) = ∑ x ∈ s, S.ev (S.L (A * B x * C * R) * S.R D)

Expand a finite sum in the middle factor of a left-register sandwich: ⟹L(A (∑_x B_x) C R) R(D)⟩ = ∑_x ⟹L(A B_x C R) R(D)⟩.

source
theorem MIPRE.LIDT.Co.Commutativity.evaluatedPointFamily_appendPoint_outcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hG : ∀ (x : MIPStarRE.LDT.Fq params), G x = (family.meas x).toSubMeas) (x : MIPStarRE.LDT.Fq params) (u : MIPStarRE.LDT.Point params) (a : MIPStarRE.LDT.Fq params) :
(evaluatedPointFamily params family (MIPStarRE.LDT.appendPoint params u x)).outcome a = ∑ g : MIPStarRE.LDT.Polynomial params with g.toFun u = a, (G x).outcome g

Evaluating the slice family at an appended point is postprocessing the slice measurement by the fiber {g | g u = a}.