Factorisation of squarefree naturals

Stream: Is there code for X?

[Yaël Dillies]

I'm having trouble putting the pieces together. Do we have anything related to the prime factorisation of a squarefree natural?

import Mathlib.Algebra.Squarefree
import Mathlib.RingTheory.Int.Basic

open scoped BigOperators

namespace Nat
variable {m n : ℕ} {s : Finset ℕ}

lemma prod_support_factorization_of_squarefree (hn : Squarefree n) :
    ∏ p in (factorization n).support, p = n := by
  sorry

lemma support_factorization_prod (hs : ∀ p ∈ s, p.Prime) :
    (factorization $ ∏ p in s, p).support = s := by
  sorry

lemma support_factorization_div_gcd (hm : Squarefree m) (hn : Squarefree n) :
    (factorization $ m / m.gcd n).support =
      (factorization m).support \ (factorization n).support := by
  sorry

end Nat

[Yaël Dillies]

This is probably a question for @Eric Rodriguez

[Bolton Bailey]

I feel like the first lemma is true for more than just squarefree numbers

[Yaël Dillies]

No. (factorization 4).support = {2}.

[Bolton Bailey]

Oh is it not Nat.factorization? Sorry.

[Bolton Bailey]

docs#Nat.factorization_prod_pow_eq_self would be the lemma for Nat.factorization

[Yaël Dillies]

It is. And Nat.factorization 4 is the Finsupp with value 2 at 2 and 0 elsewhere, so its support is {2}.

[Bolton Bailey]

Oh I understand now, it's without the exponent, thanks.

[Yaël Dillies]

Also we really need primeFactors : Finset ℕ := (Nat.factorization n).support.

[Yaël Dillies]

Let me write that quickly.

[Arend Mellendijk]

See also https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/toFinsetFactors/near/391003733

[Arend Mellendijk]

There's docs#Nat.prod_factors_toFinset_of_squarefree for the first one

[Yaël Dillies]

I got the first two. What about the third?

[Eric Rodriguez]

in your MWE it's picking up docs#factorization, btw

[Yaël Dillies]

Are they not equal, actually?

[Eric Rodriguez]

probably? api is disjoint though

[Eric Rodriguez]

@loogle factorization, Nat.factorization

[loogle]

:shrug: nothing found

[Yaël Dillies]

Ugh, time for a refactor, I guess.

[Eric Rodriguez]

i mean but then you ruin the fact that Nat.factorization is computable

[Eric Rodriguez]

i take that back and instead say computable efficiently

[Eric Rodriguez]

I'm not sure if factorization runs in a decent time for e.g. the Gaussian integers

[Eric Rodriguez]

noncomputable, never mind

[Yaël Dillies]

Yeah, it's a Finsupp

[Eric Rodriguez]

still computable, we don't have the lean3 poisoning

[Yaël Dillies]

It's not even like you can evaluate it (there's currently no representation for Finsupp). If you want decent pretty-printing results, you should use docs#Nat.factors.

[Eric Rodriguez]

image.png

[Eric Rodriguez]

@Eric Wieser made this recently iirc

[Yaël Dillies]

I was not made aware!

[Eric Wieser]

Note that the notation it prints isn't computable!

[Eric Wieser]

So you can't actually paste it and evaluate it, but you can paste it for use in a proof

[Eric Wieser]

The new notation should be visible in things like docs#Finsupp.single_add

[Eric Wieser]

Lol I guess not, weird

[Yaël Dillies]

Yeah exactly. I knew you added the notation, but I understood it was input-only.

[Eric Rodriguez]

assuming example {m n : ℕ} (h : Squarefree m) : Coprime (m / gcd m n) n, here's a solution

[Eric Rodriguez]

lemma mono {α M} [CanonicallyOrderedAddMonoid M] : Monotone (Finsupp.support (α := α) (M := M) ·) := by
  intros x y h t ht
  dsimp at ht ⊢
  rw [Finsupp.le_def] at h
  rw [Finsupp.mem_support_iff, ←pos_iff_ne_zero] at ht
  exact Finsupp.mem_support_iff.mpr (ht.trans_le (h _)).ne'

lemma support_factorization_div_gcd (hm : Squarefree m) (hn : Squarefree n) :
    (Nat.factorization $ m / m.gcd n).support =
      (Nat.factorization m).support \ (Nat.factorization n).support := by
  classical
  rw [factorization_div <| gcd_dvd_left m n]
  set f := factorization m
  set g := factorization n
  set h := factorization (m.gcd n)
  apply subset_antisymm
  · rw [Finset.subset_sdiff]
    refine ⟨mono tsub_le_self, ?_⟩
    simp only
    rw [←factorization_div <| gcd_dvd_left m n]
    apply factorization_disjoint_of_coprime
    sorry
  · have : f - g ≤ f - h := by
      refine tsub_le_tsub_left ?h f
      apply (factorization_le_iff_dvd (Nat.gcd_ne_zero_left hm.ne_zero) hn.ne_zero).mpr
      exact gcd_dvd_right m n
    exact le_trans (Finsupp.subset_support_tsub) (mono this)

(adding Mathlib.Data.Nat.Factorization.Basic as an import)

[Eric Rodriguez]

I'm kind of surprised the first lemma doesn't exist

[Eric Rodriguez]

@loogle Monotone, Finsupp.support

[loogle]

:shrug: nothing found

[Notification Bot]

A message was moved from this topic to #general > Notation for Finsupp by Eric Wieser.

[Junyan Xu]

Can you remove hn : Squarefree n?

[Eric Rodriguez]

I guess so, unless my little lemma is false without that. (I really doubt it considering I slim_checked it)

[Junyan Xu]

Oh, I see that n ≠ 0 is necessary

[Yaël Dillies]

This was my proof. I defined primeFactors n as (factorization n).support.

@[simp] lemma mem_primeFactors : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := sorry

lemma primeFactors_div_gcd (hm : Squarefree m) (hn  : n ≠ 0) :
    primeFactors (m / m.gcd n) = primeFactors m \ primeFactors n := by
  ext p
  have : m / m.gcd n ≠ 0 :=
    (Nat.div_ne_zero $ gcd_ne_zero_right hn).2 $ gcd_le_left _ hm.ne_zero.bot_lt
  simp only [mem_primeFactors, ne_eq, this, not_false_eq_true, and_true, not_and, mem_sdiff,
    hm.ne_zero, hn, dvd_div_iff (gcd_dvd_left _ _)]
  refine ⟨λ hp ↦ ⟨⟨hp.1, dvd_of_mul_left_dvd hp.2⟩, λ _ hpn ↦ hp.1.not_unit $ hm _ $
    (mul_dvd_mul_right (dvd_gcd (dvd_of_mul_left_dvd hp.2) hpn) _).trans hp.2⟩, λ hp ↦
      ⟨hp.1.1, Coprime.mul_dvd_of_dvd_of_dvd ?_ (gcd_dvd_left _ _) hp.1.2⟩⟩
  rw [coprime_comm, hp.1.1.coprime_iff_not_dvd]
  exact λ hpn ↦ hp.2 hp.1.1 $ hpn.trans $ gcd_dvd_right _ _

[Yaël Dillies]

Here is where I use it (Marica-Schönheim), if you're interested: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Discrete.20correlation.20inequalities