OAI/NumberTheory/TwoPoint/Circuits/CircuitRestrictionSurvival.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A Fourier support with sufficiently many expected live coordinates retains more than t coordinates with probability at least one half.

  1. lemma OAI.TwoPointCorrelations.booleanCount_restrict line 14
  2. theorem OAI.TwoPointCorrelations.bernoulli_support_survival line 24