Products of intermediate entries of a nonnegative log-convex sequence are bounded by the corresponding endpoint product. The proof also covers zero entries and uses no logarithm or division.

theorem EulerNonnegativeLogConvex.cross (x : ℕ → ℝ) (hx : ∀ (n : ℕ), 0 ≤ x n) (hc : ∀ (n : ℕ), x (n + 1) ^ 2 ≤ x n * x (n + 2)) (a d : ℕ) : x (a + 1) * x (a + d) ≤ x a * x (a + d + 1)

theorem EulerNonnegativeLogConvex.pair (x : ℕ → ℝ) (hx : ∀ (n : ℕ), 0 ≤ x n) (hc : ∀ (n : ℕ), x (n + 1) ^ 2 ≤ x n * x (n + 2)) (a k d : ℕ) : x (a + k) * x (a + k + d) ≤ x a * x (a + 2 * k + d)

theorem EulerNonnegativeLogConvex.between (x : ℕ → ℝ) (hx : ∀ (n : ℕ), 0 ≤ x n) (hc : ∀ (n : ℕ), x (n + 1) ^ 2 ≤ x n * x (n + 2)) (s a b : ℕ) (hsa : s ≤ a) (hab : a ≤ b) : x a * x b ≤ x s * x (a + b - s)