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.

References

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

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step3_abs_le_sqrt_globalVarianceDeviation_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) : |addInUSelectedCSChainQ2 params strategy M T S - addInUSelectedCSChainQ3 params strategy M T S| ≤ √(∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g)

Raw selected Q₂ → Q₃ global-variance Cauchy--Schwarz bound after the selected variance and self-energy factors have been estimated.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step4_abs_le_sqrt_globalVarianceDeviation_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) : |addInUSelectedCSChainQ3 params strategy M T S - addInUSelectedCSChainQ4 params strategy M T S| ≤ √(∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g)

Raw selected Q₃ → Q₄ global-variance Cauchy--Schwarz bound after the selected self-energy and variance factors have been estimated.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step3_abs_le_sqrt_of_globalVarianceDeviation_sum_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) {ζ : Error} (hglobal : ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ ζ) : |addInUSelectedCSChainQ2 params strategy M T S - addInUSelectedCSChainQ3 params strategy M T S| ≤ √ζ

Upgrade the selected Q₂ → Q₃ raw global-variance bound using an external bound on the summed global-variance deviation.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step4_abs_le_sqrt_of_globalVarianceDeviation_sum_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) {ζ : Error} (hglobal : ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ ζ) : |addInUSelectedCSChainQ3 params strategy M T S - addInUSelectedCSChainQ4 params strategy M T S| ≤ √ζ

Upgrade the selected Q₃ → Q₄ raw global-variance bound using an external bound on the summed global-variance deviation.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step34_abs_le_sqrt_of_globalVarianceDeviation_sum_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) {ζ : Error} (hglobal : ∑ g : Polynomial params, GlobalVariance.globalVarianceDeviationAtPolynomial params strategy strategy.state T g ≤ ζ) : |addInUSelectedCSChainQ2 params strategy M T S - addInUSelectedCSChainQ3 params strategy M T S| ≤ √ζ ∧ |addInUSelectedCSChainQ3 params strategy M T S - addInUSelectedCSChainQ4 params strategy M T S| ≤ √ζ

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.