Documentation

MIPStarRE.LDT.MainInductionStep.Theorems.RestrictedProbabilities.Base

Section 6 -- Restricted Probability Common Lemmas #

This module contains the averaging and scalar normalization lemmas shared by the axis-parallel, diagonal, and answer-valued restricted-probability bounds.

References #

source
def MIPStarRE.LDT.MainInductionStep.pointAppendProdEquiv (params : Parameters) [FieldModel params.q] (β : Type u_2) :
Fq params × Point params × β ≃ Point params.next × β

Repackage a restriction height, a slice point, and an auxiliary index as an ambient successor point paired with the same auxiliary index. This is the product-compatible form of CommutativityPoints.pointNextEquiv used by both ordinary and answer-valued diagonal restriction averages.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPStarRE.LDT.MainInductionStep.avgOver_uniform_pointAppend_prod (params : Parameters) [FieldModel params.q] (β : Type u_2) [Fintype β] [DecidableEq β] [Nonempty β] (g : Point params.next × β → Error) :
    (avgOver (uniformDistribution (Fq params × Point params × β)) fun (xs : Fq params × Point params × β) => g (appendPoint params xs.2.1 xs.1, xs.2.2)) = avgOver (uniformDistribution (Point params.next × β)) g

    Reindex a uniform average over a restriction height and a point, retaining an auxiliary finite index, by appending the height as the final coordinate.

    source
    theorem MIPStarRE.LDT.MainInductionStep.avgOver_uniform_restrictedDiagonalSample_append (params : Parameters) [FieldModel params.q] (j : Fin params.m) (g : RestrictedDiagonalSample params.next (embedCoord params j) → Error) :
    (avgOver (uniformDistribution (Fq params × RestrictedDiagonalSample params j)) fun (xs : Fq params × RestrictedDiagonalSample params j) => g (appendPoint params xs.2.1 xs.1, xs.2.2)) = avgOver (uniformDistribution (RestrictedDiagonalSample params.next (embedCoord params j))) g

    Reindex a restricted diagonal sample together with a restriction height as the corresponding embedded restricted diagonal sample in the successor dimension.

    source
    theorem MIPStarRE.LDT.MainInductionStep.selfConsistencyRestrictedAverage_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) :
    (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => (xRestrictedStrategy params strategy x).selfConsistencyFailureProbability) = strategy.selfConsistencyFailureProbability

    Averaging the self-consistency defect over all horizontal restrictions recovers the ambient self-consistency defect.

    source
    theorem MIPStarRE.LDT.MainInductionStep.weighted_embedded_average_le_full_average (params : Parameters) (f : Fin params.next.m → Error) (hf : ∀ (i : Fin params.next.m), 0 ≤ f i) :
    (sliceTransverseDirectionWeight params * avgOver (uniformDistribution (Fin params.m)) fun (i : Fin params.m) => f (embedCoord params i)) ≤ avgOver (uniformDistribution (Fin params.next.m)) f

    The weighted average over embedded transverse directions is bounded by the ambient average over all directions.

    source
    theorem MIPStarRE.LDT.MainInductionStep.weighted_bound_to_average (params : Parameters) {a b : Error} (h : sliceTransverseDirectionWeight params * a ≤ b) :
    a ≤ sliceConditioningLoss params * b

    Remove the transverse-direction weight from an averaged restricted bound.