Helper strong self-consistency bounds: post-delete transports #
Post-delete-an-A transport lemmas culminating in the moved-quantity bound used before the
residual-chain assembly: the counterpart of the vendored
SelfImprovement/Theorems/Results/HelperSSC/PostDeleteA.lean (under
MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10,
section "Port conventions").
Contents #
helper_pair_sandwich_operator_sum_le:∑_{h,h'} (X_h H_{h'} X_h) ⊗ T_h ≤ ∑_h X_h² ⊗ T_hfor self-adjointX_h, andhelper_pair_tensor_mass_le_one:∑_{h,h'} ev(H_{h'} ⊗ T_h) ≤ 1.- The two factors of the
eq:swap-u-for-v-attack-of-the-clonesCauchy--Schwarz bound:helperDeleteA_clone_variance_factor_le_globalVarianceDeviation_sumandhelperDeleteA_clone_mass_factor_le_one, and the bound itself,helperDeleteAQuantity_abs_sub_clonedQuantity_le_sqrt. helper_moveOverV_C_contractionand theeq:move-over-vboundhelperDeleteAClonedQuantity_abs_sub_moveOverVQuantity_le_sqrt_two_delta.
A strategy is a SymStrat params 𝔓 K; the polynomial submeasurement T, the sandwiched
submeasurement H^u and the point projectors live in 𝔓, and every scalar is
strategy.state.ev of a joint operator strategy.state.opTensor X Y; leftTensor and
rightTensor are strategy.state.L and strategy.state.R, and Xᴴ is star X. The vendored
helper_pair_sandwich_operator_sum_le names no state, its opTensor being the Kronecker product
on the carrier; here it takes the model (S : SymModel 𝔓 K) as an explicit first argument, as Co
AddInUStep34AndTransfer/Selected's addInU_selected_sandwich_tensor_if_sum_le does, and its
hypothesis (X h)ᴴ = X h is star (X h) = X h.
Global variance. The variance factor is bounded by M6's summed deviation
∑_g globalVarianceDeviationAtPolynomial params strategy strategy.state T g (Co
GlobalVariance/Defs/Families), the independent-points variance of the family
u ↦ S.L (A^u_{g(u)}) * S.R √T_g on strategy.state itself rather than the vendored weighted
state; it is identified through Co weightedPointConditionedOperator_sq, exactly where the
vendored proof rewrites with its vendored counterpart, so the statement keeps its vendored text.
Placement bounds. The two operator bounds ∑_{h,h'} H_{h'} ⊗ T_h = H.total ⊗ T.total ≤ 1 of
helper_pair_tensor_mass_le_one and helper_moveOverV_C_contraction, which the vendored file
proves twice through opTensor_le_leftTensor and leftTensor_le_one (ι₂ := ι), are the private
pair_opTensor_sum_le_one, closed by the keystone's S.opTensor_le_one.
Proofs that differ from the vendored ones.
- The nine Hermitian computations (
Matrix.conjTranspose_sub,Matrix.conjTranspose_mul,Matrix.conjTranspose_sum,Matrix.star_eq_conjTranspose,leftTensor_conjTranspose,rightTensor_conjTransposewithSubMeas.outcome_hermitian) areIsSelfAdjoint.of_nonnegof the keystone's positivity,IsSelfAdjoint.subandstar_mul; the positivity of(A^u - A^v) H (A^u - A^v)throughstar_left_conjugate_nonnegisIsSelfAdjoint.conjugate_nonneg. helperDeleteAQuantity_abs_sub_clonedQuantity_le_sqrtapplies the sandwich Cauchy--SchwarzS.ev_opTensor_sandwich_abs_le_sqrtwithX = 1,Y = A^u - A^von the differenceev((H (A^u - A^v)) ⊗ T), where the vendored proof takesX = A^u - A^v,Y = 1after conjugating it toev(((A^u - A^v) H) ⊗ T); the conjugation step disappears, the two factors come in the other order, and the closing absorption is the importedaddInU_le_sqrt_of_factor_bounds_leftin place of…_right.- In
helperDeleteAClonedQuantity_abs_sub_moveOverVQuantity_le_sqrt_two_deltathe collapse of∑_a ∑_{(h,h')}onto the fibrea = h(v)is the privatesum_fiber_collapse_pair(the vendoredhAvg), and the self-consistency input is passed to the CoPreliminaries.closenessOfInnerProduct_rightas CoAddInUStep12/Rawdoes.
Dropped hypotheses. The vendored helper_pair_tensor_mass_le_one closes with
ev_one_of_isNormalized strategy.state strategy.isNormalized (vendored line 113), and the vendored
helperDeleteAClonedQuantity_abs_sub_moveOverVQuantity_le_sqrt_two_delta passes
strategy.isNormalized to closenessOfInnerProduct_right (vendored line 607); here
strategy.state.ev_one_of_isNormalized and the ported Cauchy--Schwarz bound take no hypothesis.
No statement of the vendored file carries a swap, density or normalization hypothesis, so no
statement changed beyond the translation. The file sets no option, the vendored file-wide
respectTransparency false not being needed.
Not ported #
Every declaration of the vendored file has a counterpart here.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/self_improvement.texblueprint/src/chapter/ch07_self_improvement.tex
Post-delete-an-A transports #
The pair sandwich ∑_{(h, h')} (X_h H_{h'} X_h) ⊗ T_h is at most ∑_h X_h² ⊗ T_h for
self-adjoint X_h: summing over h' gives H.total ≤ 1.
The pair mass ∑_{(h, h')} ev(H_{h'} ⊗ T_h) of two submeasurements is at most 1.
The variance factor of eq:swap-u-for-v-attack-of-the-clones is at most the summed
global-variance deviation: the sandwich (A^u - A^v) H^u_{h'} (A^u - A^v) is dominated by
(A^u - A^v)² after summing over h', and averaging over independent points gives the
deviation.
The mass factor of eq:swap-u-for-v-attack-of-the-clones is at most 1.
Paper eq:swap-u-for-v-attack-of-the-clones: after delete-an-A, the
remaining point projector may be evaluated at an independent point at cost
√ζ_variance.
The Cauchy--Schwarz side condition of eq:move-over-v: with
C_a = ∑_{(h, h') : h(v) = a} H^u_{h'} ⊗ T_h, ∑ₐ C_a^* C_a ≤ 1.
Paper eq:move-over-v: the cloned delete-an-A quantity can be moved to
the right tensor factor at cost √(2δ) from point self-consistency.