The factorial comparison after merging equal runs

This file isolates the factorial ledger in paper (5.37). If the original leaf multiplicities are m_l, the run-compressed multiplicities are s_l, their sums are respectively 2n and m, and w = |W|, then the factorial factor produced by (5.35)--(5.36) is bounded by an absolute constant to the power n times the factorial factor in (5.15).

We take the explicit absolute constant 4. Thus the conclusion below is exactly of the paper's form C^n; increasing C only weakens the bound.

noncomputable def Anderson4D.mergeFactorialBefore {α : Type u_1} (s : Finset α) (ml sl : α → ℕ) (m w : ℕ) : ℝ

The factorial factor on the left of (5.37), after fixing the partitions and the set W.

Equations

• Anderson4D.mergeFactorialBefore s ml sl m w = (Anderson4D.sqrtFactorial (m - 2 * w) * ∏ l ∈ s, Anderson4D.sqrtFactorial (sl l)) * ∏ l ∈ s, ↑(ml l).factorial / ↑(sl l).factorial

noncomputable def Anderson4D.mergeFactorialAfter {α : Type u_1} (s : Finset α) (ml : α → ℕ) (n w : ℕ) : ℝ

The factorial factor inherited from (5.15), with its exponential constant omitted.

Equations

• Anderson4D.mergeFactorialAfter s ml n w = ↑(n - w).factorial * ∏ l ∈ s, Anderson4D.sqrtFactorial (ml l)

theorem Anderson4D.factorial_ratio_le_two_pow_mul_deficit (ml sl : ℕ) (hsl : sl ≤ ml) : ↑ml.factorial / ↑sl.factorial ≤ 2 ^ ml * ↑(ml - sl).factorial

The real factorial ratio is controlled by the binomial estimate used in the first inequality of (5.37). Positivity of the denominator is discharged here rather than hidden in a later field simplification.

theorem Anderson4D.prod_factorial_ratio_le {α : Type u_1} (s : Finset α) (ml sl : α → ℕ) (hsub : ∀ l ∈ s, sl l ≤ ml l) (n : ℕ) (hml : ∑ l ∈ s, ml l = 2 * n) : ∏ l ∈ s, ↑(ml l).factorial / ↑(sl l).factorial ≤ 2 ^ (2 * n) * ↑(∏ l ∈ s, (ml l - sl l).factorial)

Product form of the preceding binomial estimate.

theorem Anderson4D.sqrt_prod_factorial_ratio_le {α : Type u_1} (s : Finset α) (ml sl : α → ℕ) (hsub : ∀ l ∈ s, sl l ≤ ml l) (n : ℕ) (hml : ∑ l ∈ s, ml l = 2 * n) : √(∏ l ∈ s, ↑(ml l).factorial / ↑(sl l).factorial) ≤ 2 ^ n * √↑(∏ l ∈ s, (ml l - sl l).factorial)

Square-root form of the product ratio estimate. Since ∑ m_l = 2n, the square root of the binomial loss is exactly 2^n.

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

Multiplying by the residual factorial gives precisely the bracketed deficit product in the middle line of (5.37).

theorem Anderson4D.shifted_factorial_cast_pos (n w : ℕ) : 0 < ↑(2 * n - 2 * w).factorial

The denominator in the last quotient of (5.37) is strictly positive, including when natural subtraction truncates.

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

Literal form of the last parenthesized factor in (5.37): the square root of the deficit-factorial quotient is at most one.

theorem Anderson4D.sqrtFactorial_mul_factorial_ratio (ml sl : ℕ) : sqrtFactorial sl * (↑ml.factorial / ↑sl.factorial) = sqrtFactorial ml * √(↑ml.factorial / ↑sl.factorial)

The exact one-leaf square-root identity used when factoring the first line of (5.37).

theorem Anderson4D.mergeFactorialBefore_eq {α : Type u_1} (s : Finset α) (ml sl : α → ℕ) (m w : ℕ) : mergeFactorialBefore s ml sl m w = (sqrtFactorial (m - 2 * w) * ∏ l ∈ s, sqrtFactorial (ml l)) * √(∏ l ∈ s, ↑(ml l).factorial / ↑(sl l).factorial)

Exact product factorization underlying the displayed equality in (5.37). Every ratio is well-defined because factorials are strictly positive.

theorem Anderson4D.mergeFactorialBefore_le_four_pow {α : Type u_1} (s : Finset α) (ml sl : α → ℕ) (hsub : ∀ l ∈ s, sl l ≤ ml l) (n m w : ℕ) (hml : ∑ l ∈ s, ml l = 2 * n) (hsl : ∑ l ∈ s, sl l = m) (hw : 2 * w ≤ m) : mergeFactorialBefore s ml sl m w ≤ 4 ^ n * mergeFactorialAfter s ml n w

Paper (5.37), with the explicit absolute constant C = 4.

The hypotheses are exactly the numerical data available after merging equal runs: s_l ≤ m_l, ∑m_l = 2n, ∑s_l = m, and 2w ≤ m. No factorial comparison is assumed.

theorem Anderson4D.mergeFactorialBefore_le_const_pow {α : Type u_1} (s : Finset α) (ml sl : α → ℕ) (hsub : ∀ l ∈ s, sl l ≤ ml l) (C : ℝ) (hC : 4 ≤ C) (n m w : ℕ) (hml : ∑ l ∈ s, ml l = 2 * n) (hsl : ∑ l ∈ s, sl l = m) (hw : 2 * w ≤ m) : mergeFactorialBefore s ml sl m w ≤ C ^ n * mergeFactorialAfter s ml n w

Paper-style constant form of (5.37). Any fixed C ≥ 4 absorbs the explicit loss, so the preceding theorem is exactly an absolute C^n bound.