OAI/Computability/DepthThree/FinalParameterBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.liveProbability line 17
  2. def OAI.DepthThreeLowerBound.degreeCutoff line 19
  3. def OAI.DepthThreeLowerBound.factorialBase line 22
  4. theorem OAI.DepthThreeLowerBound.liveProbability_pos line 24
  5. theorem OAI.DepthThreeLowerBound.liveProbability_mul_dimension line 28
  6. theorem OAI.DepthThreeLowerBound.degreeCutoff_lower line 40
  7. theorem OAI.DepthThreeLowerBound.degreeCutoff_upper line 44
  8. theorem OAI.DepthThreeLowerBound.exists_liveProbability_threshold line 54
  9. theorem OAI.DepthThreeLowerBound.scaled_cutoff_le_factorialBase line 73
  10. theorem OAI.DepthThreeLowerBound.reverseTheta_le_factorial_tail line 99
  11. theorem OAI.DepthThreeLowerBound.exists_final_parameter_width line 124