Documentation

Complexitylib.Metacomplexity.NisanWigderson.Reconstruction.RepeatedSampling.Defs

Repeated sampling of NW reconstruction advice -- definitions #

Independent advice trials are represented by a function from a finite trial index to the finite reconstruction-advice space. Success means that at least one sampled advice attains the requested agreement threshold.

source
def Complexity.NWDesign.reconstructionAdviceTrialCount (outputLength : ℕ) (density : ℚ) :
ℕ

Canonical number of independent advice trials for output length m and positive density δ: the ceiling of 2m / δ. The definition is total; its sampling guarantee assumes positive density.

Equations
Instances For
    source
    def Complexity.NWDesign.goodReconstructionAdviceEvent {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) (agreementThreshold : ℚ) :
    Finset (design.ReconstructionAdvice current)

    Advice choices attaining a requested reconstruction-agreement threshold.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.NWDesign.repeatedGoodReconstructionAdviceProbability {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) (agreementThreshold : ℚ) (trials : ℕ) :
      ℚ

      Probability that at least one of trials independent uniform advice draws attains a requested reconstruction-agreement threshold.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For