Line interpolation: H-B consistency error aggregation

The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/LineInterpolation/HBError.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The fixed-u defect of the pasted submeasurement restricted to a vertical line, its comparison with the bad mass of BadMass.lean over distinct tuples, the passage from distinct to independent tuples (ldDnoteq), and the aggregation of the one-point line estimates of lem:ld-sandwich-line-one-point into hBConsistencyError, which drives lem:h-b-consistency.

A strategy is a SymStrat params.next 𝔓 K and the slice family an IdxPolyFamily params 𝔓; the defects are read on strategy.state. The vendored file's five scalar lemmas (the expansion of hBConsistencyError, the sum over Fin k of averages, and the bounds of the degree ratio and of the distinct-tuple loss by the displayed error) are classical and imported from the vendored file. The nonnegativity of eps and delta in avgOver_distinct_badMass_le_hBConsistencyError comes from eps_nonneg_of_isGood and delta_nonneg_of_isGood, which unfold to the vendored bipartiteConsError_nonneg and bipartiteSSCError_nonneg steps. No statement carries a swap or normalization hypothesis, the vendored statements having none.

Not ported

• hBConsistencyError_eq_k_mul_ldSandwichLineOnePointError_add: classical, imported.
• avgOver_sum_fin: classical, imported.
• one_div_q_le_rpow_degreeRatio: classical, imported.
• dnoteq_term_le_hBConsistency_extra: classical, imported.
• hBConsistency_error_bound: classical, imported.

References

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

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

theorem MIPRE.LIDT.Co.Pasting.hBConsistency_fixed_u_defect_le_avgOver_distinct {𝔓 : 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 𝔓) (k : ℕ) (u : MIPStarRE.LDT.Point params) : strategy.state.qBipartiteConsDefect (hRestrictionToVerticalLine params (constructedPastedSubMeas params family k) u) (verticalLineMeasurementFamily params strategy u) ≤ MIPStarRE.LDT.avgOver (MIPStarRE.LDT.Pasting.distinctTupleDistribution params k) fun (xs : MIPStarRE.LDT.PointTuple params k) => strategy.state.qBipartiteConsDefect (hRestrictionToVerticalLine params (pastedInterpolationFamily params family k xs) u) (verticalLineMeasurementFamily params strategy u)

For a fixed base point u, the consistency defect of the constructed pasted submeasurement restricted to the vertical line through u is at most the average over distinct tuples of the defects of the pasted interpolations.

theorem MIPRE.LIDT.Co.Pasting.avgOver_distinct_pasted_defect_le_badMass {𝔓 : 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 𝔓) {k : ℕ} (u : MIPStarRE.LDT.Point params) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.Pasting.distinctTupleDistribution params k) fun (xs : MIPStarRE.LDT.PointTuple params k) => strategy.state.qBipartiteConsDefect (hRestrictionToVerticalLine params (pastedInterpolationFamily params family k xs) u) (verticalLineMeasurementFamily params strategy u)) ≤ MIPStarRE.LDT.avgOver (MIPStarRE.LDT.Pasting.distinctTupleDistribution params k) fun (xs : MIPStarRE.LDT.PointTuple params k) => hBConsistencyBadMass params strategy family u xs

Over distinct tuples, the average defect of the pasted interpolations on the vertical line through u is at most the average bad mass.

theorem MIPRE.LIDT.Co.Pasting.avgOver_distinct_badMass_le_avgOver_uniform_badMass_add_dnoteq {𝔓 : 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 𝔓) {k : ℕ} (u : MIPStarRE.LDT.Point params) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.Pasting.distinctTupleDistribution params k) fun (xs : MIPStarRE.LDT.PointTuple params k) => hBConsistencyBadMass params strategy family u xs) ≤ (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.PointTuple params k)) fun (xs : MIPStarRE.LDT.PointTuple params k) => hBConsistencyBadMass params strategy family u xs) + ↑k ^ 2 / ↑params.q

Passing from distinct to independent tuples costs at most k² / q on the bad mass.

theorem MIPRE.LIDT.Co.Pasting.avgOver_uniform_badMass_le_k_mul_ldSandwichLineOnePointError_ofLinePointBounds {𝔓 : 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 𝔓) (eps delta gamma zeta : ℝ) (k : ℕ) (hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) fun (u : MIPStarRE.LDT.Point params) => MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.PointTuple params k)) fun (xs : MIPStarRE.LDT.PointTuple params k) => hBConsistencyBadMass params strategy family u xs) ≤ ↑k * MIPStarRE.LDT.Pasting.ldSandwichLineOnePointError params eps delta gamma zeta k

Internal aggregation form after the one-point line estimates have been supplied.

Source: In references/ldt-paper/ld-pasting.tex:1075-1109, the proof of lem:h-b-consistency applies lem:ld-sandwich-line-one-point for each coordinate and then sums the resulting bounds. The paper-facing theorem below derives these one-point estimates from the source hypotheses.

theorem MIPRE.LIDT.Co.Pasting.avgOver_uniform_badMass_le_k_mul_ldSandwichLineOnePointError {𝔓 : 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 𝔓) (eps delta gamma zeta : ℝ) (hgood : strategy.IsGood eps delta gamma) (hgamma_le : gamma ≤ 1) (hzeta_le : zeta ≤ 1) (hdq_le : params.d ≤ params.q) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) fun (u : MIPStarRE.LDT.Point params) => MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.PointTuple params k)) fun (xs : MIPStarRE.LDT.PointTuple params k) => hBConsistencyBadMass params strategy family u xs) ≤ ↑k * MIPStarRE.LDT.Pasting.ldSandwichLineOnePointError params eps delta gamma zeta k

The independent-tuple bad mass is bounded by the sum of the one-point line errors, in the source-facing Section 12 context.

theorem MIPRE.LIDT.Co.Pasting.avgOver_distinct_badMass_le_hBConsistencyError_ofLinePointBounds {𝔓 : 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 𝔓) (eps delta gamma zeta : ℝ) (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) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) fun (u : MIPStarRE.LDT.Point params) => MIPStarRE.LDT.avgOver (MIPStarRE.LDT.Pasting.distinctTupleDistribution params k) fun (xs : MIPStarRE.LDT.PointTuple params k) => hBConsistencyBadMass params strategy family u xs) ≤ MIPStarRE.LDT.Pasting.hBConsistencyError params eps delta gamma zeta k

Aggregate the one-point line comparison statements over all inserted vertical lines and absorb the distinct-tuple loss into the displayed hBConsistency error.

This is the reusable bad-mass aggregation from ld-pasting.tex lines 1186--1202 (also used in the proof of lem:h-b-consistency).

theorem MIPRE.LIDT.Co.Pasting.avgOver_distinct_badMass_le_hBConsistencyError {𝔓 : 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 𝔓) (eps delta gamma zeta : ℝ) (k : ℕ) (hd : 0 < params.d) (hgood : strategy.IsGood eps delta gamma) (hgamma_le : gamma ≤ 1) (hzeta_le : zeta ≤ 1) (hdq_le : params.d ≤ params.q) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) fun (u : MIPStarRE.LDT.Point params) => MIPStarRE.LDT.avgOver (MIPStarRE.LDT.Pasting.distinctTupleDistribution params k) fun (xs : MIPStarRE.LDT.PointTuple params k) => hBConsistencyBadMass params strategy family u xs) ≤ MIPStarRE.LDT.Pasting.hBConsistencyError params eps delta gamma zeta k

Aggregate the one-point line comparison estimates and absorb the distinct-tuple loss into the displayed hBConsistency error, deriving the one-point estimates internally from lem:ld-sandwich-line-one-point.