Documentation

MIPStarRE.LDT.Commutativity.Transport.FullSlice.Machinery.Marginalization.Core

Full-slice tensor marginalization core #

Collision residuals, postprocessing expansions, and tensor marginalization core bounds for the BABA and ABAB full-slice tensor averages.

Ex-private definitions are tensor-form machinery per architecture decision #713; downstream code should use the scalar public API exposed by the full-slice transport theorems.

References #

source
noncomputable def MIPStarRE.LDT.Commutativity.fullSliceABAByCollisionFactored {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (u : Point params) (xy : FullSliceQuestion params) :
Error

Factored collision residual for the y-marginalization tensor step.

Here the outer sandwich is the already x-evaluated family G^x_[g(u)=a], while the colliding polynomial pair is on the y side.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPStarRE.LDT.Commutativity.fullSliceBABA_tensor_marginalize_x_collision_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (hnorm : strategy.state.IsNormalized) :
    (avgOver (uniformDistribution (FullSliceQuestion params)) fun (xy : FullSliceQuestion params) => MIPStarRE.LDT.Commutativity.fullSliceBABAxCollisionFactored✝ params strategy family xy) ≤ ↑params.m * ↑params.d / ↑params.q

    Averaged x-collision bound in the form consumed by fullSliceBABA_tensor_marginalize_x.

    source
    theorem MIPStarRE.LDT.Commutativity.fullSliceABAB_tensor_marginalize_y_collision_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (hnorm : strategy.state.IsNormalized) :
    (avgOver (uniformDistribution (Point params × FullSliceQuestion params)) fun (ux : Point params × FullSliceQuestion params) => fullSliceABAByCollisionFactored params strategy family ux.1 ux.2) ≤ ↑params.m * ↑params.d / ↑params.q

    Averaged y-collision bound in the form consumed by fullSliceABAB_tensor_marginalize_y. This is the y-side analogue of fullSliceBABA_tensor_marginalize_x_collision_bound.

    source
    theorem MIPStarRE.LDT.Commutativity.avg_postprocess_sandwichTensor_eq_diag_add_collision {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} {σ : Type u_4} {κ : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [Fintype σ] [DecidableEq σ] [Nonempty σ] [Fintype κ] [DecidableEq κ] (ψ : QuantumState (ι × ι)) (A : SubMeas α ι) (B : SubMeas β ι) (eval : σ → α → κ) :
    (avgOver (uniformDistribution σ) fun (s : σ) => ∑ k : κ, ∑ b : β, ev ψ (leftTensor (B.outcome b * (postprocess A (eval s)).outcome k * B.outcome b) * rightTensor ((postprocess A (eval s)).outcome k))) = ∑ a : α, ∑ b : β, ev ψ (leftTensor (B.outcome b * A.outcome a * B.outcome b) * rightTensor (A.outcome a)) + ∑ aa : α × α, ∑ b : β, (if aa.1 = aa.2 then 0 else avgOver (uniformDistribution σ) fun (s : σ) => if eval s aa.1 = eval s aa.2 then 1 else 0) * ev ψ (leftTensor (B.outcome b * A.outcome aa.1 * B.outcome b) * rightTensor (A.outcome aa.2))

    Expand one postprocessed tensor sandwich and split the resulting pair sum into its diagonal part and off-diagonal collision residual.

    This is the common finite-sum identity behind both tensor marginalization steps. The outcome family A is postprocessed by the sample-dependent map eval s; the outer sandwich family B is not postprocessed.

    source
    theorem MIPStarRE.LDT.Commutativity.fullSliceABAByCollisionFactored_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (u : Point params) (xy : FullSliceQuestion params) :
    0 ≤ fullSliceABAByCollisionFactored params strategy family u xy

    The y-collision residual is nonnegative term-by-term.

    source
    theorem MIPStarRE.LDT.Commutativity.fullSliceBABA_tensor_marginalize_x {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (hnorm : strategy.state.IsNormalized) :
    |fullSliceBABAtensorAvg params strategy family - xEvaluatedSliceBABAtensorAvg params strategy family| ≤ ↑params.m * ↑params.d / ↑params.q

    X-side tensor marginalization bound for paper eq:gcom4-diff.

    This staged statement compares the full BAB ⊗ A tensor average to the intermediate where only the x polynomial outcome has been evaluated at u. It is the Lean-local tensor form of the Schwartz-Zippel step labelled eq:gcom4-diff in the proof of blueprint theorem thm:com-main.