Binomial and multinomial bounds for lacunary exponent tuples

Paper: L-5.12 — (5.49)–(5.51) — binomial/lacunary bounds

Formalization of Definition 5.11 and Lemma 5.12 of Deng–Shen (arXiv:2607.10105), PAPER_MAP nodes D-5.11 and L-5.12.

• Anderson4D.choose_le_pow_mul_pow — paper (5.49): for α > 1 and all m, n, (m+n).choose m ≤ α ^ m * β ^ n with the explicit constant β = α / (α - 1).
• Anderson4D.Lacunary — paper Def 5.11: a family n : ι → ℕ is K-lacunary on s if every dyadic-type window [X, 2X) with X ≥ 1 contains at most K of its members.
• Anderson4D.multinomial_le_pow_mul_pow — paper (5.50): the multinomial coefficient of (n 0, …, n (r-1)) is at most α ^ (∑ i, (i+1) * n i) * β ^ (∑ i, n i).
• Anderson4D.multinomial_le_pow_of_lacunary — paper (5.51): for a K-lacunary family the multinomial coefficient is at most C(K) ^ (∑ i, n i) with a constant depending only on K.

The proof of (5.49) follows the paper: for t = 1/(α-1) > 0 the term k = m of the binomial expansion of (t+1)^(m+n) dominates (m+n).choose m * t^m, and α * t = 1 + t, α/(α-1) = 1 + t turn the resulting quotient into α ^ m * (α/(α-1)) ^ n.

theorem Anderson4D.choose_le_pow_mul_pow (α : ℝ) (hα : 1 < α) (m n : ℕ) : ↑((m + n).choose m) ≤ α ^ m * (α / (α - 1)) ^ n

Paper (5.49), Lemma 5.12. For α > 1 and all m n : ℕ, (m+n).choose m ≤ α ^ m * β ^ n with the explicit constant β = α / (α - 1).

theorem Anderson4D.choose_le_pow_mul_pow' (α β : ℝ) (hα : 1 < α) (hβ : α / (α - 1) ≤ β) (m n : ℕ) : ↑((m + n).choose m) ≤ α ^ m * β ^ n

Paper (5.49), convenience form. Any β ≥ α/(α-1) works on the right.

def Anderson4D.Lacunary (K : ℕ) {ι : Type u_1} (s : Finset ι) (n : ι → ℕ) : Prop

Paper Definition 5.11 (node D-5.11). A family of integers n : ι → ℕ, indexed by a finite set s, is K-lacunary if for every X ≥ 1 the window [X, 2X) contains at most K of the values n j, j ∈ s (counted with multiplicity of indices).

Equations

• Anderson4D.Lacunary K s n = ∀ (X : ℕ), 1 ≤ X → {j ∈ s | X ≤ n j ∧ n j < 2 * X}.card ≤ K

theorem Anderson4D.multinomial_map {ι : Type u_1} {κ : Type u_2} (e : ι ↪ κ) (s : Finset ι) (f : κ → ℕ) : Nat.multinomial (Finset.map e s) f = Nat.multinomial s (f ∘ ⇑e)

The multinomial coefficient of a mapped finset: reindexing along an embedding. Auxiliary for the Fin-recursion in paper (5.50).

theorem Anderson4D.multinomial_comp_equiv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (f : κ → ℕ) : Nat.multinomial Finset.univ (f ∘ ⇑e) = Nat.multinomial Finset.univ f

The multinomial coefficient over univ is invariant under precomposition with an equivalence of the (finite) index type. This is the permutation invariance used to reduce paper (5.51) to a sorted tuple.

theorem Anderson4D.lacunary_comp_equiv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {K : ℕ} {n : κ → ℕ} (e : ι ≃ κ) (h : Lacunary K Finset.univ n) : Lacunary K Finset.univ (n ∘ ⇑e)

Lacunarity (Def 5.11) on univ is invariant under precomposition with an equivalence of the index type.

theorem Anderson4D.multinomial_le_pow_mul_pow_aux (α : ℝ) (hα : 1 < α) (r : ℕ) (n : Fin r → ℕ) : ↑(Nat.multinomial Finset.univ n) ≤ (α ^ ∑ i : Fin r, ↑i * n i) * (α / (α - 1)) ^ ∑ i : Fin r, n i

Sharp form of paper (5.50) with 0-based weights i.val: splitting off the first index, the telescoping of (5.54) is exact for these weights.

theorem Anderson4D.multinomial_le_pow_mul_pow (α : ℝ) (hα : 1 < α) (r : ℕ) (n : Fin r → ℕ) : ↑(Nat.multinomial Finset.univ n) ≤ (α ^ ∑ i : Fin r, (↑i + 1) * n i) * (α / (α - 1)) ^ ∑ i : Fin r, n i

Paper (5.50), Lemma 5.12. For α > 1, β = α/(α-1), and any tuple n : Fin r → ℕ, the multinomial coefficient (∑ n i)! / ∏ (n i)! is at most α ^ (∑ i, (i+1) * n i) * β ^ (∑ i, n i) (1-based weights, as in the paper).

theorem Anderson4D.multinomial_le_pow_of_lacunary_sorted (K : ℕ) (hK : 1 ≤ K) (r : ℕ) (n : Fin r → ℕ) (hmono : ∀ (i j : Fin r), i ≤ j → n j ≤ n i) (hlac : Lacunary K Finset.univ n) : ↑(Nat.multinomial Finset.univ n) ≤ (2 ^ (2 * K ^ 2 + 1)) ^ ∑ i : Fin r, n i

Paper (5.51), Lemma 5.12 — sorted form. A non-increasing K-lacunary tuple (Def 5.11) has multinomial coefficient at most (2 ^ (2K² + 1)) ^ (∑ i, n i): apply (5.50) with α = 2 (so β = α/(α-1) = 2) and absorb the weighted exponent via weighted_sum_le.

theorem Anderson4D.multinomial_le_pow_of_lacunary (K : ℕ) (hK : 1 ≤ K) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (r : ℕ) (n : Fin r → ℕ), Lacunary K Finset.univ n → ↑(Nat.multinomial Finset.univ n) ≤ C ^ ∑ i : Fin r, n i

Paper (5.51), Lemma 5.12 (node L-5.12). For every K ≥ 1 there is a constant C = 2 ^ (2K² + 1) ≥ 1, depending only on K, such that every K-lacunary tuple (Def 5.11) satisfies multinomial (n 0, …, n (r-1)) ≤ C ^ (∑ i, n i). The tuple is reduced to a non-increasing one using the permutation invariance of the multinomial coefficient (multinomial_comp_equiv) along the decreasing rearrangement built from Tuple.sort and Fin.revPerm.