combinatorial sums?

Stream: Is there code for X?

[Ralf Stephan]

$[x^n] P(x)^k = \sum_{n_1 + n_2 + \cdots + n_k = n} a_{n_1} a_{n_2} \cdots a_{n_k}$
Is this in Mathlib? How to state the sum term? Is a proof out of reach at the moment?

[Yaël Dillies]

This exists, but can you give the LHS as a Lean expression? There are many ways you could formalise your current statement and I'm not sure which one you want

[Ralf Stephan]

import Mathlib
set_option autoImplicit false
open PowerSeries

example (k n : ℕ) (φ : ℚ⟦X⟧) (hC : constantCoeff ℚ φ = 1) : coeff ℚ n (φ ^ k) = RHS := by sorry

[Ralf Stephan]

(deleted)

[Ralf Stephan]

Is this coeff_prod (f := φ) (d := n) (s := range k)?

[Ralf Stephan]

lemma coeff_pow (k n : ℕ) (φ : R⟦X⟧) :
    coeff ℚ n (φ ^ k) = ∑ l ∈ finsuppAntidiag (range k) n, ∏ i ∈ range k, coeff R (l i) φ := by
  have h₁ (i : ℕ) : Function.const ℕ φ i = φ := rfl
  have h₂ (i : ℕ) : ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i := by
    apply prod_range_induction (fun _ => φ) (fun i => φ ^ i) rfl (congrFun rfl) i
  rw [← h₂, ← h₁ k]
  apply coeff_prod (f := Function.const ℕ φ) (d := n) (s := range k)

[Ralf Stephan]

Any objections against submitting this to Mathlib?

[Yaël Dillies]

Looks fine except for the fact that you should generalise away from Rat

[Ralf Stephan]

Part of #14452.