Finite sums encoded by independent geometric exponents

theorem NairTenenbaum.finite_sum_geometric_product_le {α : Type u_1} {ι : Type u_2} [Fintype ι] (T : Finset α) (e : α → ι → ℕ) (he : Set.InjOn e ↑T) (w : ι → ℝ) (hw₀ : ∀ (i : ι), 0 ≤ w i) (hw₁ : ∀ (i : ι), w i < 1) : ∑ a ∈ T, ∏ i : ι, w i ^ e a i ≤ ∏ i : ι, (1 - w i)⁻¹

theorem NairTenenbaum.one_sub_inv_le_exp_quadratic {t : ℝ} (ht₁ : t ≤ 1 / 2) : (1 - t)⁻¹ ≤ Real.exp (t + 2 * t ^ 2)