Elementary exponential--factorial comparisons

The Hepp-tree volume iteration produces a factor q ^ (q - 1) from parent-function codes at a branch with q children. Paper (5.25) absorbs this into q! at exponential cost. This file records a kernel-checked, fully explicit version of that absorption.

theorem Anderson4D.pow_self_le_four_pow_mul_factorial (n : ℕ) : n ^ n ≤ 4 ^ n * n.factorial

The elementary bound n^n ≤ 4^n n!.

We compare n^n with the descending factorial (2n)(2n-1)…(n+1), then bound the central binomial coefficient by its row sum.

theorem Anderson4D.factorial_two_mul_le_four_pow_mul_factorial_sq (n : ℕ) : (2 * n).factorial ≤ 4 ^ n * n.factorial ^ 2

Central-binomial form of the even-factorial estimate: (2n)! ≤ 4^n (n!)².

theorem Anderson4D.sqrt_factorial_two_mul_le_two_pow_mul_factorial (n : ℕ) : √↑(2 * n).factorial ≤ 2 ^ n * ↑n.factorial

Square-root form used in paper (5.37): √((2n)!) ≤ 2^n n!.

theorem Anderson4D.sqrt_factorial_two_mul_sub_le (n s : ℕ) (hs : s ≤ n) : √↑(2 * n - 2 * s).factorial ≤ 2 ^ (n - s) * ↑(n - s).factorial

Shifted version of the preceding bound, matching √((2n-2s)!) in (5.37).

The factorial audit in paper (5.37)

theorem Anderson4D.prod_factorial_le_factorial_sum {α : Type u_1} (s : Finset α) (f : α → ℕ) : ∏ a ∈ s, (f a).factorial ≤ (∑ a ∈ s, f a).factorial

A product of factorials is bounded by the factorial of the sum.

This is the order-theoretic form of the multinomial divisibility lemma and is the basic tool for the last square-root factor in (5.37).

theorem Anderson4D.factorial_le_two_pow_mul_factorial_mul_factorial_sub (m s : ℕ) (hs : s ≤ m) : m.factorial ≤ 2 ^ m * s.factorial * (m - s).factorial

The binomial estimate used in the first inequality of (5.37): m! ≤ 2^m s! (m-s)!.

theorem Anderson4D.prod_factorial_sub_mul_factorial_sub_le {α : Type u_1} (s : Finset α) (ml sl : α → ℕ) (hsub : ∀ a ∈ s, sl a ≤ ml a) (n m w : ℕ) (hml : ∑ a ∈ s, ml a = 2 * n) (hsl : ∑ a ∈ s, sl a = m) (hw : 2 * w ≤ m) : (∏ a ∈ s, (ml a - sl a).factorial) * (m - 2 * w).factorial ≤ (2 * n - 2 * w).factorial

The bracketed factorial quotient in the last line of paper (5.37) is at most one, before passing to ℝ and taking square roots.

If M = ∑ m_l = 2n, S = ∑ s_l = m, and 2w ≤ m, then the deficits m_l-s_l, together with the residual m-2w, have total 2n-2w. Multinomial divisibility therefore gives the stated inequality.

theorem Anderson4D.pow_pred_le_four_pow_mul_factorial (n : ℕ) : n ^ (n - 1) ≤ 4 ^ n * n.factorial

The parent-code exponent n - 1 is absorbed by the same bound.

theorem Anderson4D.prod_pow_pred_le_prod_four_pow_factorial {α : Type u_1} (s : Finset α) (q : α → ℕ) : ∏ a ∈ s, q a ^ (q a - 1) ≤ ∏ a ∈ s, 4 ^ q a * (q a).factorial

Product form used when one parent-code factor occurs at every branch.