Documentation

MIPRE.Background.LIDT.Co.Pasting.ComparisonLemmas.LdSandwichLineOnePoint.Endpoint

Section 12 pasting: line one-point transport — endpoint lemmas #

The endpoint lemmas of the line one-point transport: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/LdSandwichLineOnePoint/Endpoint.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

A strategy is a SymStrat params.next 𝔓 K and the slice family an IdxPolyFamily params 𝔓, so the right endpoint measurement is a local measurement in 𝔓, and the two endpoint consistency statements are ConsRels on strategy.state. They come from ldGbcon_of_axis_self of Co/Pasting/Core/LdGbcon.lean, reindexed along pointNextEquiv and then along the split of a sandwiched-line question at its i-th coordinate; no swap or normalization hypothesis appears, the vendored statements having none.

The left endpoint identity ldSandwichLineOnePointLeftFamily_zero_eq_endpoint (the sandwich Ĝ^{x_1} ⋯ Ĝ^{x_k} ⋯ Ĝ^{x_1}, restricted to g_1 ≠ ⊥ and read at u, is the evaluation of G^{x_1} at u) holds in any ordered ⋆-ring, and is proved here in 𝔓: the tail of the sandwich sums to the identity and G^{x_1}_g is a projection.

Not ported #

References #

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

source
noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointRightEndpointMeasurement {𝔓 : 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) (ux : MIPStarRE.LDT.Point params × MIPStarRE.LDT.Fq params) :
Measurement (MIPStarRE.LDT.Fq params) 𝔓

The vertical-line measurement through (u, 0), read at the height x: the right endpoint B^u_{f(x)} of the line one-point transport, as a measurement.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointRightEndpointMeasurement_toSubMeas {𝔓 : 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) (ux : MIPStarRE.LDT.Point params × MIPStarRE.LDT.Fq params) :
    (ldSandwichLineOnePointRightEndpointMeasurement params strategy ux).toSubMeas = postprocess (verticalLineMeasurementFamily params strategy ux.1) fun (f : MIPStarRE.LDT.AxisLinePolynomial params.next) => f.toFun ux.2

    The right endpoint measurement is the postprocessed vertical-line family.

    source
    theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_endpoint_ldGbcon_of_axis_self {𝔓 : 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) (eps delta zeta : ℝ) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) :
    strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params × MIPStarRE.LDT.Fq params)) (fun (ux : MIPStarRE.LDT.Point params × MIPStarRE.LDT.Fq params) => postprocess (evaluateAt params ux.1 (family.meas ux.2).toSubMeas) some) (fun (ux : MIPStarRE.LDT.Point params × MIPStarRE.LDT.Fq params) => postprocess (ldSandwichLineOnePointRightEndpointMeasurement params strategy ux).toSubMeas some) (zeta + √(8 * ↑params.m * eps + 4 * delta))

    The slice family evaluated at u is consistent with the vertical-line answer through (u, 0) read at the height x, uniformly over (u, x), with the error of ldGbcon.

    source
    theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_endpoint_ldGbcon_lift_of_axis_self {𝔓 : 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) (eps delta zeta : ℝ) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (k i : ℕ) (hi : i < k) :
    strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) (fun (q : MIPStarRE.LDT.Pasting.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))

    The endpoint consistency of ldSandwichLineOnePoint_endpoint_ldGbcon_of_axis_self, lifted to sandwiched-line questions through their split at the i-th coordinate.

    source
    theorem MIPRE.LIDT.Co.Pasting.gHatIdxMeas_outcome_some_eq_evaluateAt {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (x : MIPStarRE.LDT.Fq params) (u : MIPStarRE.LDT.Point params) (a : MIPStarRE.LDT.Fq params) :
    (∑ g : MIPStarRE.LDT.Pasting.GHatOutcome params, if Option.map (fun (g' : MIPStarRE.LDT.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

    The some a outcome of Ĝ^x read at u is the outcome a of G^x evaluated at u.

    source
    theorem MIPRE.LIDT.Co.Pasting.gHatSandwichFamily_restrict_zero_outcome_some {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {n : ℕ} (xs : MIPStarRE.LDT.PointTuple params (n + 1)) (u : MIPStarRE.LDT.Point params) (a : MIPStarRE.LDT.Fq params) :
    (postprocess (restrictSubMeas (gHatSandwichFamily params family (n + 1) xs) fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (n + 1)) => Option.isSome (gs 0) = true) fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (n + 1)) => Option.map (fun (g : MIPStarRE.LDT.Polynomial params) => g.toFun u) (gs 0)).outcome (some a) = ∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (n + 1), if Option.map (fun (g : MIPStarRE.LDT.Polynomial params) => g.toFun u) (gs 0) = some a then have half := gHatHalfProductOutcomeOperator params family (n + 1) xs gs; half * star half else 0

    The some a outcome of the sandwich restricted to g_1 ≠ ⊥ and read at u, as a sum of squared half-products.

    source
    theorem MIPRE.LIDT.Co.Pasting.evaluateAt_postprocess_some_outcome_none_eq_zero {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (x : MIPStarRE.LDT.Fq params) (u : MIPStarRE.LDT.Point params) :
    (postprocess (evaluateAt params u (family.meas x).toSubMeas) some).outcome none = 0

    Evaluating a polynomial submeasurement and tagging the result with some puts no mass on none.

    source
    theorem MIPRE.LIDT.Co.Pasting.gHatSandwichFamily_restrict_zero_outcome_none_eq_zero {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {n : ℕ} (xs : MIPStarRE.LDT.PointTuple params (n + 1)) (u : MIPStarRE.LDT.Point params) :
    (postprocess (restrictSubMeas (gHatSandwichFamily params family (n + 1) xs) fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (n + 1)) => Option.isSome (gs 0) = true) fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (n + 1)) => Option.map (fun (g : MIPStarRE.LDT.Polynomial params) => g.toFun u) (gs 0)).outcome none = 0

    The sandwich restricted to g_1 ≠ ⊥ and read at u puts no mass on none.

    source
    theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointLeftFamily_zero_outcome_some_eq_endpoint {𝔓 : 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 : ℕ} (hk : 0 < k) (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (a : MIPStarRE.LDT.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

    The some a outcome of the left family at the first coordinate is the outcome a of G^{x_1} evaluated at u.

    source
    theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointLeftFamily_zero_eq_endpoint {𝔓 : 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 : ℕ} (hk : 0 < k) :
    ldSandwichLineOnePointLeftFamily params strategy family k 0 = fun (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) => postprocess (evaluateAt params q.1 (family.meas (q.2 ⟨0, hk⟩)).toSubMeas) some

    The left family at the first coordinate is the evaluation of G^{x_1} at u, tagged with some: the left endpoint of the line one-point transport.