The part factor ρ(j,σ) ≤ (9/4)^{j-1}

This file defines the part factor of the multi-jump accounting (apd:rmk:multijump) and proves the bound apd:eq:part_factor analytically: for every part size j ≥ 2, every rung boundary σ ≥ j and every real c ≥ 0.

In the multi-jump accounting a composition part of size j ending at rung boundary σ replaces the j single jumps it covers, and the ratio of what it costs to what they would have cost is

ρ(j,σ) := ε_j^{(σ)} / ∏_{ν=σ-j+1}^{σ} ε_1^{(ν)} = (σ+j-1+c)^j / ( j! · ∏_{i=σ-j+1}^{σ} (i+c) ), c := k_o/(k_h−1),

the powers of sin(dt) cancelling on both sides. The bound is ρ(j,σ) ≤ (9/4)^{j-1}.

Main definitions

• partFactor: the part factor as a function of j and the single real variable s = σ + c.
• diagFactor: its value on the diagonal s = j, the sequence (2j−1)^j/(j!)².

Main results

• partFactor_antitone: partFactor j is antitone on [j, ∞).
• partFactor_at_diag: partFactor j j = diagFactor j.
• diagFactor_ratio, diagFactor_le: diagFactor (j+1) ≤ (9/4) · diagFactor j for j ≥ 2, hence diagFactor j ≤ (9/4)^{j-1}.
• partFactor_le: partFactor j s ≤ (9/4)^{j-1} for j ≥ 2 and s ≥ j (apd:eq:part_factor).

The collapse that makes it short

ρ depends on σ and c only through s := σ + c: the denominator's factors are s, s−1, …, s−j+1 and the numerator is (s+j−1)^j. So monotonicity in σ and monotonicity in c are one monotonicity in a single real variable, and it is termwise algebra rather than calculus — writing s' = s + d, the i-th factor comparison reduces to d·(i − 2(j−1)) ≤ 0. No derivative, and c may be any nonnegative real rather than a rational k_o/(k_h−1).

The maximum is then at s = j (σ = j, c = 0), where ρ = (2j−1)^j/(j!)², and that sequence is below (9/4)^{j-1} by an induction whose ratio bound is uniform in j, so the result holds for every j ≥ 2; the only numerical input is exp(4/3) ≤ 4.03. The bound is attained with equality at j = σ = 2, c = 0.

noncomputable def Lean4LPD.partFactor (j : ℕ) (s : ℝ) : ℝ

The part factor, in the single variable s = σ + c to which the two parameters σ and c collapse:

partFactor j s = (s + j − 1)^j / ( j! · ∏_{i<j} (s − j + 1 + i) ).

The product runs over s−j+1, …, s, which is the product ∏_{i=σ-j+1}^{σ}(i+c) of the module docstring written in increasing order so that no ℕ subtraction occurs.

Equations

• Lean4LPD.partFactor j s = (s + ↑j - 1) ^ j / (↑j.factorial * ∏ i ∈ Finset.range j, (s - ↑j + 1 + ↑i))

theorem Lean4LPD.partFactor_denom_pos {j : ℕ} {s : ℝ} (hs : ↑j ≤ s) : 0 < ∏ i ∈ Finset.range j, (s - ↑j + 1 + ↑i)

theorem Lean4LPD.partFactor_antitone {j : ℕ} {s s' : ℝ} (hj : 1 ≤ j) (hs : ↑j ≤ s) (hss : s ≤ s') : partFactor j s' ≤ partFactor j s

The one monotonicity. partFactor j is antitone on [j, ∞). This is monotonicity in the boundary σ and in c at once, since ρ depends on them only through s = σ + c; it is what places the maximum at σ = j, c = 0. The proof is termwise: with s' = s + d, d ≥ 0, the i-th factor comparison is d · (i − 2(j−1)) ≤ 0, which holds because i < j.

theorem Lean4LPD.prod_range_add_one_cast (n : ℕ) : ∏ i ∈ Finset.range n, (↑i + 1) = ↑n.factorial

∏_{i<n} (i+1) = n!, over ℝ.

theorem Lean4LPD.partFactor_at_diag (j : ℕ) : partFactor j ↑j = (2 * ↑j - 1) ^ j / (↑j.factorial * ↑j.factorial)

The maximum, at s = j (σ = j, c = 0): ρ(j,j)|_{c=0} = (2j−1)^j/(j!)², which is diagFactor j.

theorem Lean4LPD.exp_four_thirds_le : Real.exp (4 / 3) ≤ 4.03

exp(4/3) ≤ 4.03, the one numeric fact the induction below needs. Obtained from exp x ≤ 1/(1-x) at x = 1/12 and exp(4/3) = exp(1/12)^16 ≤ (12/11)^16 = 4.0237.

noncomputable def Lean4LPD.diagFactor (j : ℕ) : ℝ

The diagonal sequence f j = (2j−1)^j/(j!)².

Equations

• Lean4LPD.diagFactor j = (2 * ↑j - 1) ^ j / (↑j.factorial * ↑j.factorial)

theorem Lean4LPD.diagFactor_pos {j : ℕ} (hj : 1 ≤ j) : 0 < diagFactor j

theorem Lean4LPD.diagFactor_ratio {j : ℕ} (hj : 2 ≤ j) : diagFactor (j + 1) ≤ 9 / 4 * diagFactor j

The uniform ratio bound: f(j+1) ≤ (9/4) f(j) for every j ≥ 2, where f = diagFactor. ((2j+1)/(2j−1))^j ≤ exp(2j/(2j−1)) ≤ exp(4/3) ≤ 4.03, and (2j+1)·4.03 ≤ (9/4)(j+1)² for j ≥ 2.

theorem Lean4LPD.diagFactor_le (j : ℕ) (hj : 2 ≤ j) : diagFactor j ≤ (9 / 4) ^ (j - 1)

(2j−1)^j/(j!)² ≤ (9/4)^{j-1} for every j ≥ 2, with equality at j = 2, where both sides are 9/4. By induction on j from the uniform ratio bound diagFactor_ratio.

theorem Lean4LPD.partFactor_le {j : ℕ} {s : ℝ} (hj : 2 ≤ j) (hs : ↑j ≤ s) : partFactor j s ≤ (9 / 4) ^ (j - 1)

The part-factor bound (apd:eq:part_factor). For every part size j ≥ 2 and every boundary s = σ + c ≥ j,

ρ(j,σ) ≤ (9/4)^{j-1},

with equality at j = σ = 2, c = 0. The proof descends to the diagonal s = j by partFactor_antitone and concludes with diagFactor_le; it is analytic throughout and covers every j ≥ 2, every σ ≥ j and every real c ≥ 0.