theorem J_sum (p n : ℕ) : ∑ q ∈ Finset.range (n + 1), Jₚ (p, q) = Jₚ (p + 1, n)

theorem nBranchingFormula' (s t : ℕ+) : nBranching s t = 1 + ∑ p ∈ Finset.range ↑t, Jₚ (p + 1, (↑s * (↑t - p) - 1) / ↑t)

theorem J_asProd (p q : ℕ) : Jₚ (p, q) * p.factorial = ∏ n ∈ Finset.range p, (q + n + 1)

theorem J_asymptotic (p : ℕ) : Asymptotics.IsEquivalent Filter.atTop (fun (q : ℕ) => ↑(Jₚ (p, q))) fun (q : ℕ) => ↑q ^ p / ↑p.factorial

theorem sub_natPred (t : ℕ+) : ↑t - t.natPred = 1

theorem nBranchingBound (s t : ℕ+) : (↑↑s / ↑↑t) ^ ↑t / ↑(↑t).factorial < ↑(nBranching s t)

theorem PNat_val_tendsto : Filter.Tendsto PNat.val Filter.atTop Filter.atTop

theorem divEquivalent (d : ℕ) : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(n / d)) fun (n : ℕ) => ↑n / ↑d

theorem nBranchingAsymptotic (t : ℕ+) : Asymptotics.IsEquivalent Filter.atTop (fun (s : ℕ+) => (↑↑s / ↑↑t) ^ ↑t / ↑(↑t).factorial) fun (s : ℕ+) => ↑(nBranching s t)