Section 12 pasting: line one-point transport — endpoint lemmas #
Internal helper module; part of the file-split for #1127.
References #
references/ldt-paper/ld-pasting.texblueprint/src/chapter/ch09_pasting.tex
noncomputable def
MIPStarRE.LDT.Pasting.ldSandwichLineOnePointRightEndpointMeasurement
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(ux : Point params × Fq params)
:
Measurement (Fq params) ι
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPStarRE.LDT.Pasting.ldSandwichLineOnePointRightEndpointMeasurement_toSubMeas
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(ux : Point params × Fq params)
:
(ldSandwichLineOnePointRightEndpointMeasurement params strategy ux).toSubMeas = postprocess (verticalLineMeasurementFamily params strategy ux.1) fun (f : AxisLinePolynomial params.next) =>
f.toFun ux.2
theorem
MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_endpoint_ldGbcon_of_axis_self
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(eps delta zeta : Error)
(haxis : strategy.axisParallelFailureProbability ≤ eps)
(hself : strategy.selfConsistencyFailureProbability ≤ delta)
(family : IdxPolyFamily params ι)
(hcons : family.ConsistentWithPoints strategy zeta)
:
ConsRel strategy.state (uniformDistribution (Point params × Fq params))
(fun (ux : Point params × Fq params) => postprocess (evaluateAt params ux.1 (family.meas ux.2).toSubMeas) some)
(fun (ux : Point params × Fq params) =>
postprocess (ldSandwichLineOnePointRightEndpointMeasurement params strategy ux).toSubMeas some)
(zeta + √(8 * ↑params.m * eps + 4 * delta))
theorem
MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_endpoint_ldGbcon_lift_of_axis_self
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(eps delta zeta : Error)
(haxis : strategy.axisParallelFailureProbability ≤ eps)
(hself : strategy.selfConsistencyFailureProbability ≤ delta)
(family : IdxPolyFamily params ι)
(hcons : family.ConsistentWithPoints strategy zeta)
(k i : ℕ)
(hi : i < k)
:
ConsRel strategy.state (uniformDistribution (SandwichedLineQuestion params k))
(fun (q : SandwichedLineQuestion params k) =>
postprocess (evaluateAt params q.1 (family.meas (q.2 ⟨i, hi⟩)).toSubMeas) some)
(ldSandwichLineOnePointRightFamily params strategy family k i) (zeta + √(8 * ↑params.m * eps + 4 * delta))
theorem
MIPStarRE.LDT.Pasting.gHatIdxMeas_outcome_some_eq_evaluateAt
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(x : Fq params)
(u : Point params)
(a : Fq params)
:
(∑ g : GHatOutcome params,
if Option.map (fun (g' : Polynomial params) => g'.toFun u) g = some a then (gHatIdxMeas params family x).outcome g
else 0) = (evaluateAt params u (family.meas x).toSubMeas).outcome a
theorem
MIPStarRE.LDT.Pasting.gHatSandwichFamily_restrict_zero_outcome_some
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
{n : ℕ}
(xs : PointTuple params (n + 1))
(u : Point params)
(a : Fq params)
:
(postprocess
(restrictSubMeas (gHatSandwichFamily params family (n + 1) xs) fun (gs : GHatTupleOutcome params (n + 1)) =>
Option.isSome (gs 0) = true)
fun (gs : GHatTupleOutcome params (n + 1)) =>
Option.map (fun (g : Polynomial params) => g.toFun u) (gs 0)).outcome
(some a) = ∑ gs : GHatTupleOutcome params (n + 1),
if Option.map (fun (g : Polynomial params) => g.toFun u) (gs 0) = some a then
have half := gHatHalfProductOutcomeOperator params family (n + 1) xs gs;
half * Matrix.conjTranspose half
else 0
theorem
MIPStarRE.LDT.Pasting.evaluateAt_postprocess_some_outcome_none_eq_zero
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(x : Fq params)
(u : Point params)
:
theorem
MIPStarRE.LDT.Pasting.gHatSandwichFamily_restrict_zero_outcome_none_eq_zero
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
{n : ℕ}
(xs : PointTuple params (n + 1))
(u : Point params)
:
(postprocess
(restrictSubMeas (gHatSandwichFamily params family (n + 1) xs) fun (gs : GHatTupleOutcome params (n + 1)) =>
Option.isSome (gs 0) = true)
fun (gs : GHatTupleOutcome params (n + 1)) =>
Option.map (fun (g : Polynomial params) => g.toFun u) (gs 0)).outcome
none = 0
theorem
MIPStarRE.LDT.Pasting.ldSandwichLineOnePointLeftFamily_zero_outcome_some_eq_endpoint
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
{k : ℕ}
(hk : 0 < k)
(q : SandwichedLineQuestion params k)
(a : Fq params)
:
(ldSandwichLineOnePointLeftFamily params strategy family k 0 q).outcome (some a) = (evaluateAt params q.1 (family.meas (q.2 ⟨0, hk⟩)).toSubMeas).outcome a
theorem
MIPStarRE.LDT.Pasting.ldSandwichLineOnePointLeftFamily_zero_eq_endpoint
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
{k : ℕ}
(hk : 0 < k)
:
ldSandwichLineOnePointLeftFamily params strategy family k 0 = fun (q : SandwichedLineQuestion params k) =>
postprocess (evaluateAt params q.1 (family.meas (q.2 ⟨0, hk⟩)).toSubMeas) some
theorem
MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_endpoint_sqrt_bound
(params : Parameters)
(eps delta : Error)
(k : ℕ)
(hk_pos : 1 ≤ k)
(heps_nonneg : 0 ≤ eps)
(hdelta_nonneg : 0 ≤ delta)
:
theorem
MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_endpoint_error_le
(params : Parameters)
[FieldModel params.q]
(eps delta gamma zeta : Error)
(k : ℕ)
(hk_pos : 1 ≤ k)
(heps_nonneg : 0 ≤ eps)
(hdelta_nonneg : 0 ≤ delta)
(hgamma_nonneg : 0 ≤ gamma)
(hzeta_nonneg : 0 ≤ zeta)
(hzeta_le : zeta ≤ 1)
: