OAI/NumberTheory/EgyptianFractions/TypeIIBlockScalar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.TypeIIBlockScalar.block_bound line 8

   Source documentation

   The scalar aggregation for one dyadic Vaughan Type-II block. All analytic information is explicit in the three elementary size bounds.

   theorem block_bound (X M T Q U V H : ℝ)
       (hX : 0 ≤ X) (hM : 0 ≤ M) (hT : 0 ≤ T)
       (hQ : 0 < Q) (hU : 0 < U) (hV : 0 < V) (hH : 1 ≤ H)
       (hMT : M * T ≤ X) (hTU : T ≤ 2 * X / U) (hMV : M ≤ X / V) :
       (2 * M * H ^ 3) * ((2 * T / Q + 1) * (2 * M + 4 * Q * H)) *
           (T * H ^ 2) ≤
         32 * X * H ^ 6 * (X / Q + X / U + X / V + Q) := by
   …