Shared internal helpers for SelfImprovement results

Formerly private lemmas, now module-visible with internal-helper docstrings so they can be reused across the split result-module leaves.

Contents

• averagedPointOperator_le_one — the averaged point operator for any polynomial is bounded by 1; used by self-improvement fallback estimates.
• bipartiteSSCRel_uniform_const — lift a bipartite SSC from Unit to any nonempty question type (used by selfImprovement).
• sddRel_uniform_const — lift an SDD from Unit to any nonempty question type (used by selfImprovement).
• cons_rel_uniform_full_total_match_mass_lower_bound — from ConsRel with total-1 families, derive 1 - δ ≤ avgOver matchMass; used by input_consistency_match_mass_lower_bound.

References

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

Shared scalar bounds

theorem MIPStarRE.LDT.SelfImprovement.averagedPointOperator_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (g : Polynomial params) : averagedPointOperator params strategy g ≤ 1

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

theorem MIPStarRE.LDT.SelfImprovement.bipartiteSSCRel_uniform_const {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Question : Type u_2} {Outcome : Type u_3} [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (A : SubMeas Outcome ι) (δ : Error) : BipartiteSSCRel ψ (uniformDistribution Unit) (constSubMeasFamily A) δ → BipartiteSSCRel ψ (uniformDistribution Question) (fun (x : Question) => A) δ

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

theorem MIPStarRE.LDT.SelfImprovement.sddRel_uniform_const {κ : Type u_2} {Question : Type u_3} {Outcome : Type u_4} [Fintype κ] [DecidableEq κ] [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] (ψ : QuantumState κ) (A B : SubMeas Outcome κ) (δ : Error) : SDDRel ψ (uniformDistribution Unit) (constSubMeasFamily A) (constSubMeasFamily B) δ → SDDRel ψ (uniformDistribution Question) (fun (x : Question) => A) (fun (x : Question) => B) δ

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

theorem MIPStarRE.LDT.SelfImprovement.cons_rel_uniform_full_total_match_mass_lower_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Question : Type u_2} {Outcome : Type u_3} [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (hψ : ψ.IsNormalized) (A B : IdxSubMeas Question Outcome ι) (δ : Error) (hA_total : ∀ (q : Question), (A q).total = 1) (hB_total : ∀ (q : Question), (B q).total = 1) (hcons : ConsRel ψ (uniformDistribution Question) A B δ) : 1 - δ ≤ avgOver (uniformDistribution Question) fun (q : Question) => 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.