OAI/NumberTheory/TwoPoint/Circuits/CircuitRestrictionProbability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A finite second-moment lower-tail bound for the live coordinates of a random restriction. It is used to transfer high-degree Fourier mass.

  1. lemma OAI.TwoPointCorrelations.FiniteLaw.probability_mul_le_average line 14
  2. lemma OAI.TwoPointCorrelations.independent_boolean_variance line 28
  3. theorem OAI.TwoPointCorrelations.independent_boolean_lower_tail line 44
  4. theorem OAI.TwoPointCorrelations.independent_boolean_survival line 69