Documentation

MIPRE.Background.LIDT.Co.Commutativity.Transport.Pullback

Section 11 commutativity: evaluated-slice pullback #

Pulling a family on full-slice questions back to evaluated-slice questions preserves the averaged squared distance, used to transport full-slice bounds: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Transport/Pullback.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The two lemmas use only the state vector, so they take a vector state V : VecState K and joint operator families, by the rule for same-space quantities; a strategy passes strategy.state. The reindexing equivalence evaluatedSliceQuestionEquiv is classical and is imported from the vendored file, which this file imports alongside its mirrored import.

Not ported #

References #

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

source
def MIPRE.LIDT.Co.Commutativity.evaluatedSliceQuestionEquiv (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] :
MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params ≃ (MIPStarRE.LDT.Point params × MIPStarRE.LDT.Point params) × MIPStarRE.LDT.Commutativity.FullSliceQuestion params

Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.

Reindex an evaluated-slice question into its truncated points and underlying full-slice question.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.LIDT.Co.Commutativity.sddErrorOp_pullback_fullSliceQuestion_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A B : IdxOpFamily (MIPStarRE.LDT.Commutativity.FullSliceQuestion params) Outcome (K →L[ℂ] K)) :
    (V.sddErrorOp (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => A (MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => B (MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q)) = V.sddErrorOp (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.FullSliceQuestion params)) A B

    Pulling a family on FullSliceQuestion back along fullSliceQuestionOfEvaluatedSlice preserves the averaged sddErrorOp.

    source
    theorem MIPRE.LIDT.Co.Commutativity.sddOpRel_of_pullback_fullSliceQuestion {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A B : IdxOpFamily (MIPStarRE.LDT.Commutativity.FullSliceQuestion params) Outcome (K →L[ℂ] K)) (δ : ℝ) :
    V.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => A (MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q)) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => B (MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q)) δ → V.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.FullSliceQuestion params)) A B δ

    Any SDDOpRel bound proved after pulling back along fullSliceQuestionOfEvaluatedSlice descends to FullSliceQuestion.