Documentation

MIPRE.Background.LIDT.Co.MainInductionStep.Theorems.RestrictedProbabilities.Diagonal

Section 6 — Diagonal restricted probability bounds #

The diagonal-line part of the restricted-probability bookkeeping for the main induction step: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/MainInductionStep/Theorems/RestrictedProbabilities/Diagonal.lean in the port of planning/c6b-plan.md (milestone M12, section "Port conventions").

A strategy is a SymStrat params.next 𝔓 K (Co/Test/StrategyCore.lean), whose state is the symmetric model strategy.state : SymModel 𝔓 K; the vendored qBipartiteConsDefect strategy.state A B and bipartiteConsError strategy.state 𝒟 A B are strategy.state.qBipartiteConsDefect A B and strategy.state.bipartiteConsError 𝒟 A B (Co/Test/Defs.lean), and errors are real numbers (the vendored Error := ℝ). The restricted strategy keeps the state, so every restricted defect is a defect of strategy.state.

The restricted diagonal measurement read at the base point is the ambient one on the appended line (restrictDiagonalMeasurement_postprocess_zero, Co MainInductionStep/Defs.lean), so restrictedDiagonalSampleError_eq reduces to the identification of the appended line, as in the vendored proof; the vendored final simp calls are that lemma and one rewrite. The try rfl steps of the vendored file are gone.

Not ported #

Every declaration of the vendored file has a counterpart here.

References #

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

source
theorem MIPRE.LIDT.Co.MainInductionStep.restrictedDiagonalSampleError_eq {𝔓 : 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) (x : MIPStarRE.LDT.Fq params) (j : Fin params.m) (s : MIPStarRE.LDT.RestrictedDiagonalSample params j) :
strategy.state.qBipartiteConsDefect ((xRestrictedStrategy params strategy x).restrictedDiagonalPointAnswerFamily j s) ((xRestrictedStrategy params strategy x).restrictedDiagonalLineAnswerFamily j s) = strategy.state.qBipartiteConsDefect (diagonalPointAnswerFamily strategy (MIPStarRE.LDT.embedCoord params j) (MIPStarRE.LDT.appendPoint params s.1 x, s.2)) (diagonalLineAnswerFamily strategy (MIPStarRE.LDT.embedCoord params j) (MIPStarRE.LDT.appendPoint params s.1 x, s.2))

The j-restricted diagonal defect of the x-restricted strategy at the sample s is the ambient defect at the embedded index and the sample with the height appended to its base.

source
noncomputable def MIPRE.LIDT.Co.MainInductionStep.diagonalSliceIndexError {𝔓 : 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) (x : MIPStarRE.LDT.Fq params) (j : Fin params.m) :
ℝ

Per-index diagonal-line consistency defect of the restricted x-slice strategy at embedded index j, averaged over the restricted diagonal sample space.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.LIDT.Co.MainInductionStep.diagonalIndexError {𝔓 : 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) (j : Fin params.next.m) :
    ℝ

    Per-index diagonal-line consistency defect of the ambient (m+1)-dimensional strategy at index j, averaged over the ambient restricted diagonal sample space.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.LIDT.Co.MainInductionStep.diagonalSliceIndexErrorAverage_eq_diagonalIndexError {𝔓 : 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) (j : Fin params.m) :
      (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => diagonalSliceIndexError params strategy x j) = diagonalIndexError params strategy (MIPStarRE.LDT.embedCoord params j)

      Averaging the restricted per-index diagonal error over the slice height gives the ambient per-index error at the embedded index.

      source
      theorem MIPRE.LIDT.Co.MainInductionStep.averageRestrictedDiagonalFailure_eq_embeddedDiagonalIndices {𝔓 : 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) :
      (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => (xRestrictedStrategy params strategy x).diagonalFailureProbability) = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (Fin params.m)) fun (j : Fin params.m) => diagonalIndexError params strategy (MIPStarRE.LDT.embedCoord params j)

      The average over slice heights of the restricted diagonal failure probability is the average over embedded indices of the ambient per-index error.

      source
      theorem MIPRE.LIDT.Co.MainInductionStep.weighted_diagonal_bound {𝔓 : 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 gamma : ℝ) (hgood : strategy.IsGood eps delta gamma) :
      (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => MIPStarRE.LDT.MainInductionStep.sliceTransverseDirectionWeight params * (xRestrictedStrategy params strategy x).diagonalFailureProbability) ≤ gamma

      The weighted average of the restricted diagonal slice errors is bounded by the ambient diagonal-line test error.