OAI/Algebra/DepthFive/BetaRefinements.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.LowerParameters.beta_log_error_bounds line 10

   Source documentation

   The rounded multiplication fraction has logarithmic error at most 2/b.

   theorem beta_log_error_bounds {n : ℕ} (hn : 16 ≤ n) :
       0 ≤ Real.log (beta n / ((alpha n) ^ (rho n))) ∧
         Real.log (beta n / ((alpha n) ^ (rho n))) ≤ 2 / (b n : ℝ) := by
   …

   Mentions: OAI.Problem335.LowerParameters.beta, OAI.Problem335.LowerParameters.alpha, OAI.Problem335.LowerParameters.rho, OAI.Problem335.LowerParameters.b

2. theorem OAI.Problem335.LowerParameters.beta_le_rpow_mul_exp_two_div line 37

   Source documentation

   Sharp multiplicative rounding bound used when summing path runs.

   theorem beta_le_rpow_mul_exp_two_div {n : ℕ} (hn : 16 ≤ n) :
       beta n ≤ (alpha n) ^ (rho n) * Real.exp (2 / (b n : ℝ)) := by
   …

   Mentions: OAI.Problem335.LowerParameters.beta, OAI.Problem335.LowerParameters.alpha, OAI.Problem335.LowerParameters.rho, OAI.Problem335.LowerParameters.b