Section 12 pasting: scalar bounds for complementary Bernoulli branches

The elementary scalar estimates used by the complementary branches of thm:ld-pasting, the large-error reduction of references/ldt-paper/ld-pasting.tex, lines 52--55: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Bernoulli/ScalarBounds.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

Four declarations read a strategy or a family and are ported: kappa_nonneg_of_complete, and the three large-parameter bounds on ν, whose strategy is a SymStrat params.next 𝔓 K and whose slice family an IdxPolyFamily params 𝔓. kappa_nonneg_of_complete bounds the mass of the left-placed averaged submeasurement by 1 through the keystone's S.leftTensor_le_one, S.ev_mono and S.ev_one_of_isNormalized, the last without the vendored normalization field (section "Swap symmetry is a theorem"). No lemma of the file has a swap, density or normalization hypothesis.

The other six are arithmetic on the classical error functions ldPastingInInductionNu and ldPastingInInductionError: this file imports the vendored file and names them through an explicit open MIPStarRE.LDT.Pasting (…) list.

Not ported

• ldPasting_kappa_coefficient_nonneg: classical, imported.
• ldPasting_degreeRatio_nonneg: classical, imported.
• one_le_ldPastingNu_coefficient: classical, imported.
• one_le_ldPastingNu_of_one_le_sum: classical, imported.
• one_le_ldPastingError_of_one_le_nu: classical, imported.
• one_le_ldPastingError_of_k_eq_zero: classical, imported.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/ld-pasting.tex

theorem MIPRE.LIDT.Co.Pasting.kappa_nonneg_of_complete {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {kappa : ℝ} (hcomplete : family.Complete strategy.state kappa) : 0 ≤ kappa

The scalar κ in a complete family is nonnegative.

theorem MIPRE.LIDT.Co.Pasting.one_le_ldPastingNu_of_large_gamma {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma zeta : ℝ) (hgood : strategy.IsGood eps delta gamma) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hgamma : 1 < gamma) : 1 ≤ MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta

The ν term is at least one when γ > 1 and k ≥ 1.

theorem MIPRE.LIDT.Co.Pasting.one_le_ldPastingNu_of_large_zeta {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma zeta : ℝ) (hgood : strategy.IsGood eps delta gamma) (k : ℕ) (hk_pos : 1 ≤ k) (hzeta : 1 < zeta) : 1 ≤ MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta

The ν term is at least one when ζ > 1 and k ≥ 1.

theorem MIPRE.LIDT.Co.Pasting.one_le_ldPastingNu_of_large_degreeRatio {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma zeta : ℝ) (hgood : strategy.IsGood eps delta gamma) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hdq : params.q < params.d) : 1 ≤ MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta

The ν term is at least one when d / q > 1 and k ≥ 1.