Shared helpers for the self-improvement results

Four small lemmas reused across the self-improvement result files: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/SelfImprovement/Theorems/Results/CommonHelpers.lean in the port of planning/c6b-plan.md (milestone M10, section "Port conventions").

• averagedPointOperator_le_one: the averaged point operator A_g = E_u A^u_{g(u)} is at most the identity of 𝔓.
• bipartiteSSCRel_uniform_const: lift a bipartite strong self-consistency from Unit to any nonempty question type. It is bipartite, so it takes the model (S : SymModel 𝔓 K) and a local submeasurement A : SubMeas Outcome 𝔓.
• sddRel_uniform_const: the same for the state-dependent distance. It uses only the state, so it takes a vector state (V : VecState K) and joint submeasurements A B : SubMeas Outcome (K →L[ℂ] K) (the vendored state is on an arbitrary carrier κ). Callers pass strategy.state.toVecState and should give the lifted submeasurements explicitly, not leave them to unification (the pitfall recorded with M3).
• cons_rel_uniform_full_total_match_mass_lower_bound: from ConsRel with complete families, 1 - δ ≤ E_q ∑_a ⟨Ψ, A^q_a ⊗ B^q_a Ψ⟩. The vendored hypothesis hψ : ψ.IsNormalized is dropped: it is a theorem of the model (VecState.ev_one_of_isNormalized).

The vendored file imports SelfImprovement/Theorems/Thresholds/Final.lean, wholly classical and without a Co file; so does this one.

Not ported

Every declaration of the vendored file has a counterpart here.

References

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

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

Shared scalar bounds

theorem MIPRE.LIDT.Co.SelfImprovement.averagedPointOperator_le_one {𝔓 : 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 𝔓 K) (g : MIPStarRE.LDT.Polynomial params) : averagedPointOperator params strategy g ≤ 1

Internal helper: the averaged point operator for any polynomial is bounded by 1.

theorem MIPRE.LIDT.Co.SelfImprovement.bipartiteSSCRel_uniform_const {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] (S : SymModel 𝔓 K) (A : SubMeas Outcome 𝔓) (δ : ℝ) : S.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A) δ → S.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Question) (fun (x : Question) => A) δ

Internal helper: lift bipartite SSC from Unit to any nonempty question type.

theorem MIPRE.LIDT.Co.SelfImprovement.sddRel_uniform_const {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] (V : VecState K) (A B : SubMeas Outcome (K →L[ℂ] K)) (δ : ℝ) : V.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A) (constSubMeasFamily B) δ → V.SDDRel (MIPStarRE.LDT.uniformDistribution Question) (fun (x : Question) => A) (fun (x : Question) => B) δ

Internal helper: lift SDD from Unit to any nonempty question type.

theorem MIPRE.LIDT.Co.SelfImprovement.cons_rel_uniform_full_total_match_mass_lower_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] (S : SymModel 𝔓 K) (A B : IdxSubMeas Question Outcome 𝔓) (δ : ℝ) (hA_total : ∀ (q : Question), (A q).total = 1) (hB_total : ∀ (q : Question), (B q).total = 1) (hcons : S.ConsRel (MIPStarRE.LDT.uniformDistribution Question) A B δ) : 1 - δ ≤ MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution Question) fun (q : Question) => S.qBipartiteMatchMass (A q) (B q)

Internal helper: from ConsRel with total-1 families, derive 1 - δ ≤ avgOver matchMass. Used by input_consistency_match_mass_lower_bound. (The vendored hypothesis hψ : ψ.IsNormalized is a theorem of the model.)