OAI/NumberTheory/EgyptianFractions/SecondDerivativeBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.second_derivative_partition_sqrt_budget line 8

   Source documentation

   The elementary square-root optimization of bad-point counting and first-derivative cancellation, with explicit harmless constants.

   theorem second_derivative_partition_sqrt_budget (A T lam : ℝ)
       (hA : 0 ≤ A) (hT : 0 ≤ T) (hlam : 0 < lam) (hlamone : lam ≤ 1) :
       (A * lam * T + 2 * Real.sqrt lam + 1) * (2 * Real.sqrt lam / lam + 1) +
         (A * lam * T + 2) * (2 / Real.sqrt lam + 1) ≤
           6 * A * T * Real.sqrt lam + 6 / Real.sqrt lam + 9 := by
   …