Partial fractions

These results were formalised by the Xena Project, at the suggestion of Patrick Massot.

The main theorem

• div_eq_quo_add_sum_rem_div: General partial fraction decomposition theorem for polynomials over an integral domain R : If f, g₁, g₂, ..., gₙ ∈ R[X] and the gᵢs are all monic and pairwise coprime, then ∃ q, r₁, ..., rₙ ∈ R[X] such that f / g₁g₂...gₙ = q + r₁/g₁ + ... + rₙ/gₙ and for all i, deg(rᵢ) < deg(gᵢ).

• The result is formalized here in slightly more generality, using finsets. That is, if ι is an arbitrary index type, g denotes a map from ι to R[X], and if s is an arbitrary finite subset of ι, with g i monic for all i ∈ s and for all i,j ∈ s, i ≠ j → g i is coprime to g j, then we have ∃ q ∈ R[X] , r : ι → R[X] such that ∀ i ∈ s, deg(r i) < deg(g i) and f / ∏ g i = q + ∑ (r i) / (g i), where the product and sum are over s.

• The proof is done by proving the two-denominator case and then performing finset induction for an arbitrary (finite) number of denominators.

Scope for Expansion

• Proving uniqueness of the decomposition

theorem div_eq_quo_add_rem_div_add_rem_div (R : Type) [CommRing R] [IsDomain R] (K : Type) [Field K] [Algebra (Polynomial R) K] [IsFractionRing (Polynomial R) K] (f : Polynomial R) {g₁ : Polynomial R} {g₂ : Polynomial R} (hg₁ : Polynomial.Monic g₁) (hg₂ : Polynomial.Monic g₂) (hcoprime : IsCoprime g₁ g₂) : ∃ (q : Polynomial R) (r₁ : Polynomial R) (r₂ : Polynomial R), Polynomial.degree r₁ < Polynomial.degree g₁ ∧ Polynomial.degree r₂ < Polynomial.degree g₂ ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂

Let R be an integral domain and f, g₁, g₂ ∈ R[X]. Let g₁ and g₂ be monic and coprime. Then, ∃ q, r₁, r₂ ∈ R[X] such that f / g₁g₂ = q + r₁/g₁ + r₂/g₂ and deg(r₁) < deg(g₁) and deg(r₂) < deg(g₂).

theorem div_eq_quo_add_sum_rem_div (R : Type) [CommRing R] [IsDomain R] (K : Type) [Field K] [Algebra (Polynomial R) K] [IsFractionRing (Polynomial R) K] (f : Polynomial R) {ι : Type u_1} {g : ι → Polynomial R} {s : Finset ι} (hg : ∀ i ∈ s, Polynomial.Monic (g i)) (hcop : Set.Pairwise ↑s fun (i j : ι) => IsCoprime (g i) (g j)) : ∃ (q : Polynomial R) (r : ι → Polynomial R), (∀ i ∈ s, Polynomial.degree (r i) < Polynomial.degree (g i)) ∧ (↑f / Finset.prod s fun (i : ι) => ↑(g i)) = ↑q + Finset.sum s fun (i : ι) => ↑(r i) / ↑(g i)

Let R be an integral domain and f ∈ R[X]. Let s be a finite index set. Then, a fraction of the form f / ∏ (g i) can be rewritten as q + ∑ (r i) / (g i), where deg(r i) < deg(g i), provided that the g i are monic and pairwise coprime.