Point-event self-consistency transport

This module contains the point self-consistency endpoints for the six-step local-variance transport chain in lem:local-variance-of-points (expansion.tex, lines 300--311). These are the first and last 2δ moves; the point-line 2ε moves live in PointLine.lean.

Good-strategy interfaces for the local-variance transport chain

theorem MIPStarRE.LDT.GlobalVariance.pointConditionedEventSelfConsistency {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (g : Polynomial params) : SDDRel strategy.state (uniformDistribution (Point params)) (IdxSubMeas.liftLeft fun (u : Point params) => pointConditionedEventSubMeasAtPolynomial params strategy g u) (IdxSubMeas.liftRight fun (u : Point params) => pointConditionedEventSubMeasAtPolynomial params strategy g u) (2 * delta)

The 2δ self-consistency interface for the point event A^u_{g(u)}.

This is the evaluated, two-outcome version of the first/last moves in lem:local-variance-of-points (expansion.tex, lines 305--306 and 310--311): postprocess the point measurement by the event a = g(u), then apply prop:two-notions-of-self-consistency-after-evaluation to the good-strategy self-consistency branch. The remaining six-step proof still has to pull this point-distribution estimate to the hypercube-edge sampling and weight it by (G_g)^{1/2} via prop:cab-approx-delta.

theorem MIPStarRE.LDT.GlobalVariance.pointConditionedEventSelfConsistency_weighted_point {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => have D := weightedPointConditionedOperatorAtPolynomial params strategy G g u - weightedPointConditionedRightOperatorAtPolynomial params strategy G g u; ev strategy.state (Matrix.conjTranspose D * D)) ≤ 2 * delta

The first self-consistency move in lem:local-variance-of-points, after applying prop:cab-approx-delta with the multiplier I ⊗ (G_g)^{1/2} but before pulling the point marginal to the hypercube-edge distribution.

This proves the weighted native-distribution version of expansion.tex, lines 305--306: A^u_{g(u)} ⊗ (G_g)^{1/2} ≈_{2δ} I ⊗ (G_g)^{1/2} A^u_{g(u)}.

theorem MIPStarRE.LDT.GlobalVariance.pointConditionedEventSelfConsistency_weighted_point_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (G : SubMeas (Polynomial params) ι) : (∑ g : Polynomial params, avgOver (uniformDistribution (Point params)) fun (u : Point params) => have D := weightedPointConditionedOperatorAtPolynomial params strategy G g u - weightedPointConditionedRightOperatorAtPolynomial params strategy G g u; ev strategy.state (Matrix.conjTranspose D * D)) ≤ 2 * delta

Grouped-by-evaluation-value endpoint for the first self-consistency move in lem:local-variance-of-points.

This is the sum-level analogue of pointConditionedEventSelfConsistency_weighted_point. It follows the transport at references/ldt-paper/expansion.tex, lines 305--306, but first groups all polynomials with the same value g(u). The multiplier family is 0 away from the fiber a = g(u) and is I ⊗ (G_g)^{1/2} on that fiber, so the cabApproxDelta contraction is supplied by the submeasurement inequality ∑_{g : g(u)=a} G_g ≤ I. Consequently the bound is 2δ for the polynomial sum, with no polynomial-cardinality loss.

theorem MIPStarRE.LDT.GlobalVariance.pointConditionedEventSelfConsistency_weighted_leftEdge_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (G : SubMeas (Polynomial params) ι) : (∑ g : Polynomial params, avgOver (ExpansionHypercubeGraph.rerandomizeCoord params) fun (uv : Point params × Point params) => have D := weightedPointConditionedOperatorAtPolynomial params strategy G g uv.1 - weightedPointConditionedRightOperatorAtPolynomial params strategy G g uv.1; ev strategy.state (Matrix.conjTranspose D * D)) ≤ 2 * delta

Sum-level first self-consistency endpoint on the hypercube-edge sampler.

This is the u-endpoint version of references/ldt-paper/expansion.tex, lines 305--306, after grouping polynomials by the common value g(u) before applying cabApproxDelta. It is the edge-distribution form of pointConditionedEventSelfConsistency_weighted_point_sum.

theorem MIPStarRE.LDT.GlobalVariance.pointConditionedEventSelfConsistency_weighted_rightEdge {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : (avgOver (ExpansionHypercubeGraph.rerandomizeCoord params) fun (uv : Point params × Point params) => have D := weightedPointConditionedRightOperatorAtPolynomial params strategy G g uv.2 - weightedPointConditionedOperatorAtPolynomial params strategy G g uv.2; ev strategy.state (Matrix.conjTranspose D * D)) ≤ 2 * delta

The final weighted self-consistency move on the target endpoint of the hypercube edge distribution.

This is the symmetric line-310 to line-311 substep of lem:local-variance-of-points: after the second marginal reindexing, I ⊗ (G_g)^{1/2} A^v_{g(v)} is 2δ-close to A^v_{g(v)} ⊗ (G_g)^{1/2}.

theorem MIPStarRE.LDT.GlobalVariance.pointConditionedEventSelfConsistency_weighted_rightEdge_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (G : SubMeas (Polynomial params) ι) : (∑ g : Polynomial params, avgOver (ExpansionHypercubeGraph.rerandomizeCoord params) fun (uv : Point params × Point params) => have D := weightedPointConditionedRightOperatorAtPolynomial params strategy G g uv.2 - weightedPointConditionedOperatorAtPolynomial params strategy G g uv.2; ev strategy.state (Matrix.conjTranspose D * D)) ≤ 2 * delta

Sum-level final self-consistency endpoint on the hypercube-edge sampler.

This is the v-endpoint version of references/ldt-paper/expansion.tex, lines 310--311. The second marginal of rerandomizeCoord is uniform, and the squared difference is unchanged after swapping the two endpoint operators.