OAI/Algebra/DepthFive/ParameterBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Assembly of the numerical inequalities for the actual rank parameters.

  1. theorem OAI.Problem335.LowerParameters.n_le_a0 line 11
  2. theorem OAI.Problem335.LowerParameters.n_le_b0 line 17
  3. theorem OAI.Problem335.LowerParameters.alpha_le_inv_sqrt_mul_exp line 20
  4. theorem OAI.Problem335.LowerParameters.alpha_le_rpow_mul_exp line 35
  5. theorem OAI.Problem335.LowerParameters.beta_le_rpow_mul_exp line 40
  6. theorem OAI.Problem335.LowerParameters.one_sub_rho_le_two_div_sqrt line 55
  7. theorem OAI.Problem335.LowerParameters.one_sub_rho_le_four_div_sqrt line 66
  8. theorem OAI.Problem335.LowerParameters.eventually_q_beta_le_two_div_sqrt line 71
  9. structure OAI.Problem335.LowerParameters.Admissible line 84

    Source documentation

    The explicit inequalities from the parameter lemma that are consumed by both circuit-rank and moment estimates. All are asserted for the same n.

    structure Admissible (n : ℕ) : Prop where
…
  10. theorem OAI.Problem335.LowerParameters.eventually_admissible line 105