Section 12 pasting: H-B consistency #
Aggregation theorem proving lem:h-b-consistency from the one-point line consistency statements.
References #
references/ldt-paper/ld-pasting.texblueprint/src/chapter/ch09_pasting.tex
theorem
MIPStarRE.LDT.Pasting.hBConsistency_ofLinePointBounds_of_axis_self
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(eps delta gamma zeta : Error)
(haxis : strategy.axisParallelFailureProbability ≤ eps)
(hself_good : strategy.selfConsistencyFailureProbability ≤ delta)
(hgamma_nonneg : 0 ≤ gamma)
(hd : 0 < params.d)
(family : IdxPolyFamily params ι)
(hcons : family.ConsistentWithPoints strategy zeta)
(hself : family.StronglySelfConsistent strategy.state zeta)
(hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta)
(k : ℕ)
(hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i)
:
HBConsistencyStatement params strategy family eps delta gamma zeta k
Internal form of lem:h-b-consistency after applying
lem:ld-sandwich-line-one-point at each coordinate.
Source: The proof in references/ldt-paper/ld-pasting.tex:1075-1109
uses the one-point line estimates and then performs the averaging and
distinct-tuple comparison. The paper-facing theorem hBConsistency below
derives the one-point estimates from the source hypotheses.
theorem
MIPStarRE.LDT.Pasting.hBConsistency_ofLinePointBounds
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(eps delta gamma zeta : Error)
(hgood : strategy.IsGood eps delta gamma)
(hd : 0 < params.d)
(family : IdxPolyFamily params ι)
(hcons : family.ConsistentWithPoints strategy zeta)
(hself : family.StronglySelfConsistent strategy.state zeta)
(hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta)
(k : ℕ)
(hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i)
:
HBConsistencyStatement params strategy family eps delta gamma zeta k
theorem
MIPStarRE.LDT.Pasting.hBConsistency
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(eps delta gamma zeta : Error)
(hgood : strategy.IsGood eps delta gamma)
(hgamma_le : gamma ≤ 1)
(hzeta_le : zeta ≤ 1)
(hdq_le : params.d ≤ params.q)
(hd : 0 < params.d)
(family : IdxPolyFamily params ι)
(hcons : family.ConsistentWithPoints strategy zeta)
(hself : family.StronglySelfConsistent strategy.state zeta)
(hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta)
(k : ℕ)
:
HBConsistencyStatement params strategy family eps delta gamma zeta k
lem:h-b-consistency, source-facing form.