OAI/NumberTheory/TwoPoint/Circuits/CircuitLogarithmicBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Convert a dyadic accuracy index to the natural logarithm used in the published fixed-depth bounded-independence input.

  1. lemma OAI.TwoPointCorrelations.dyadic_index_of_ratio line 10
  2. theorem OAI.TwoPointCorrelations.bravermanDegree_logarithmic_budget line 40