theorem MathlibNt.Analysis.SieveNormalization.upper_exp_product {X V S L t c g : ℝ} (hX : 0 ≤ X) (ht : 0 ≤ t) (hV : V ≤ c * Real.exp (-g) * t * S / L) : X * (Real.exp g * t) * V ≤ c * t ^ 2 * S * X / L

Cancel the reciprocal exponential factors in an upper sieve main term.

theorem MathlibNt.Analysis.SieveNormalization.lower_product {a t f X V M : ℝ} (hX : 0 ≤ X) (hf : 0 ≤ f) (hscale : a * t ≤ X * V) (hdensity : f * V ≤ M) : a * f * t ≤ X * M

Multiply a lower product estimate by the nonnegative lower density.