Homogeneous polynomials

Stream: new members

[Pim Otte]

I'm trying to prove something about polynomials and their Waring Rank: The waring rank is the least number of summands such that a polynomial can be written as some of homogeneous linear forms raised to some power.

3 questions about the example below:

1. Are the definitions reasonable? Anything I could rewrite to make life easier, especially given the questions below?
2. the "have factoid" line has a type error, and I guess it's because I need to somehow promote to an element of the homogeneous ideal. I can't really find a way to construct a homogeneous polynomial from the start.
3. How would I set up the use statement? I imagine I need to feed in all the conditions, but I wouldn't know where to start on that.

Thanks in advance:)

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

noncomputable theory
open_locale big_operators


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

-- Is this an okay formulation?
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 test (p ∈  mv_polynomial.homogeneous_submodule (fin 2) ℂ 2) (α β : ℂ) : 0 = 0 :=
begin
    have le_equiv : waring_rank p ≤ 1,
    {
      unfold waring_rank,
      have valid_rank_one: 1 ∈ {n : ℕ | ∃ (s : finset (ℕ × ↥(mv_polynomial.homogeneous_submodule (fin 2) ℂ 1))), is_waring_decomposition p s ∧ sizeof s = n},
      {
        rw set.mem_set_of_eq,
        have h_lin_form : mv_polynomial.monomial (finsupp.single (0 : (fin 2)) 1) α + mv_polynomial.monomial (finsupp.single (1 : (fin 2)) 1) β ∈ mv_polynomial.homogeneous_submodule (fin 2) ℂ 1,
        {
          sorry,
        },
        have factoid:  is_waring_decomposition p {(2, (mv_polynomial.monomial (finsupp.single (0 : (fin 2)) 1) α + mv_polynomial.monomial (finsupp.single (1 : (fin 2)) 1) β))},
        {
             -- how to promote to element of homogeneous submodule,
        },
        -- how to do this use
        -- use ({(2, (mv_polynomial.monomial (finsupp.single 0 1) α + mv_polynomial.monomial (finsupp.single 1 1) β))} : finset (ℕ × ↥(mv_polynomial.homogeneous_submodule (fin 2) ℂ 1))),
        sorry,
      },
      exact cInf_le valid_rank_one,
    },
end

[Johan Commelin]

@Pim Otte The assumption p ∈ ... in your test lemma doesn't generate the assumptions that you would expect. That's because in type theory you need to write p : .... Does that help getting you unstuck?

[Junyan Xu]

@Pim Otte Here are some simplifications and comments about the code, including an answer to question 2. Turns out the p ∈ is unproblematic. I don't understand what "the statement" means in question 3 though.

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

noncomputable theory
open_locale big_operators
open mv_polynomial /- so that you can remove the `mv_polynomial.` prefixes. -/

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

/- The formulation looks reasonable, but if you care about the case of infinite Waring rank, you
  may consider using `with_top ℕ`. Otherwise `Inf` returns a junk value when it's infinite. -/
def waring_rank {σ : Type*} {R : Type*} [comm_semiring R] (p : mv_polynomial σ R) : ℕ :=
Inf {n : ℕ | ∃ s, is_waring_decomposition p s ∧ s.card = n}

lemma test (p ∈ homogeneous_submodule (fin 2) ℂ 2) (α β : ℂ) : 0 = 0 :=
begin
  have le_equiv : waring_rank p ≤ 1,
  { apply nat.Inf_le, /- automatically give you `valid_rank_one` -/
    { rw set.mem_set_of_eq,
      have h_lin_form :
        monomial (finsupp.single (0 : fin 2) 1) α + monomial (finsupp.single 1 1) β
        ∈ homogeneous_submodule (fin 2) ℂ 1, { sorry },
      /- Only need type annotation ( : fin 2) at one place.
        Usually written:
        have h_lin_form : C α * X (0 : fin 2) + C β + X 1 ∈ homogeneous_submodule (fin 2) ℂ 1, -/

      have factoid : is_waring_decomposition p {(2, ⟨C α * X (0 : fin 2) + C β * X 1, _⟩)},
      /- `homogeneous_submodule σ R 1` in `finset (ℕ × homogeneous_submodule σ R 1)` is
        coerced from a submodule to a (sub)type, and a term of a subtype consists of a term `q`
        of the ambient type (here `mv_polynomial σ R`) and a proof `h` that it lies in the subtype
        (i.e. `q ∈ homogeneous_submodule σ R 1`), and can be written as `⟨q, h⟩`. In the above
        I write an underscore _ for `h`, so that Lean creates a goal for you to fill in. -/
      swap 3,
      { /- The following proves that
          `C α * X (0 : fin 2) + C β * X 1 ∈ homogeneous_submodule (fin 2) R 1`;
          note that `∈ homogeneous_submodule` is defined to mean `is_homogeneous`, see
           `mv_polynomial.mem_homogeneous_submodule`.` -/
        apply submodule.add_mem _ _ _; exact (is_homogeneous_C _ _).mul (is_homogeneous_X _ _) },
      { sorry },
      /- You can also do : -/
      have factoid' : is_waring_decomposition p {_},
      swap 3,
      { use 2, use C α * X 0 + C β * X 1,
        apply submodule.add_mem _ _ _; exact (is_homogeneous_C _ _).mul (is_homogeneous_X _ _) },
      sorry,
      sorry,
    },
  },
end

[Pim Otte]

@Junyan Xu Thanks a lot, this is very insightful! I was aware of the infinite case. It's good to know that this could be handled using with_top. In this particular case, it turns out that Waring rank is always finite, so it doesn't really matter.

The final question was about the commented out use statement in my sample to fulfill the existential quantifier, but knowing how the term of the coerced type works actually solved my issues with that too.