English
For any finite index set s and nonnegative function f, the multinomial of the doubled function 2·f is bounded above by the product of a power of the sum and the original multinomial.
Русский
Для конечного множества индексов s и неотрицательной функции f мультиномиал функции 2f ограничивает произведение степени суммы и исходного мультиномиала.
LaTeX
$$$\mathrm{multinomial}(s, 2f) \le (\sum_{i\in s} f(i))^{\sum_{i\in s} f(i)} \cdot \mathrm{multinomial}(s,f)$$$
Lean4
theorem multinomial_two_mul_le_mul_multinomial :
multinomial s (fun i ↦ 2 * f i) ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * multinomial s f :=
by
rw [multinomial, multinomial, ← mul_sum, ← Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum ..)]
refine
Nat.div_le_div_of_mul_le_mul (by positivity) ((prod_factorial_dvd_factorial_sum ..).trans (Nat.dvd_mul_left ..)) ?_
calc
(2 * ∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! ≤ ((2 * ∑ i ∈ s, f i) ^ (∑ i ∈ s, f i) * (∑ i ∈ s, f i)!) * ∏ i ∈ s, (f i)! :=
by gcongr; exact Nat.factorial_two_mul_le _
_ = ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, 2 ^ f i * (f i)! := by
rw [mul_pow, ← prod_pow_eq_pow_sum, prod_mul_distrib]; ring
_ ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)! :=
by
gcongr
rw [← doubleFactorial_two_mul]
exact doubleFactorial_le_factorial _
