OAI/Algebra/DepthFive/ParameterCutoff.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The real cutoff separating the two circuit-factor cases.

  1. def OAI.Problem335.LowerParameters.cutoff line 9
  2. theorem OAI.Problem335.LowerParameters.cutoff_pos line 11
  3. theorem OAI.Problem335.LowerParameters.sqrt_quarter_le_cutoff line 17
  4. theorem OAI.Problem335.LowerParameters.cutoff_le_sqrt_half line 26
  5. theorem OAI.Problem335.LowerParameters.cutoff_mul_four_s line 35
  6. theorem OAI.Problem335.LowerParameters.n_div_cutoff line 40
  7. theorem OAI.Problem335.LowerParameters.two_lt_cutoff line 46
  8. theorem OAI.Problem335.LowerParameters.low_degree_scaled_lt_quarter line 53
  9. theorem OAI.Problem335.LowerParameters.Admissible.q_le_power line 61
  10. theorem OAI.Problem335.LowerParameters.Admissible.q_le_half line 64
  11. theorem OAI.Problem335.LowerParameters.Admissible.beta_le_half line 67
  12. theorem OAI.Problem335.LowerParameters.eventually_admissible_cutoff line 70