Documentation

MIPRE.Background.LIDT.Co.Commutativity.GCommStability.Scalar.RawSecond

Section 11 commutativity: raw second scalar stability bound #

The raw uncollapsed form of the second scalar stability estimate: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/GCommStability/Scalar/RawSecond.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The raw defect is stated with the placements strategy.state.L and strategy.state.R, and the two helpers avgOver_right_linear and sum_ev_leftTensor_mul_rightTensor_const take the symmetric model S where the vendored ones take the state ψ, in the same position. The vendored hypothesis hnorm : strategy.state.IsNormalized of gCommStabilityTwo_raw_scalar_pointwise_bound and gCommStabilityTwo_raw_scalar is dropped, as the port conventions drop hψ : ψ.IsNormalized: the first Cauchy–Schwarz factor is bounded through VecState.ev_one_of_isNormalized, which takes no hypothesis. Callers omit that argument, which stood between zeta and family.

The proofs are shorter than the vendored ones. Self-adjointness through Matrix.PosSemidef is IsSelfAdjoint.of_nonneg; the Kronecker computations of the Cauchy–Schwarz factors are the keystone's conjTranspose_opTensor and opTensor_mul, and their positivity and monotonicity opTensor_nonneg, opTensor_mono_left and opTensor_mono_right. The inner bound of gCommStabilityTwo_raw_left_sum_le is the total bound of sandwichByOuterSubMeas, reindexed by Equiv.prodComm, and avgOver_right_linear pulls the average through the right placement with ev_opTensor_averageOperatorOverDistribution_right.

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.avgOver_right_linear {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {U : Type u_3} {Γ : Type u_4} {Aidx : Type u_5} [Fintype Γ] [Fintype Aidx] (𝒟U : MIPStarRE.LDT.Distribution U) (S : SymModel 𝔓 K) (L : Γ → Aidx → 𝔓) (P : Aidx → 𝔓) (Q : U → Γ → 𝔓) :
(MIPStarRE.LDT.avgOver 𝒟U fun (u : U) => ∑ g : Γ, ∑ a : Aidx, S.ev (S.L (L g a) * S.R (P a * Q u g))) = ∑ g : Γ, ∑ a : Aidx, S.ev (S.L (L g a) * S.R (P a * averageOperatorOverDistribution 𝒟U fun (u : U) => Q u g))

Averaging over u commutes with the finite sums and passes into the right placement: E_u ∑_{g,a} ⟨L_{g,a} ⊗ P_a Q_{u,g}⟩ = ∑_{g,a} ⟨L_{g,a} ⊗ P_a (E_u Q_{u,g})⟩.

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

A finite sum of left placements against a fixed right placement collapses into the left factor.

source
noncomputable def MIPRE.LIDT.Co.Commutativity.gCommStabilityTwoRawScalarDefect {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (x : MIPStarRE.LDT.Fq params) :
ℝ

Raw uncollapsed scalar defect for the paper's second G-commutativity stability estimate after the right-register point-product swap.

For fixed slice height x, this is the expression from commutativity-G.tex, clm:g-comm-stability2, before collapsing the (v,y), b-average into gCommStabilityTwoR. The left register contains G^x_g B^{v,y}_b (1-G^x), while the right register contains the swapped point product P^{v,y}_b P^{u,x}_{g(u)}.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.LIDT.Co.Commutativity.gCommStabilityTwo_raw_left_sum_le {𝔓 : 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) (vy : MIPStarRE.LDT.Point params.next) :
    ∑ gb : MIPStarRE.LDT.Polynomial params × MIPStarRE.LDT.Fq params, (1 - (G x).total) * ((evaluatedPointFamily params family vy).outcome gb.2 * (G x).outcome gb.1 * (evaluatedPointFamily params family vy).outcome gb.2) * (1 - (G x).total) ≤ 1 - (G x).total

    The left-register sandwiches of the raw second defect sum to at most 1 - G^x: ∑_{g,b} (1 - G^x) B_b G^x_g B_b (1 - G^x) ≤ 1 - G^x for projective G^x.

    source
    theorem MIPRE.LIDT.Co.Commutativity.gCommStabilityTwo_raw_scalar_pointwise_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (zeta : ℝ) (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) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (x : MIPStarRE.LDT.Fq params) :
    |gCommStabilityTwoRawScalarDefect params strategy family G x| ≤ √(hbound.storedResidual G x)

    Pointwise Cauchy–Schwarz bound for the raw second scalar defect: |raw defect at x| ≤ √⟨Ψ, (1 - G^x) ⊗ Z^x Ψ⟩.

    source
    theorem MIPRE.LIDT.Co.Commutativity.gCommStabilityTwo_raw_scalar {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (zeta : ℝ) (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) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) :
    |MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) (gCommStabilityTwoRawScalarDefect params strategy family G)| ≤ √zeta

    Raw paper form of the second scalar G-commutativity stability estimate.

    This bounds the uncollapsed post-swap defect used in the paper line-87 removal: the defect still averages over (v,y), u, g, b rather than first packaging the left-register sandwich as gCommStabilityTwoR. The vendored theorem asks for a normalized state.