Unselected add-in-u Step 3/4 global-variance bounds

Unselected self-energy estimates, variance-factor comparisons, and the combined global-variance bridges for the projection-simplified add-in-u chain.

References

• references/ldt-paper/self_improvement.tex lines 299--340
• blueprint/src/chapter/ch07_self_improvement.tex

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q3_q4_self_energy_factor_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : (avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ h : Polynomial params, have Au := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.1; have Mh := (sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h; ev strategy.state (opTensor (Au * Mh * Au) (T.outcome h))) ≤ 1

Self-energy factor ≤ 1 for the Q₃ → Q₄ factored Cauchy--Schwarz.

The first square-root factor D₁ produced by add_in_u_cs_chain_q3_q4_factored_cs is bounded by 1. The proof collapses the outer projection A^u_{h(u)} around the sandwiched submeasurement H^u_h = A^u_{h(u)} · T_h · A^u_{h(u)} via projectivity, then bounds the per-point sum of opTensor (H^u_h) (T_h) by the submeasurement-opTensor-sum lemma, lifts to expectation via ev ψ, and averages over (u, v) with the v-average collapsing to unity.

This supplies the hD₁_le_one hypothesis required by add_in_u_cs_chain_q3_q4_le_sqrt_of_factor_bounds. The proof is fully symmetric in u ↔ v up to projection renaming, so the same pattern directly supplies hD₂_le_one for the Q₂ → Q₃ factored add_in_u_cs_chain_q2_q3_le_sqrt_of_factor_bounds analogue.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q2_q3_self_energy_factor_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : (avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ h : Polynomial params, have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.2; have Mh := (sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h; ev strategy.state (opTensor (Av * Mh * Av) (T.outcome h))) ≤ 1

Self-energy factor ≤ 1 for the Q₂ → Q₃ factored Cauchy--Schwarz.

The second square-root factor produced by add_in_u_cs_chain_q2_q3_factored_cs is bounded by 1. For fixed (u,v), the diagonal summand is one summand of the nonnegative residual tensor sum Σ_{i,r,o} A^v_o H^u_i A^v_o ⊗ T_r. The residual sum is at most 1 by sandwichTensor_residual_sum_le_one, applied to the point measurement at v, the sandwiched polynomial submeasurement at u, and the original submeasurement T.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q2_q3_variance_factor_le_globalVarianceDeviation_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : (avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ h : Polynomial params, have Au := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.1; have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.2; have Mh := (sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h; ev strategy.state (opTensor ((Av - Au) * Mh * (Av - Au)) (T.outcome h))) ≤ ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g

The variance factor in the Q₂ → Q₃ factored Cauchy--Schwarz estimate is bounded by the polynomial sum of the global-variance deviations.

For each polynomial h, the sandwiched operator H^u_h is bounded by 1. Thus the summand (A^v_{h(v)} - A^u_{h(u)}) H^u_h (A^v_{h(v)} - A^u_{h(u)}) ⊗ T_h is dominated by the squared point-operator difference tensored with T_h. The latter is exactly the integrand defining globalVarianceDeviationAtPolynomial, after expanding the weighted point-conditioned operator.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q3_q4_variance_factor_le_globalVarianceDeviation_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : (avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ h : Polynomial params, have Au := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.1; have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.2; have Mh := (sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h; ev strategy.state (opTensor ((Av - Au) * Mh * (Av - Au)) (T.outcome h))) ≤ ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g

The variance factor in the Q₃ → Q₄ factored Cauchy--Schwarz estimate is bounded by the polynomial sum of the global-variance deviations.

This is the same variance expression as in the Q₂ → Q₃ estimate, appearing as the second square-root factor rather than the first.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q2_q3_le_sqrt_globalVarianceDeviation_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √(∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g)

Raw Q₂ → Q₃ global-variance Cauchy--Schwarz bound after both factors have been estimated.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q3_q4_le_sqrt_globalVarianceDeviation_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √(∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g)

Raw Q₃ → Q₄ global-variance Cauchy--Schwarz bound after both factors have been estimated.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q2_q3_le_sqrt_of_globalVarianceDeviation_sum_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) {ζ : Error} (hglobal : ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ ζ) (hcs : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √(∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g)) : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √ζ

The global-variance sum bound upgrades the raw Cauchy--Schwarz estimate for the first global-variance replacement step into the displayed sqrt ζ bound.

This is the variance-use fragment of eq:change-one in references/ldt-paper/self_improvement.tex, lines 299--318. The hypothesis hcs is the Cauchy--Schwarz estimate eq:change-one-cauchy-schwarz (lines 306--311) after the second-square-root has been bounded by 1 using (A^v_{h(v)})² ≤ I and the fact that T is a measurement (lines 312--316, 318); concretely, the right-hand side is the summed globalVarianceDeviationAtPolynomial (the displayed first-square-root content). This lemma applies only the remaining ≤ ζ_variance step from lem:global-variance-of-points (line 317) via sqrt-monotonicity.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q3_q4_le_sqrt_of_globalVarianceDeviation_sum_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) {ζ : Error} (hglobal : ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ ζ) (hcs : |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √(∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g)) : |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √ζ

The global-variance sum bound upgrades the raw Cauchy--Schwarz estimate for the second global-variance replacement step into the displayed sqrt ζ bound.

This is the variance-use fragment of eq:change-another in references/ldt-paper/self_improvement.tex, lines 319--340. The hypothesis hcs is the Cauchy--Schwarz estimate of lines 326--332 after the first-square-root has been bounded by 1 using (A^u_{h(u)})² ≤ I and the fact that T is a measurement (lines 333--338); concretely, the right-hand side is the summed globalVarianceDeviationAtPolynomial (the displayed second-square-root content, equal to the first-square-root term of eq:change-one-cauchy-schwarz per line 340). This lemma applies only the remaining ≤ ζ_variance step (line 340) via sqrt-monotonicity.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q2_q3_le_sqrt_of_globalVarianceDeviation_sum_le_from_factor_bounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) {ζ : Error} (hglobal : ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ ζ) : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √ζ

Closed global-variance bridge for the first projection-simplified Cauchy--Schwarz replacement step.

The factor estimates proved above supply the raw square-root bound, so the only remaining hypothesis is the summed global-variance estimate.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q3_q4_le_sqrt_of_globalVarianceDeviation_sum_le_from_factor_bounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) {ζ : Error} (hglobal : ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ ζ) : |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √ζ

Closed global-variance bridge for the second projection-simplified Cauchy--Schwarz replacement step.

The factor estimates proved above supply the raw square-root bound, so the only remaining hypothesis is the summed global-variance estimate.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_global_variance_steps_of_sum_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) {ζ : Error} (hglobal : ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ ζ) (h23cs : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √(∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g)) (h34cs : |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √(∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g)) : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √ζ ∧ |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √ζ

Combined Step 3/4 variance bridge for the projection-simplified add-in-u Cauchy--Schwarz chain.

Given the two raw Cauchy--Schwarz estimates against the summed independent-points deviation and a GlobalVariance sum bound, this produces the two sqrt ζ absolute-difference bounds needed by add_in_u_simplified_transfer_of_cs_chain. It deliberately does not assemble the final transfer, so the remaining self-consistency steps and arithmetic absorption stay separate.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_global_variance_steps_of_sum_bound_from_factor_bounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) {ζ : Error} (hglobal : ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ ζ) : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √ζ ∧ |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √ζ

Combined Step 3/4 variance bridge using the factor estimates proved in this file.

This is the closed form of add_in_u_cs_chain_global_variance_steps_of_sum_bound: the raw Cauchy--Schwarz estimates are supplied by add_in_u_cs_chain_q2_q3_le_sqrt_globalVarianceDeviation_sum and add_in_u_cs_chain_q3_q4_le_sqrt_globalVarianceDeviation_sum.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_global_variance_steps_of_local_sum_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (T : SubMeas (Polynomial params) ι) (hlocal : ∑ g : Polynomial params, GlobalVariance.localVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ GlobalVariance.localVarianceOfPointsError params eps delta) (h23cs : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √(∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g)) (h34cs : |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √(∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g)) : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √(GlobalVariance.globalVarianceOfPointsError params eps delta) ∧ |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √(GlobalVariance.globalVarianceOfPointsError params eps delta)

Local-variance-sum version of the combined Step 3/4 variance bridge.

This consumes the expected output of the local-variance normalization step (expansion.tex, lines 317--321) through globalVarianceDeviation_sum_le_of_localVarianceDeviation_sum_le, then applies the combined Step 3/4 bridge above. It remains a named bridge because the blueprint cites this local-sum interface separately from the closed factor-bound lemma below.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q2_q3_le_sqrt_of_localVarianceDeviation_sum_le_from_factor_bounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (T : SubMeas (Polynomial params) ι) (hlocal : ∑ g : Polynomial params, GlobalVariance.localVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ GlobalVariance.localVarianceOfPointsError params eps delta) : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √(GlobalVariance.globalVarianceOfPointsError params eps delta)

Closed local-variance bridge for the first projection-simplified Cauchy--Schwarz replacement step.

The local-variance sum estimate is first transported to the corresponding global-variance estimate, and the factor estimates provide the raw Cauchy--Schwarz bound.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q3_q4_le_sqrt_of_localVarianceDeviation_sum_le_from_factor_bounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (T : SubMeas (Polynomial params) ι) (hlocal : ∑ g : Polynomial params, GlobalVariance.localVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ GlobalVariance.localVarianceOfPointsError params eps delta) : |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √(GlobalVariance.globalVarianceOfPointsError params eps delta)

Closed local-variance bridge for the second projection-simplified Cauchy--Schwarz replacement step.

The local-variance sum estimate is first transported to the corresponding global-variance estimate, and the factor estimates provide the raw Cauchy--Schwarz bound.

theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_global_variance_steps_of_local_sum_bound_from_factor_bounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (T : SubMeas (Polynomial params) ι) (hlocal : ∑ g : Polynomial params, GlobalVariance.localVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ GlobalVariance.localVarianceOfPointsError params eps delta) : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √(selfImprovementVarianceError params eps delta) ∧ |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √(selfImprovementVarianceError params eps delta)

Local-variance-sum version of the combined Step 3/4 variance bridge using the factor estimates proved in this file.

This is the closed local-sum form of add_in_u_cs_chain_global_variance_steps_of_sum_bound_from_factor_bounds: the only new input is the local-variance sum hypothesis, which is first transported to the global-variance sum bound.