OAI/Combinatorics/Sensitivity/PowerAmplification.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed seed with a strict quadratic gap gives a fixed power separation.

  1. theorem OAI.Paper320.log_exponent_gt_two line 12
  2. theorem OAI.Paper320.rpow_log_exponent line 19
  3. theorem OAI.Paper320.power_amplification line 24