Polynomial rewriting

Stream: new members

[Pim Otte]

I'm trying to prove a small result about multivariate polynomials, and I'm kinda banging my head against the wall.

I think the best way to proceed at this point is trying to substitute the hmiddle hypothesis into the goal. However, the side I'd like to substitute in has a 2alphabeta term, and the goal has a alpha*beta term, with a 2 outside the monomial. I've tried bringing the 2 inside the monomial, but can't make it work, I think because most of the related lemma's work with constant polynomials and not scalars? I've tried introducing an extra fact and applying div_eq_iff_eq_mul' to hmiddle, but it doesn't seem to stick.

Any pointers? (Any other remarks about the rest are also welcome, I'm still learning a lot:))

import data.mv_polynomial.basic
import ring_theory.polynomial.homogeneous
import data.complex.basic
open_locale big_operators

noncomputable theory


def is_waring_decomposition {σ : Type*} {R : Type*} [comm_semiring R] (p : mv_polynomial σ R) (s : finset (ℕ × mv_polynomial.homogeneous_submodule σ R 1)) := (∑ i in s, (i.2 : mv_polynomial σ R)^i.1) = p

def waring_rank {σ : Type*} {R : Type*} [comm_semiring R] (p : mv_polynomial σ R) : nat := Inf ({n : ℕ | ∃ s : finset (ℕ × mv_polynomial.homogeneous_submodule σ R 1), is_waring_decomposition p s ∧ sizeof s = n} : set ℕ)

lemma simple_waring_rank (p ∈ mv_polynomial.homogeneous_submodule (fin 2) ℂ 2) : 2 ≤ waring_rank(p)  ↔ ((mv_polynomial.coeff (finsupp.single 0 1 + finsupp.single 1 1) p)^2 - 4*(mv_polynomial.coeff (finsupp.single 0 2) p)*(mv_polynomial.coeff (finsupp.single 1 2) p) ≠ 0 ∨ p = 0):=
begin
  split,
  {
    contrapose!,
    intro h,

    have choose_α_β : ∃ (α β : ℂ), (mv_polynomial.coeff (finsupp.single 0 1 + finsupp.single 1 1) p = 2*α*β ∧ mv_polynomial.coeff (finsupp.single 0 2) p = α^2 ∧ mv_polynomial.coeff (finsupp.single 1 2) p = β^2),
    {
      sorry,
    },

    cases choose_α_β with α h',
    cases h' with β hαβ,
    have fact₁ : (mv_polynomial.monomial (finsupp.single 0 1) α + mv_polynomial.monomial (finsupp.single 1 1) β)^2 = p,
    {
      ring_nf SOP,
      rw mv_polynomial.ext_iff,
      intros m,
      simp only [mv_polynomial.monomial_pow, mv_polynomial.monomial_mul, finsupp.smul_single', mul_one, mv_polynomial.coeff_add,
  mv_polynomial.coeff_monomial],
      cases hαβ with hmiddle h',
      cases h' with hfirst hlast,
      rw ← hfirst,
      rw ← hlast,
      -- hmiddle: mv_polynomial.coeff (finsupp.single 0 1 + finsupp.single 1 1) p = 2 * α * β
      -- goal: ite (finsupp.single 0 2 = m) (mv_polynomial.coeff (finsupp.single 0 2) p) 0 + mv_polynomial.coeff m (⇑(mv_polynomial.monomial (finsupp.single 0 1 + finsupp.single 1 1)) (α * β) * 2) + ite (finsupp.single 1 2 = m) (mv_polynomial.coeff (finsupp.single 1 2) p) 0 = mv_polynomial.coeff m p
      --                                                                                                                                                                                ____________
      -- how to rw hmiddle into goal?
      have fact : (mv_polynomial.coeff (finsupp.single 0 1 + finsupp.single 1 1) p) / 2 =  α * β,
      {
        rw mul_assoc at hmiddle,
        -- Failing here too
        sorry,
      },
      sorry,
    },
    sorry,
  },
  sorry,
end

[Ruben Van de Velde]

You'll need to prove you're not dividing by zero:

      have fact : (mv_polynomial.coeff (finsupp.single 0 1 + finsupp.single 1 1) p) / 2 =  α * β,
      { rw mul_assoc at hmiddle,
        have : (2 : ℂ) ≠ 0, sorry,
        rw [eq_comm, eq_div_iff this, hmiddle],
        ring },

[Ruben Van de Velde]

I wonder if anyone can guess the differences between eq_div_iff, eq_div_iff_mul_eq, eq_div_iff_mul_eq' and eq_div_iff_mul_eq'', or between div_eq_iff, div_eq_iff_eq_mul and div_eq_iff_eq_mul' (no double prime available)