Section 12 pasting: over all outcomes — nonglobal-mass decomposition

Nonglobal-mass definitions, the vertical-line insertion, and the line-consistency decomposition that splits the nonglobal eligible mass into the bad-line event and the line-consistent residual.

References

• references/ldt-paper/ld-pasting.tex
• blueprint/src/chapter/ch09_pasting.tex

noncomputable def MIPStarRE.LDT.Pasting.overAllOutcomesDistinctNonglobalMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) : Error

Distinct-tuple mass of interpolation-eligible but globally inconsistent outcomes.

This is the scalar quantity bounded in ld-pasting.tex lines 1174--1275 when the proof removes the Global_τ(x) restriction. It is the exact local residual between the all-outcomes expansion over distinct tuples and the pasted/global part.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Pasting.avgOver_distinct_eligibleMass_eq_global_add_nonglobal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) : (avgOver (distinctTupleDistribution params k) fun (xs : PointTuple params k) => subMeasMass strategy.state (interpolationEligibleSandwichFamily params family k xs).liftLeft) = (avgOver (distinctTupleDistribution params k) fun (xs : PointTuple params k) => subMeasMass strategy.state (restrictSubMeas (interpolationEligibleSandwichFamily params family k xs) (IsGloballyConsistent params xs)).liftLeft) + overAllOutcomesDistinctNonglobalMass params strategy family k

Distinct eligible mass splits into pasted/global mass plus nonglobal mass.

noncomputable def MIPStarRE.LDT.Pasting.overAllOutcomesDistinctBadLineMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) : Error

The distinct-tuple line-mismatch mass that appears after inserting the vertical-line measurement in ld-pasting.tex lines 1178--1202.

This is the part paid for by the already-available one-point line comparison statements. The remaining md/q Schwartz--Zippel term is kept separate below.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Pasting.overAllOutcomes_distinct_bad_line_mass_le_hBConsistencyError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (eps delta gamma zeta : Error) (k : ℕ) (hd : 0 < params.d) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i) : overAllOutcomesDistinctBadLineMass params strategy family k ≤ hBConsistencyError params eps delta gamma zeta k

The one-point line comparison hypotheses bound the inserted line-mismatch mass by the displayed hBConsistency error.

Paper route: this is the aggregation in ld-pasting.tex lines 1186--1202, using prop:ld-dnoteq plus lem:ld-sandwich-line-one-point.

noncomputable def MIPStarRE.LDT.Pasting.overAllOutcomesLineConsistentIndicatorLocal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k : ℕ} (u : Point params) (xs : PointTuple params k) : Error

Local consistency-indicator mass after summing out the inserted vertical-line measurement.

For fixed u and xs, it retains nonglobal eligible tuples for which there exists some degree-d vertical-line answer matching every supported slice at u. This is the Lean counterpart of the indicator Consistent_τ(g,y,u) introduced at ld-pasting.tex lines 1204--1219.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Pasting.overAllOutcomesDistinctLineConsistentIndicatorMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) : Error

Distinct-tuple average of the consistency-indicator nonglobal mass.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Pasting.lineConsistentNonglobalMass_le_indicatorMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) : MIPStarRE.LDT.Pasting.overAllOutcomesDistinctLineConsistentNonglobalMass✝ params strategy family k ≤ overAllOutcomesDistinctLineConsistentIndicatorMass params strategy family k

Averaged line-consistent residual after the explicit line answer is summed out.

theorem MIPStarRE.LDT.Pasting.overAllOutcomes_distinct_nonglobal_mass_le_bad_line_mass_add_lineConsistent {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (k : ℕ) : overAllOutcomesDistinctNonglobalMass params strategy family k ≤ overAllOutcomesDistinctBadLineMass params strategy family k + MIPStarRE.LDT.Pasting.overAllOutcomesDistinctLineConsistentNonglobalMass✝ params strategy family k

Strict reduction of the old local residual: the nonglobal mass is bounded by the already-isolated line-mismatch mass plus the narrower line-consistent nonglobal residual.

This proves the insertion and finite-sum split from ld-pasting.tex lines 1174--1228. The following indicator lemma then sums out the inserted measurement; together they reduce the residual to the Schwartz--Zippel estimate at lines 1235--1275.