Selected add-in-u Step 3/4 global-variance bounds #
Selected-family Cauchy--Schwarz estimates and factor bounds for the Q₂ → Q₃ and Q₃ → Q₄
add-in-u moves: the counterpart of the vendored
SelfImprovement/Theorems/Results/AddInUStep34AndTransfer/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 AddInUStep34AndTransfer/Factored:
the sums run over the selected pairs (o, h) ∈ S_u, extended by zero to all pairs, with an
arbitrary outcome operator M^u_o.
Contents #
addInU_selected_cs_chain_step3_factored_cs,addInU_selected_cs_chain_step4_factored_cs: the operator Cauchy--Schwarz bounds,S.ev_opTensor_sandwich_abs_le_sqrt(CoBasic/OperatorExpectations) at each(u, v, o, h), lifted through the importedaddInU_selected_weighted_cauchy_schwarz.addInU_selected_sandwich_tensor_if_sum_le:∑_{(o,h) ∈ S_u} (X_h M^u_o X_h) ⊗ T_h ≤ ∑_h X_h² ⊗ T_hfor self-adjointX_h.addInU_selected_cs_chain_self_energy_factor_le_one_at: the self-energy factor is at most1.addInU_selected_cs_chain_step34_variance_factor_le_globalVarianceDeviation_sum: the variance factor is at most the summed global-variance deviation.addInU_selected_cs_chain_step{3,4}_abs_le_sqrt_globalVarianceDeviation_sum, their_of_…_leupgrades and the combinedaddInU_selected_cs_chain_step34_abs_le_sqrt_of_…_le.
Every scalar is strategy.state.ev of a joint operator; opTensor A B is
strategy.state.opTensor A B, rightTensor A is strategy.state.R A, and Xᴴ is star X. The
vendored addInU_selected_sandwich_tensor_if_sum_le 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), as Co AddInUStep12/Selected's
addInU_selected_filtered_tensor_sum_le_one does. Its hypothesis (X h)ᴴ = X h is
star (X h) = X h, which is IsSelfAdjoint (X h) by definition. The vendored Hermitian facts
SubMeas.outcome_hermitian … and rw [Matrix.conjTranspose_sub, hAu_herm, hAv_herm] are
(IsSelfAdjoint.of_nonneg …).star_eq and IsSelfAdjoint.sub; the positivity of X · H · X
through star_left_conjugate_nonneg and simpa [Matrix.star_eq_conjTranspose] is
IsSelfAdjoint.conjugate_nonneg, with the keystone's opTensor_nonneg and ev_nonneg_of_psd.
Two private helpers carry what the vendored proofs repeat inline: the self-adjointness of
A^u_{h(u)}, and ev (if c then Z else 0) = if c then ev Z else 0 (the vendored
by_cases hmem … simp [hmem, ev_zero]). The vendored simpa using conversion between the
selected sum ∑_{(o,h) ∈ S_u} of the Co addInU_selected_cs_chain_step{3,4}_diff_eq and the
zero-extended sum of the classical Cauchy--Schwarz is Fintype.sum_ite_mem.
Global variance. The summed deviation ∑_g globalVarianceDeviationAtPolynomial params strategy strategy.state T g is that of M6 (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, not the
vendored weighted state (M6's departure). The variance factor is identified with it through Co
weightedPointConditionedOperator_sq, star D * D = opTensor (star (A^u − A^v) (A^u − A^v)) T_g,
exactly where the vendored proof rewrites with its vendored counterpart, so the statement keeps
its vendored text.
Dropped hypothesis. The vendored addInU_selected_cs_chain_self_energy_factor_le_one_at
closes with ev_one_of_isNormalized strategy.state strategy.isNormalized (vendored line 484);
here strategy.state.ev_one_of_isNormalized takes no hypothesis. No statement of the vendored
file carries a swap, density or normalization hypothesis, so no statement changed.
Not ported #
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/self_improvement.texlines 299--340blueprint/src/chapter/ch07_self_improvement.tex
Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.
Selected-support weighted Cauchy--Schwarz for the add-in-u Step 3/4
summands.
The selected Step 3 and Step 4 estimates use the same finite inequality: the
summands are restricted to the selected pairs S_u, and are extended by zero
outside this support. This helper fixes the distribution and the selected
support, leaving only the three summands and their pointwise estimates to be
specified by the two applications.
Selected factored Cauchy--Schwarz bound for the Q₂ → Q₃ add-in-u step.
This is the selection-parametrized analogue of
add_in_u_cs_chain_q2_q3_factored_cs. The summation is over all pairs
(o,h), with the terms outside the selected set S_u set to zero; this form is
convenient for the finite Cauchy--Schwarz lemma and is equivalent to the
fiberwise selected sum appearing in the paper.
Selected factored Cauchy--Schwarz bound for the Q₃ → Q₄ add-in-u step.
This is the selection-parametrized analogue of
add_in_u_cs_chain_q3_q4_factored_cs; as in
addInU_selected_cs_chain_step3_factored_cs, terms outside the selected set
are represented by zeros in the finite Cauchy--Schwarz sum.
A selected sandwich tensor sum is bounded by replacing the selected submeasurement mass with the identity.
For a fixed point u, the selected pairs are a subcollection of
Outcome × Polynomial params. Summing over all pairs, the Outcome-mass
collapses to (M u).total, and the submeasurement inequality
(M u).total ≤ I gives the displayed upper bound.
The selected self-energy factor is at most 1.
For each pair of points the selected sandwich ∑_{(o,h) ∈ S_u} (A_h M^u_o A_h) ⊗ T_h, with
A_h = A^{p(u,v)}_{h(p(u,v))}, is dominated by ∑_h A_h ⊗ T_h ≤ 1 ⊗ T_{tot} ≤ 1, the point
measurement being projective.
The selected Step 3/4 variance factor is bounded by the summed global-variance deviation.
The selected middle operators form a submeasurement after summing over their
outcome coordinate, so the selected sandwich is dominated by the square of
A^v_{h(v)} - A^u_{h(u)}. Averaging over independent points identifies the
result with the global-variance deviation sum.
Raw selected Q₂ → Q₃ global-variance Cauchy--Schwarz bound after the
selected variance and self-energy factors have been estimated.
Raw selected Q₃ → Q₄ global-variance Cauchy--Schwarz bound after the
selected self-energy and variance factors have been estimated.
Upgrade the selected Q₂ → Q₃ raw global-variance bound using an external
bound on the summed global-variance deviation.
Upgrade the selected Q₃ → Q₄ raw global-variance bound using an external
bound on the summed global-variance deviation.
Combined selected Step 3/4 global-variance bridge.
The two selected replacement steps use the same summed global-variance hypothesis. This closed form supplies the raw selected Cauchy--Schwarz estimates from the factored Step 3/4 proofs in this file and then applies the external bound on the global-variance sum to both steps.