Zulip Chat Archive

Stream: maths

Topic: golfing challenge


view this post on Zulip Johan Commelin (May 02 2020 at 17:03):

This shouldn't be so hard/long/slow...

import ring_theory.polynomial

namespace polynomial

/-- The formal derivative of polynomials, as additive homomorphism. -/
noncomputable def derivative_hom (R : Type*) [comm_semiring R] : polynomial R →+ polynomial R :=
{ to_fun := derivative,
  map_zero' := derivative_zero,
  map_add' := λ p q, derivative_add }

@[simp] lemma derivative_neg {R : Type*} [comm_ring R] (f : polynomial R) :
  derivative (-f) = -derivative f :=
(derivative_hom R).map_neg f

@[simp] lemma derivative_sub {R : Type*} [comm_ring R] (f g : polynomial R) :
  derivative (f - g) = derivative f - derivative g :=
(derivative_hom R).map_sub f g

lemma is_coprime_of_is_root_of_eval_derivative_ne_zero {R : Type*} [field R]
  (f : polynomial R) (r : R) (hf : f.is_root r) (hf' : f.derivative.eval r  0) :
  ideal.is_coprime (X - C r : polynomial R) (f / (X - C r)) :=
begin
  rw  mul_div_by_monic_eq_iff_is_root at hf,
  rw  hf at hf',
  simp only [eval_C, eval_X, add_zero, derivative_X, derivative_mul, one_mul, zero_mul,
    eval_sub, sub_zero, ne.def, derivative_sub, eval_add, eval_mul, derivative_C, sub_self] at hf',
  apply is_coprime_of_dvd,
  { push_neg, left, assume eqz,
    apply_fun polynomial.degree at eqz,
    rw polynomial.degree_X_sub_C at eqz,
    exact option.no_confusion eqz },
  { rintros a h1 h2 b, hab H,
    have : irreducible (X - C r),
    { apply polynomial.irreducible_of_degree_eq_one, exact polynomial.degree_X_sub_C _ },
    rcases (this.is_unit_or_is_unit hab) with ha|⟨b,rfl,
    { exact h1 ha },
    apply hf',
    show is_root _ _,
    rw  dvd_iff_is_root,
    refine dvd_trans b⁻¹, _⟩ H,
    rw [hab, units.mul_inv_cancel_right] }
end

end polynomial

view this post on Zulip Alex J. Best (May 02 2020 at 18:15):

Probably this can be golfed more, but heres a slightly different proof (I think?)

lemma is_coprime_of_is_root_of_eval_derivative_ne_zero {R : Type*} [field R]
  (f : polynomial R) (r : R) (hf : f.is_root r) (hf' : f.derivative.eval r  0) :
  ideal.is_coprime (X - C r : polynomial R) (f / (X - C r)) :=
begin
  have aa : (X - C r) * (f / (X - C r)) = f - (f %ₘ (X - C r))  := begin
    rw [eq_sub_iff_add_eq,  eq_sub_iff_add_eq', mod_by_monic_eq_sub_mul_div],
    exact monic_X_sub_C r,
  end,
  apply_fun derivative at aa,
  simp only [derivative_X, derivative_mul, one_mul, sub_zero, derivative_sub, mod_by_monic_X_sub_C_eq_C_eval, derivative_C] at aa,
  refine or.resolve_left (dvd_or_coprime (X - C r) (f / (X - C r)) (irreducible_of_degree_eq_one (polynomial.degree_X_sub_C r))) _,
  intro,
  apply hf',
  have : (X - C r)  derivative f := aa  (dvd_add a (dvd.intro (derivative (f / (X - C r))) rfl)),
  rw [ dvd_iff_mod_by_monic_eq_zero (monic_X_sub_C _), mod_by_monic_X_sub_C_eq_C_eval] at this,
  apply_fun coeff at this,
  convert congr_fun this 0,
  rw [coeff_C_zero],
end

view this post on Zulip Johan Commelin (May 02 2020 at 20:42):

Thanks... it's certainly shorter than what I had.

view this post on Zulip Johan Commelin (May 09 2020 at 12:25):

Feel free to turn this into a kata.

import data.nat.choose

-- Generalise this to arbitrary property that is respected by addition/multiplication:
-- example applications: sum_pos, sum_neg, ... others?
lemma dvd_sum {α : Type*} {R : Type*} [comm_ring R]
  (s : finset α) (f : α  R) (b : R) (H :  a  s, b  f a) :
  b  s.sum f :=
begin
  let t := s,
  replace H :  a  t, b  f a := H,
  have hs : s  t := finset.subset.refl s,
  revert hs,
  classical,
  apply finset.induction_on s, {simp},
  intros a s' ha IH hs',
  rw finset.insert_subset at hs',
  cases hs' with has hs',
  simp [*, dvd_add]
end

lemma coe_nat_dvd {α : Type*} [comm_ring α] (m n : ) (h : m  n) :
  (m : α)  n :=
by { rcases h with k, rfl, refine k, by norm_cast }

lemma dvd_sub_pow_of_dvd_sub (R : Type*) [comm_ring R] (p : ) [hp : fact p.prime]
  (a b : R) (h : (p : R)  a - b) (k : ) :
  (p^(k+1) : R)  a^(p^k) - b^(p^k) :=
begin
  induction k with k ih, { simpa using h }, clear h,
  simp only [nat.succ_eq_add_one],
  rcases ih with c, hc,
  rw sub_eq_iff_eq_add' at hc,
  replace hc := congr_arg (λ x, x^p) hc,
  dsimp only at hc,
  rw [ pow_mul, add_pow, finset.sum_range_succ, nat.choose_self, nat.cast_one, mul_one,
    nat.sub_self, pow_zero, mul_one] at hc,
  conv { congr, skip, rw [nat.pow_succ] },
  simp only [nat.pow_eq_pow] at hc,
  rw [hc, pow_mul, add_sub_cancel'], clear hc a,
  apply dvd_sum,
  intros i hi,
  rw finset.mem_range at hi,
  rw mul_pow,
  conv { congr, skip, congr, congr, skip, rw mul_comm },
  repeat { rw mul_assoc, apply dvd_mul_of_dvd_right }, clear c b,
  norm_cast,
  apply coe_nat_dvd,
  by_cases H : i = 0,
  { subst H,
    suffices : p ^ (k + 1 + 1)  (p ^ (k + 1)) ^ p, by simpa,
    rw  nat.pow_mul,
    apply nat.pow_dvd_pow,
    refine le_trans (add_le_add_left' $ le_add_left $ le_refl _ : k + 1 + 1  k + 1 + (k + 1)) _,
    refine le_trans (le_of_eq _) (nat.mul_le_mul_left (k+1) $ (hp.two_le : 2  p)),
    rw mul_two },
  have i_pos := nat.pos_of_ne_zero H, clear H,
  rw nat.pow_succ,
  apply mul_dvd_mul,
  { generalize H : (p^(k+1)) = b,
    have := nat.sub_pos_of_lt hi,
    conv {congr, rw  nat.pow_one b},
    apply nat.pow_dvd_pow,
    exact this },
  exact nat.prime.dvd_choose i_pos hi _
end

view this post on Zulip Johan Commelin (May 09 2020 at 12:25):

Currently it takes so long on my machine that I'm worried codewars wouldn't accept it.

view this post on Zulip Reid Barton (May 09 2020 at 12:26):

Johan Commelin said:

Feel free to turn this into a kata mathlib PR.

view this post on Zulip Johan Commelin (May 09 2020 at 12:26):

Only after it's fast enough to be a kata

view this post on Zulip Chris Hughes (May 09 2020 at 12:43):

The generalization of the first theorem is is_add_submonoid.sum_mem. Whether that's a good way to state it I don't know.

view this post on Zulip Johan Commelin (May 09 2020 at 12:44):

But it might be a good way to prove it.

view this post on Zulip Johan Commelin (May 09 2020 at 12:45):

On the other hand, the other suggestions don't really follow from sum_mem, I guess. Things like sum_pos and sum_neg

view this post on Zulip Johan Commelin (May 09 2020 at 12:46):

Well, they do, but I don't think the relevant submonoids have been set up.

view this post on Zulip Chris Hughes (May 09 2020 at 13:19):

sum_pos and sum_neg actually need is_add_subsemigroup.sum_mem_of_ne_empty which doesn't exist.

view this post on Zulip Johan Commelin (May 09 2020 at 13:20):

sum_nonpos and sum_nonneg...

view this post on Zulip Kenny Lau (May 09 2020 at 14:07):

import data.nat.choose algebra.geom_sum ring_theory.ideals

-- Generalise this to arbitrary property that is respected by addition/multiplication:
-- example applications: sum_pos, sum_neg, ... others?
lemma dvd_sum {α : Type*} {R : Type*} [comm_ring R]
  (s : finset α) (f : α  R) (b : R) (H :  a  s, b  f a) :
  b  s.sum f :=
begin
  classical, revert H,
  apply finset.induction_on s,
  { intros, exact dvd_zero b, },
  intros a s has ih H,
  rw finset.forall_mem_insert at H,
  rw finset.sum_insert has,
  exact dvd_add H.1 (ih H.2)
end

lemma coe_nat_dvd {α : Type*} [comm_ring α] (m n : ) (h : m  n) :
  (m : α)  n :=
by { rcases h with k, rfl, refine k, by norm_cast }

instance {α : Type*} [comm_ring α] (I : ideal α) : is_ring_hom (ideal.quotient.mk I) :=
(ideal.quotient.mk_hom I).is_ring_hom

lemma mk_eq_mk_hom {α : Type*} [comm_ring α] (I : ideal α) (x : α) :
  ideal.quotient.mk I x = ideal.quotient.mk_hom I x :=
rfl

theorem ring_hom.map_geom_series₂ {α β : Type*} [comm_ring α] [comm_ring β] (x y : α) (n : )
  (f : α →+* β) : f (geom_series₂ x y n) = geom_series₂ (f x) (f y) n :=
by { rw [geom_series₂_def, geom_series₂_def,  finset.sum_hom _ f],
    simp_rw [f.map_mul, f.map_pow] }

theorem geom_series₂_self {α : Type*} [comm_ring α] (x : α) (n : ) :
  geom_series₂ x x n = n * x ^ (n-1) :=
calc  (finset.range n).sum (λ i, x ^ i * x ^ (n - 1 - i))
    = (finset.range n).sum (λ i, x ^ (i + (n - 1 - i))) : by simp_rw [ pow_add]
... = (finset.range n).sum (λ i, x ^ (n - 1)) : finset.sum_congr rfl
  (λ i hi, congr_arg _ $ nat.add_sub_cancel' $ nat.le_pred_of_lt $ finset.mem_range.1 hi)
... = add_monoid.smul (finset.range n).card (x ^ (n - 1)) : finset.sum_const _
... = n * x ^ (n - 1) : by rw [finset.card_range, add_monoid.smul_eq_mul]


lemma dvd_sub_pow_of_dvd_sub (R : Type*) [comm_ring R] (p : ) [hp : fact p.prime]
  (a b : R) (h : (p : R)  a - b) (k : ) :
  (p^(k+1) : R)  a^(p^k) - b^(p^k) :=
begin
  induction k with k ih,
  { rwa [pow_one, nat.pow_zero, pow_one, pow_one] },
  rw [nat.pow_succ, pow_mul, pow_mul,  geom_sum₂_mul, pow_succ],
  refine mul_dvd_mul _ ih,
  rw [ ideal.mem_span_singleton,  ideal.quotient.eq, mk_eq_mk_hom, mk_eq_mk_hom] at h,
  rw [ ideal.mem_span_singleton,  ideal.quotient.eq_zero_iff_mem, mk_eq_mk_hom,
      ring_hom.map_geom_series₂, ring_hom.map_pow, ring_hom.map_pow, h, geom_series₂_self,
       ring_hom.map_pow,  ring_hom.map_pow,  add_monoid.smul_eq_mul],
  erw [ (ideal.quotient.mk_hom (ideal.span ({p} : set R))).to_add_monoid_hom.map_smul,
      ideal.quotient.eq_zero_iff_mem],
  rw add_monoid.smul_eq_mul,
  exact ideal.mul_mem_right _ (ideal.mem_span_singleton.2 $ dvd_refl (p : R))
end

view this post on Zulip Kenny Lau (May 09 2020 at 14:08):

@Johan Commelin the trick is to use geom_series\2 and quotient ring

view this post on Zulip Johan Commelin (May 09 2020 at 14:12):

@Kenny Lau Sounds good. Thanks! Wanna make a PR?

view this post on Zulip Kenny Lau (May 09 2020 at 14:12):

go ahead

view this post on Zulip Johan Commelin (May 09 2020 at 14:32):

@Kenny Lau Golfed further:

lemma dvd_sub_pow_of_dvd_sub (R : Type*) [comm_ring R] (p : ) [hp : fact p.prime]
  (a b : R) (h : (p : R)  a - b) (k : ) :
  (p^(k+1) : R)  a^(p^k) - b^(p^k) :=
begin
  induction k with k ih,
  { rwa [pow_one, nat.pow_zero, pow_one, pow_one] },
  rw [nat.pow_succ, pow_mul, pow_mul,  geom_sum₂_mul, pow_succ],
  refine mul_dvd_mul _ ih,
  have : (p : R)  ideal.span ({p} : set R), { rw ideal.mem_span_singleton },
  rw [ ideal.quotient.eq_zero_iff_mem, mk_eq_mk_hom, ring_hom.map_nat_cast] at this,
  rw [ ideal.mem_span_singleton,  ideal.quotient.eq, mk_eq_mk_hom, mk_eq_mk_hom] at h,
  rw [ ideal.mem_span_singleton,  ideal.quotient.eq_zero_iff_mem, mk_eq_mk_hom,
      ring_hom.map_geom_series₂, ring_hom.map_pow, ring_hom.map_pow, h, geom_series₂_self,
      this, zero_mul],
end

view this post on Zulip Kenny Lau (May 09 2020 at 14:33):

@Johan Commelin aha, you applied the quotient philosophy even more

view this post on Zulip Kevin Buzzard (May 09 2020 at 15:03):

Wow, from a monster it's now at de Bruijn index 1!

view this post on Zulip Johan Commelin (May 09 2020 at 15:11):

#2640

view this post on Zulip Johan Commelin (May 09 2020 at 16:57):

Unexpected side effect: the proof doesn't use that p is prime (-;

view this post on Zulip Johan Commelin (May 09 2020 at 16:58):

Maybe not so unexpected after all. But that hypothesis certainly existed in my mental copy of this lemma (-;

view this post on Zulip Johan Commelin (May 09 2020 at 16:58):

Linters are good.

view this post on Zulip Kenny Lau (May 09 2020 at 17:03):

wow that's unexpected

view this post on Zulip Mario Carneiro (May 09 2020 at 17:03):

it's probably because you called the variable p

view this post on Zulip Johan Commelin (May 09 2020 at 17:04):

It's called n now (-;

view this post on Zulip Reid Barton (May 09 2020 at 17:07):

I sort of think it should still be called p

view this post on Zulip Reid Barton (May 09 2020 at 17:07):

I had no idea this was true for p not prime and I would certainly expect to see p in the theorem statement

view this post on Zulip Johan Commelin (May 09 2020 at 17:07):

Oops... I didn't update the theorem name...

view this post on Zulip Johan Commelin (May 09 2020 at 17:09):

@Reid Barton You can prove the special case, if you want :grinning_face_with_smiling_eyes:

view this post on Zulip Reid Barton (May 09 2020 at 17:10):

I don't need the special case, I just want the theorem statement to read as expected, with the prime p hypothesis mysteriously absent.

view this post on Zulip Johan Commelin (May 09 2020 at 17:15):

Sure, was only joking

view this post on Zulip Kevin Buzzard (May 09 2020 at 17:24):

Yeah I like that style, it's kind of an in joke

view this post on Zulip Kevin Buzzard (May 09 2020 at 17:25):

For 2 you can beat this result, 2^(k+2) divides the 2^kth power if k>=1.

view this post on Zulip Johan Commelin (May 09 2020 at 17:26):

And does this get used somewhere?

view this post on Zulip Kevin Buzzard (May 09 2020 at 17:26):

And the pair (1,5) show that this is tight for all k>=1

view this post on Zulip Kevin Buzzard (May 09 2020 at 17:26):

Analogous to the pair (1,p+1) showing its tight for odd primes

view this post on Zulip Johan Commelin (May 09 2020 at 17:27):

You mean for arbitrary p ≥ 3?

view this post on Zulip Johan Commelin (May 09 2020 at 17:27):

For p = 1 you can do even better than for p = 2!!!

view this post on Zulip Kevin Buzzard (May 09 2020 at 17:27):

Yes you can use it to demonstrate that 1+p resp 5 have large multiplicative orders mod p^n, and determine their order precisely

view this post on Zulip Johan Commelin (May 09 2020 at 17:28):

And is this fact about 5 used somewhere?

view this post on Zulip Kevin Buzzard (May 09 2020 at 17:28):

This gives you the structure theorem for the units of Z/p^nZ and then by CRT the structure of the units in Z/NZ

view this post on Zulip Johan Commelin (May 09 2020 at 17:28):

Aah, I see

view this post on Zulip Kevin Buzzard (May 09 2020 at 17:29):

Yes it tells you that the units in Z/32 have an element of order 8 and with that and the elements +-17 you know the structure of the group modulo the structure theorem

view this post on Zulip Kevin Buzzard (May 09 2020 at 17:29):

Which you can probably prove by hand here

view this post on Zulip Johan Commelin (May 09 2020 at 17:29):

dec_trivial?

view this post on Zulip Johan Commelin (May 09 2020 at 17:30):

Lol, just kidding

view this post on Zulip Kevin Buzzard (May 09 2020 at 17:30):

If only

view this post on Zulip Johan Commelin (May 09 2020 at 17:30):

But were you aware that this lemma doesn't need the primality assumption?

view this post on Zulip Kevin Buzzard (May 09 2020 at 17:30):

It's come_on_lean you need

view this post on Zulip Kevin Buzzard (May 09 2020 at 17:30):

No I didn't know

view this post on Zulip Johan Commelin (May 09 2020 at 17:30):

Would that give you a speed up for the structure theorem?

view this post on Zulip Kevin Buzzard (May 09 2020 at 17:30):

But everything I said needed it

view this post on Zulip Johan Commelin (May 09 2020 at 17:30):

Ok, I see

view this post on Zulip Johan Commelin (May 09 2020 at 17:31):

Well, we can make those tightness bounds into an issue for later

view this post on Zulip David Wärn (May 09 2020 at 17:42):

I think this is made more precise by the "Lifting the Exponent lemma", i.e. "vp(anbn)=vp(ab)+vp(n)v_p(a^n - b^n) = v_p(a-b) + v_p(n) for p odd prime with p dividing aba-b but not a or b"

view this post on Zulip Johan Commelin (May 09 2020 at 17:44):

But that needs the primality assumption...

view this post on Zulip David Wärn (May 09 2020 at 17:47):

Probably one direction does, yes

view this post on Zulip David Wärn (May 09 2020 at 17:48):

Or maybe both... Not sure


Last updated: May 19 2021 at 02:10 UTC