Partial fraction decompostion with derivative

Stream: Is there code for X?

[Weiyi Wang]

I am looking for the formula
image.png
(from https://en.wikipedia.org/wiki/Partial_fraction_decomposition). I found https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Polynomial/PartialFractions.html but it only states the existence. Is there one with explicit formula using the derivative?

[Eric Wieser]

Note that $\LaTeX$ works here in $$ $$s!

[Weiyi Wang]

Thanks. I just copied the image from wikipedia :sweat_smile:

If this is not in mathlib yet, I suppose I can get it from Lagrange interpolation... I'll try it tomorrow

[Weiyi Wang]

For those who are using dark mode, here is the formula I want
$\frac{P(x)}{Q(x)} = \sum_r \frac{P(r)}{Q'(r)} \frac{1}{x-r}$
where Q is a degree n polynomial with n distinct roots r

[Weiyi Wang]

Well, I proved a primitive version with P(x) = 1 (which is enough for my own stuff) and Lagrange.nodal

lemma PartialFractionDecompostion [Field F] [DecidableEq F]
(x: F) (roots: Finset F) (hasroots: roots.Nonempty) (notroot: x ∉ roots):
((Lagrange.nodal roots id).eval x)⁻¹ = ∑ r ∈ roots, (x - r)⁻¹ * ((Polynomial.derivative (Lagrange.nodal roots id)).eval r)⁻¹ := by
  apply DivisionMonoid.inv_eq_of_mul
  rw [Finset.mul_sum]
  have h0 (r: F) (h: r ∈ roots): (Polynomial.derivative (Lagrange.nodal roots id)).eval r
    = Polynomial.eval r (∏ r' ∈ roots.erase r, (Polynomial.X - Polynomial.C r')) := by
    rw [Lagrange.derivative_nodal]
    rw [Polynomial.eval_finset_sum]
    unfold Lagrange.nodal
    simp
    apply Finset.sum_eq_single r
    · intro r' r'mem r'ne
      rw [Polynomial.eval_prod]
      apply Finset.prod_eq_zero_iff.mpr
      use r
      constructor
      · exact Finset.mem_erase_of_ne_of_mem (id (Ne.symm r'ne)) h
      · simp
    · exact fun a ↦ False.elim (a h)

  have h1 :
     ∑ r ∈ roots, ((Lagrange.nodal roots id).eval x) * ((x - r)⁻¹ * ((Polynomial.derivative (Lagrange.nodal roots id)).eval r)⁻¹)
   = ∑ r ∈ roots, (Lagrange.basis roots id r).eval x := by
    apply Finset.sum_congr rfl
    intro r rmem
    rw [h0 r rmem]
    unfold Lagrange.nodal
    rw [Polynomial.eval_prod]
    simp
    have notroot': x - r ≠ 0 := by
      refine sub_ne_zero_of_ne ?_
      exact Ne.symm (ne_of_mem_of_not_mem rmem notroot)
    rw [← mul_assoc]
    rw [← Finset.mul_prod_erase roots _ rmem]
    nth_rw 2 [mul_comm]
    rw [← mul_assoc]
    rw [inv_mul_cancel₀ notroot']
    rw [one_mul]
    unfold Lagrange.basis
    rw [Polynomial.eval_prod]
    rw [Polynomial.eval_prod]
    unfold Lagrange.basisDivisor
    rw [← Finset.prod_inv_distrib]
    rw [← Finset.prod_mul_distrib]
    apply Finset.prod_congr rfl
    intro r' r'mem
    simp
    rw [mul_comm]
  rw [h1]
  rw [← Polynomial.eval_finset_sum]
  rw [Lagrange.sum_basis (Set.injOn_id _) hasroots]
  simp

For my application the polynomial Q(x) is in complex numbers, but I also need to prove that it has no multiple roots...