feat(data/mv_polynomial): add partial derivatives

[shingtaklam1324]

This adds partial derivatives to data/mv_polynomial.lean

• The additional import of tactic.omega is used in lines 1419 and 1420 to deal with arithmetic.
• There are also a few lemmas which I proved in the process when I was looking at data/polynomial.lean. These lemmas may not all be necessary.
• Also to do with those lemmas, the names of those lemmas may need changing.

[jcommelin]

Nice work! This is looking very good!

[kbuzzard]

Someone who understands induction better than me might want to advise on whether this needs an @[elab_as_eliminator] tag. Note also [recursor 5] on line 193 and see also https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.5Brecursor.205.5D . Is [recursor 5] deprecated? Does anyone know?

[kbuzzard]

The linter seems to be complaining about algebra.punit_instances but I can't reproduce :-(

[bryangingechen]

The linter seems to be complaining about algebra.punit_instances but I can't reproduce :-(

This was fixed in #2291. Merging master into this branch should fix that.

[kbuzzard]

Thanks. How can that even happen?

[kbuzzard]

The linter is now complaining that pderivative_monomial is tagged as simp and wants to rewrite pderivative v (C a * (X v)^n) to C (a * n) * (X v)^(n - 1), however pderivative_C_mul will get to it first and will simplify it to C a * pderivative v ((X v)^n). I removed the simp tag from pderivative_monomial but I do wonder whether the lemma could just be deleted completely; I am not sure that a random monomial in precisely one variable is the sort of thing that naturally comes up in practice anyway.

[semorrison]

Unfortunately, this would introduce a new -T50000 challenge:

$ lean -T50000 src/data/mv_polynomial.lean 
/Users/scott/projects/lean/mathlib-pderivative/src/data/mv_polynomial.lean:1397:0: error: (deterministic) timeout

It's not obvious to me how to slice this proof up, but we probably should.

[semorrison]

Could you explain why you've used erase, rather than just subtraction? It seems

def pderivative (v : S) (p : mv_polynomial S R) : mv_polynomial S R :=
p.sum (λ A B, monomial (A - single v 1) (B * (A v)))

might have been simpler.

[shingtaklam1324]

I'm not 100% sure to be honest. I think I tried that but lean complained about not having comm_ring ℕ when I went ahead with the proofs.

I'm gonna check that though.

[kbuzzard]

Proof slicing: I guess one could prove lemmas of the form "if v is not in the support of u then pderivative (monomial u r * monomial u' r') = monomial u r * pderivative (monomial u' r')

[kbuzzard]

Scott -- natural number subtraction (which Shing used) is bad enough -- your proposal uses subtraction on an object which is not a ring (so subtraction is poorly behaved) and is not nat either (so there is no automation which can deal with it). There will be no lemmas to deal with it. Shing's approach constrains the bad subtraction to the simplest type on which it occurs so I think is better for formalising given what we have.

[semorrison]

Can I suggest a different approach. Have a look at this framework:

/-- `pderivative v p` is the partial derivative of `p` with respect to `v` -/
def pderivative (v : S) (p : mv_polynomial S R) : mv_polynomial S R :=
p.sum (λ A B, monomial (A - single v 1) (B * (A v)))

-- TODO move earlier
@[simp]
lemma sum_monomial  {A : Type*} [add_comm_monoid A] 
  {u : S →₀ ℕ} {r : R} {b : (S →₀ ℕ) → R → A} (w : b u 0 = 0) :
    sum (monomial u r) b = b u r :=
sum_single_index w

@[simp]
lemma pderivative_monomial {v : S} {u : S →₀ ℕ} {a : R} :
  pderivative v (monomial u a) = monomial (u - single v 1) (a * (u v)) :=
begin
  simp [pderivative],
end

-- this one is not actually necessary, but good to check that everything is flowing in the right direction
lemma pderivative_monomial_single {a : R} {v : S} {n : ℕ} :
  pderivative v (monomial (single v n) a) = monomial (single v (n-1)) (a * n) :=
begin
  simp,
  -- TODO add missing `single_sub` lemma earlier, and verify this proof then works by simp
  sorry
end

-- Before we proceed, go edit `monomial_add` and `monomial_mul` above,
-- and reverse the direction of the equalities. 
-- Nothing breaks, and everything gets easier here.

lemma pderivative_monomial_mul {v : S} {u u' : S →₀ ℕ} {r r' : R} :
  pderivative v (monomial u r * monomial u' r') =
    pderivative v (monomial u r) * monomial u' r' + monomial u r * pderivative v (monomial u' r') :=
begin
  simp,
  -- fails, but tells us the two preparatory lemmas we need
end

lemma foo_prep {v : S} {u u' : S →₀ ℕ} (h : u v ≠ 0) :
  u - single v 1 + u' = u + u' - single v 1 :=
sorry

@[simp]
lemma foo {v : S} {u u' : S →₀ ℕ} {r r' : R} : 
  monomial (u - single v 1 + u') (r * (u v) * r') =
    monomial (u + u' - single v 1) (r * (u v) * r') :=
by sorry -- prove `by_cases u v = 0`

lemma bar_prep {v : S} {u u' : S →₀ ℕ} (h : u' v ≠ 0) :
  u + (u' - single v 1) = u + u' - single v 1 :=
sorry

@[simp]
lemma bar {v : S} {u u' : S →₀ ℕ} {r r' : R} : 
  monomial (u + (u' - single v 1)) (r * (r' * (u' v))) =
    monomial (u + u' - single v 1) (r * (r' * (u' v))) :=
by sorry -- prove `by_cases u' v = 0`

lemma pderivative_monomial_mul_take_2 {v : S} {u u' : S →₀ ℕ} {r r' : R} :
  pderivative v (monomial u r * monomial u' r') =
    pderivative v (monomial u r) * monomial u' r' + monomial u r * pderivative v (monomial u' r') :=
begin
  simp,
  congr,
  ring,
end

[semorrison]

I agree foo_prep is still unpleasant, but we've constrained all our interaction with bad subtraction to that lemma, and it's only a few lines of awful if you ext v', by_cases h : v' = v.

[semorrison]

foo_prep would become nicer if we reversed the direction of the inequality in finsupp.single_eq_of_ne, and further nicer if somehow hacked by_cases to produce a ≠ directly.

[shingtaklam1324]

I've had a look at what you've put there and filled in the proofs on my local copy, and it does seem to be much shorter than what I had, especially for pderivative_monomial_mul, and it checks much faster.

pderivative_add is also trivial with this approach. As pderivative_add and pderivative_mul are the main results of the PR, I think your approach may be better.

Upon further investigation, finsupp.nat_sub_apply exists, so subtraction of finsupps in this case can be reduced to subtraction of nats, so that's not (or rather, less of) an issue.

As a side note, rw foo_prep h works in foo with h : ¬⇑u v = 0, No hacking of by_cases required.

[semorrison]

Sounds great! Looking forward to seeing the update. Did you get foo_prep to work without having to use ne.def? That was the part I was upset about.

[shingtaklam1324]

I think so? I just derived that (u v) is (succ something) using cases (u v), {contradiction}. There's probably a better way.

lemma foo_prep {v : S} {u u' : S →₀ ℕ} (h : u v ≠ 0) :
  u - single v 1 + u' = u + u' - single v 1 :=
begin
  ext f,
  rw [add_apply, nat_sub_apply, nat_sub_apply, add_apply],
  by_cases h : v = f,
  { rw [←h, single_eq_same], cases (u v), {contradiction},
    rw nat.succ_sub_one, rw nat.succ_add, rw nat.succ_sub_one,
  },
  rw single_eq_of_ne h, simp
end

Also if I'm to go ahead with this, I'd need to either rename foo bar fooprep and barprep or figure out how to make lemmas which are not exported in Lean. I don't think foo and bar are generally applicable to many scenarios, so I think I'll need to find how to make them hidden.

[semorrison]

foo_prep (obviously with a better name, e.g. sub_single_add) should go in data/finsupp.
foo should stay local to this proof, as it's not good for anything else. I would just name it monomial_sub_single_add, but not make it private.

[shingtaklam1324]

foo_prep (obviously with a better name, e.g. sub_single_add) should go in data/finsupp.
foo should stay local to this proof, as it's not good for anything else. I would just name it monomial_sub_single_add, but not make it private.

Sorry, I didn't see your comment at the time. I just labelled it private as well and left it there. Is it something that would be useful elsewhere?

[shingtaklam1324]

Also, would something like

lemma pderivative_eq_zero_of_not_mem_vars {v : S} {f : mv_polynomial S R} (h : v ∉ f.vars) :
  pderivative v f = 0 := sorry

be nice to have? I managed to prove it in the case when f is a monomial u a, but that uses u.support, and there isn't something like that for mv_polynomials in general, just vars and degree_of, so I haven't been able to prove it in the more general case.

[jcommelin]

Yes, that seems like a useful lemma to me.

[jcommelin]

Yes, that's always painful... I don't know how to fix this off the top of my head.

[semorrison]

Can you just rewrite the polynomial f as a sum over its support of singles, then use the fact you've already proved linearity to reduce to the monomial case?

[semorrison]

To do this, you'll need to write a wrapper around finsupp.sum_single for mv_polynomial. You may also need to dress up pderivative as an add_monoid_hom, so that you can use add_monoid_hom.map_sum. If you prefer this can happen in a separate PR.

[jcommelin]

Can you just rewrite the polynomial f as a sum over its support of singles, then use the fact you've already proved linearity to reduce to the monomial case?

There is a lemma polynomial.as_sum which could be helpful here. But it doesn't give you monomial bla bla but C (coeff _) * X ^ bla. Maybe this lemma should use monomial instead.

[shingtaklam1324]

I've taken a look at polynomial.as_sum, and that uses (range (p.nat_degree + 1)).sum, but there isn't really something equivalent for mv_polynomial.

[kbuzzard]

Can you just rewrite the polynomial f as a sum over its support of singles, then use the fact you've already proved linearity to reduce to the monomial case?

There is a lemma polynomial.as_sum which could be helpful here. But it doesn't give you monomial bla bla but C (coeff _) * X ^ bla. Maybe this lemma should use monomial instead.

mv_polynomial is spanned as an add_comm_group by the monomials (in the sense of mv_polynomial.lean): I think monomials should be thought of as the fundamental building blocks in this set-up, rather than C(a)*X^blah.

[semorrison]

I've tidied up the aux lemmas a little. Let's do this other lemma in a separate PR; no need to hold up the work here!

I'll try to write a mv_polynomial.as_sum for you in a moment.

[semorrison]

Presumably you'll see this on zulip, but just in case: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/pderivative