Selected add-in-u Step 1/2 Cauchy--Schwarz bounds #
Selected-family contraction inputs and raw √(2δ) estimates for the first two add-in-u moves
in the self-improvement chain: the counterpart of the vendored
SelfImprovement/Theorems/Results/AddInUStep12/Selected.lean (under
MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10,
section "Port conventions"). It is the selected-pair twin of Co AddInUStep12/Raw: the sums run
over the selected pairs (o, h) ∈ S_u with an arbitrary outcome operator M^u_o, in place of
all polynomials h with the sandwiched operator.
Contents #
addInU_selected_filtered_tensor_sum_le_one: the selected fibre mass∑_{(o,h) ∈ S_u, h(v) = a} M^u_o ⊗ T_his at most1.addInU_selected_step1_C_contraction,addInU_selected_step2_C_contraction: the contraction side conditions∑ₐ C_a^* C_a ≤ 1and∑ₐ C_a C_a^* ≤ 1of the weighted Cauchy--Schwarz bounds, as inequalities inK →L[ℂ] K.addInU_selected_cs_chain_step1_abs_le_sqrt_two_delta,addInU_selected_cs_chain_step2_abs_le_sqrt_two_delta:|Q₀ − Q₁| ≤ √(2δ)and|Q₁ − Q₂| ≤ √(2δ)for the selected chain.
Every scalar is strategy.state.ev of a joint operator; leftTensor A, rightTensor A and
opTensor A B are strategy.state.L A, strategy.state.R A and strategy.state.opTensor A B,
and Xᴴ is star X. The vendored addInU_selected_filtered_tensor_sum_le_one names no state,
its opTensor being the Kronecker product on the carrier; here it takes the model
(ψ : SymModel 𝔓 K) as an explicit first argument (S is the selection), and its proof is the
keystone's opTensor_le_one after summing the fibre into M^u_{tot} ⊗ T_{tot}. The vendored
Hermitian facts (Matrix.nonneg_iff_posSemidef.mp (…outcome_pos _)).isHermitian.eq and the
Matrix.conjTranspose_sum/conjTranspose_opTensor computation of Kᴴ = K are
(IsSelfAdjoint.of_nonneg …).star_eq. The vendored proofs pass strategy.isNormalized to
closenessOfInnerProduct_right/_left (vendored lines 448 and 662); the ported Cauchy--Schwarz
bounds (Co Preliminaries/SwitchSandwichPrep/InnerProduct) have no normalization hypothesis, so
it is dropped, and the vendored rw [hCop_zero, Matrix.mul_zero, ev_zero] steps are mul_zero
(zero_mul) with VecState.ev_zero. No statement of the vendored file carries a swap, density
or normalization hypothesis.
The contraction proofs reuse Co Raw's addInU_sum_projection_sandwich_le_one, which is why this
file imports Co AddInUStep12/Raw beside Algebra, where the vendored file imports Algebra
alone (the vendored AddInUStep34AndTransfer/Factored imports both). The two raw bounds share
the new addInU_selected_sum_fiber_collapse, the selected form of Raw's
addInU_sum_fiber_collapse; the vendored proofs repeat it inline as hcollapse.
Not ported #
Every declaration of the vendored file has a counterpart here.
New here #
addInU_selected_sum_fiber_collapse: the collapse of∑ₐ ∑_{(o,h)}onto the selected pairs witha = h(v), shared by the two raw bounds.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/self_improvement.texlines 255–297 (eq:move-one,eq:move-another)blueprint/src/chapter/ch07_self_improvement.tex
The selected fiber tensor mass is a contraction.
For fixed points u, v and a value a, the selected sum over pairs
(o,h) ∈ S_u with h(v)=a is bounded by the full product
M^u_{\mathrm{tot}} ⊗ T_{\mathrm{tot}}, hence by the identity.
Cauchy--Schwarz contraction side condition for selected Step 1.
For a fixed (u, v), the selected fiber sum
K_a = ∑_{(o,h) ∈ S_u, h(v)=a} M^u_o ⊗ T_h is a contraction. Sandwiching
by the right-register point projector A^v_a and summing over a is therefore
bounded by the identity.
Cauchy--Schwarz contraction side condition for selected Step 2.
This is the left-register analogue of addInU_selected_step1_C_contraction:
for each fixed (u,v), the operators
C_a = A^v_a \otimes I · K_a, with K_a the selected fiber tensor mass,
have ∑_a C_a C_a^* ≤ I.
Collapsing a double sum ∑ₐ ∑_{(o,h)} ev(X a (o,h)) onto the selected pairs with
a = h(v), when X a (o,h) vanishes unless (o,h) ∈ s and h(v) = a: the step that turns the
fibre-indexed Cauchy--Schwarz sums of the two selected raw bounds into the single sums over the
selected pairs of the algebraic alignment.
Raw selected |Q₀ - Q₁| ≤ √(2δ) bound for the first add-in-u move.
This is the selection-parametrized form of
addInU_cs_chain_step1_abs_le_sqrt_two_delta. It applies the weighted
Cauchy--Schwarz estimate to the selected pairs (o,h) ∈ S_u; the contraction
side condition is addInU_selected_step1_C_contraction.
Raw selected |Q₁ - Q₂| ≤ √(2δ) bound for the second add-in-u move.
This is the selection-parametrized form of
addInU_cs_chain_step2_abs_le_sqrt_two_delta. It uses the left-action
Cauchy--Schwarz estimate with the selected Step 2 contraction side condition.