Nisan--Wigderson set systems and generators -- proof internals #

theorem Complexity.NWDesign.card_support_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (output : Fin outputLength) :

(design.support output).card = inputLength

theorem Complexity.NWDesign.mem_support_iff_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (output : Fin outputLength) (coordinate : Fin seedLength) :

coordinate ∈ design.support output ↔ ∃ (input : Fin inputLength), (design.coordinates output) input = coordinate

theorem Complexity.NWDesign.overlap_comm_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (first second : Fin outputLength) :

design.overlap first second = design.overlap second first

theorem Complexity.NWDesign.overlap_self_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (output : Fin outputLength) :

design.overlap output output = inputLength

theorem Complexity.NWDesign.overlap_le_inputLength_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (first second : Fin outputLength) :

design.overlap first second ≤ inputLength

theorem Complexity.NWDesign.hasOverlapBudget_mono_internal {outputLength inputLength seedLength first second : ℕ} {design : NWDesign outputLength inputLength seedLength} (hbudget : design.HasOverlapBudget first) (hle : first ≤ second) :

theorem Complexity.NWDesign.restrictSeed_apply_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (output : Fin outputLength) (seed : Fin seedLength → Bool) (input : Fin inputLength) :

design.restrictSeed output seed input = seed ((design.coordinates output) input)

theorem Complexity.NWDesign.generator_apply_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (seed : Fin seedLength → Bool) (output : Fin outputLength) :

design.generator hardFunction seed output = hardFunction (design.restrictSeed output seed)

theorem Complexity.NWDesign.exists_oriented_hybridGap_of_randomTest_internal {outputLength inputLength seedLength tapes time threshold : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hlow : (design.generator hardFunction).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) :

∃ (complement : Bool), ∃ step < outputLength, density / ↑outputLength ≤ (design.generator hardFunction).hybridGap (BitGenerator.orientTest test complement) step

theorem Complexity.NWDesign.exists_oriented_hybridGap_of_seedDescriptions_internal {outputLength inputLength seedLength tapes time threshold : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (design.generator hardFunction seed)) time) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) :

∃ (complement : Bool), ∃ step < outputLength, density / ↑outputLength ≤ (design.generator hardFunction).hybridGap (BitGenerator.orientTest test complement) step

theorem Complexity.NWDesign.exists_predictionSuccess_ge_half_add_density_div_internal {outputLength inputLength seedLength tapes time threshold : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hlow : (design.generator hardFunction).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) :

∃ (complement : Bool) (step : Fin outputLength), 1 / 2 + density / ↑outputLength ≤ NextBitPrediction.successProbability ((design.generator hardFunction).targetBit step) ((design.generator hardFunction).testAtCandidate (BitGenerator.orientTest test complement) step)

theorem Complexity.NWDesign.exists_predictionSuccess_ge_half_add_density_div_of_seedDescriptions_internal {outputLength inputLength seedLength tapes time threshold : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (design.generator hardFunction seed)) time) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) :

Documentation