Documentation

MIPStarRE.LDT.SelfImprovement.Theorems.Results.AddInUStep34AndTransfer.Factored

Add-in-u Step 3/4 factored Cauchy--Schwarz bounds #

Real-valued variance-bound conversions and the non-selected factored Cauchy--Schwarz estimates for the Q₂ → Q₃ and Q₃ → Q₄ add-in-u moves.

References #

source
theorem MIPStarRE.LDT.SelfImprovement.addInU_le_sqrt_of_factor_bounds_right {a D₁ D₂ s : Error} (hCS : a ≤ √D₁ * √D₂) (hD₁_le : D₁ ≤ s) (hD₂_le_one : D₂ ≤ 1) :
a ≤ √s

Real square-root absorption for the Q₂ → Q₃ add-in-u factor order.

source
theorem MIPStarRE.LDT.SelfImprovement.addInU_le_sqrt_of_factor_bounds_left {a D₁ D₂ s : Error} (hCS : a ≤ √D₁ * √D₂) (hD₁_le_one : D₁ ≤ 1) (hD₂_le : D₂ ≤ s) :
a ≤ √s

Real square-root absorption for the Q₃ → Q₄ add-in-u factor order.

Add-in-u variance-bound conversions #

The following four lemmas are conditional real-valued conversions for the Q₂ → Q₃ and Q₃ → Q₄ add-in-u steps. They do not prove the operator-theoretic Cauchy--Schwarz estimates from references/ldt-paper/self_improvement.tex, lines 299--340. Instead, they convert either a squared real bound or a factored product of square-root bounds into the absolute-value square-root shape used by the surrounding scalar chain.

The hypotheses hsq, hCS, and hD*_le* are the places where future operator-level arguments must supply the Cauchy--Schwarz, submeasurement contraction, and total-mass estimates. In particular, T is a submeasurement in these statements; any ≤ 1 input corresponds to a total_le_one-style bound rather than a measurement equality.

source
theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q2_q3_le_sqrt_of_factor_bounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (D₁ D₂ : Error) (hCS : |addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √D₁ * √D₂) (hD₁_le : D₁ ≤ ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g) (hD₂_le_one : D₂ ≤ 1) :
|addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T| ≤ √(∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g)

Convert factored Q₂ → Q₃ sqrt bounds to the summed-deviation sqrt bound.

This lemma assumes the Cauchy--Schwarz product bound as hCS, a bound on the first factor by the summed independent-points deviation, and a ≤ 1 bound on the second factor. The proof is purely real-valued; the submeasurement and operator content belongs in the hypotheses.

source
theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q3_q4_le_sqrt_of_factor_bounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (D₁ D₂ : Error) (hCS : |addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √D₁ * √D₂) (hD₁_le_one : D₁ ≤ 1) (hD₂_le : D₂ ≤ ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g) :
|addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T| ≤ √(∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g)

Convert factored Q₃ → Q₄ sqrt bounds to the summed-deviation sqrt bound.

This lemma assumes the Cauchy--Schwarz product bound as hCS, a ≤ 1 bound on the first factor, and a bound on the second factor by the summed independent-points deviation. The proof is purely real-valued; the submeasurement and operator content belongs in the hypotheses.

source
theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q2_q3_factored_cs {ι : 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| ≤ √(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))) * √(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)))

Factored operator Cauchy--Schwarz bound for the Q₂ → Q₃ add-in-u step.

Applies the bipartite-tensor sandwich Cauchy--Schwarz primitive ev_opTensor_sandwich_abs_le_sqrt at each (u, v, h) and lifts the pointwise estimate through the avgOver-finset Cauchy--Schwarz inequality. The two factors are the variance term (A^v_{h(v)} - A^u_{h(u)}) · H^u_h · (A^v_{h(v)} - A^u_{h(u)}) and the self-energy term A^v_{h(v)} · H^u_h · A^v_{h(v)}.

The paper presents this step before the fiberwise o-sum is collapsed, using the middle operator M^u_o. The Lean chain has already reindexed that sum by o = h(u), so the middle operator is the helper outcome H^u_h = (sandwichedPolynomialSubMeasAt params strategy T u).outcome h.

This is the operator Cauchy--Schwarz part of eq:change-one-cauchy-schwarz in references/ldt-paper/self_improvement.tex, lines 306--311. It does not yet identify the first factor with the summed global-variance deviation, nor bound the second factor by 1; those factor estimates are supplied below and then fed into add_in_u_cs_chain_q2_q3_le_sqrt_of_factor_bounds.

source
theorem MIPStarRE.LDT.SelfImprovement.add_in_u_cs_chain_q3_q4_factored_cs {ι : 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| ≤ √(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))) * √(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)))

Factored operator Cauchy–Schwarz bound for the Q₃ → Q₄ add-in-u step.

Applies the bipartite-tensor sandwich Cauchy–Schwarz primitive ev_opTensor_sandwich_abs_le_sqrt (PR #1121) at each (u, v, h) and lifts the bound through the avgOver-finset Cauchy–Schwarz weightedFinsetCauchySchwarz. The expressions A^u_{h(u)} · H^u_h · A^u_{h(u)} and (A^v_{h(v)} − A^u_{h(u)}) · H^u_h · (A^v_{h(v)} − A^u_{h(u)}) are PSD by the conjugate-transpose-mul-mul-same monotonicity of the projection-sandwich H^u_h = A^u_{h(u)} · T_h · A^u_{h(u)}.

This is the operator/real Cauchy–Schwarz fragment of eq:change-another in references/ldt-paper/self_improvement.tex, lines 326–332. Combined with sub-measurement-monotonicity on the first factor (≤ 1) and the independent-points global-variance identification of the second factor (= ∑ g, globalVarianceDeviationAtPolynomial …), this feeds add_in_u_cs_chain_q3_q4_le_sqrt_of_factor_bounds and the add_in_u_cs_chain_q3_q4_le_sqrt_of_globalVarianceDeviation_sum_le bridge from PR #1083.