not rlly complete

a.lean

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Analysis.Asymptotics.Asymptotics
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Data.Finset.Basic
import Mathlib.Data.List.Intervals
import Mathlib.Data.Nat.Interval
import Mathlib.Data.Nat.Prime
import Mathlib.Data.Nat.Squarefree
import Mathlib.Data.Real.Basic
import Mathlib.Init.Data.Bool.Lemmas
import Mathlib.NumberTheory.ArithmeticFunction
import Mathlib.Order.LocallyFinite
import Mathlib.Order.RelClasses

import LakeSeave.Utils
import LakeSeave.Moebius

open Nat Finset BigOperators ArithmeticFunction

variable (z x n : ℕ)

local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)

/- Time to choose conventions for < and ≤ and > and ≥
   Pretty sure I will regret these arbitrary choices soon but yeah. -/

def smooth : Prop := ∀ p ∈ n.factors, p < z

def rough : Prop := ∀ p ∈ n.factors, p ≥ z

instance : ∀ z, DecidablePred (smooth z) := by unfold smooth ; infer_instance

instance : ∀ z, DecidablePred (rough z) := by unfold rough ; infer_instance

theorem smooth_zero : smooth z 0 := fun _ h ↦ absurd h $ List.not_mem_nil _

theorem rough_zero : rough z 0 := fun _ h ↦ absurd h $ List.not_mem_nil _

theorem smooth_one : smooth z 1 := fun _ h ↦ absurd h $ List.not_mem_nil _

theorem rough_one : rough z 1 := fun _ h ↦ absurd h $ List.not_mem_nil _

theorem not_smooth_of_rough (h : rough z n) (h₀ : n ≠ 0) (h₁ : n ≠ 1) : ¬smooth z n := by
  intro h'
  have : n.factors ≠ [] := (factors_eq_nil _).not.mpr $ not_or.mpr ⟨h₀, h₁⟩
  let ⟨p, hp⟩ := List.exists_mem_of_ne_nil (factors n) this
  exact not_lt_of_ge (h p hp) (h' p hp)

theorem not_rough_of_smooth (h : smooth z n) (h₀ : n ≠ 0) (h₁ : n ≠ 1) : ¬rough z n := by
  intro h'
  have : n.factors ≠ [] := (factors_eq_nil _).not.mpr $ not_or.mpr ⟨h₀, h₁⟩
  let ⟨p, hp⟩ := List.exists_mem_of_ne_nil (factors n) this
  exact not_lt_of_ge (h' p hp) (h p hp)

def prime_Icc (a b : ℕ) := (Icc a b).filter Nat.Prime

def prime_Ico (a b : ℕ) := (Ico a b).filter Nat.Prime

lemma mem_prime_Icc : p ∈ prime_Icc a b ↔ p ∈ Icc a b ∧ p.Prime := by rw [prime_Icc, mem_filter]

lemma mem_prime_Ico : p ∈ prime_Ico a b ↔ p ∈ Ico a b ∧ p.Prime := by rw [prime_Ico, mem_filter]

lemma right_not_mem_prime_Ico : b ∉ prime_Ico a b :=
  fun h ↦ right_not_mem_Ico (mem_filter.mp h).left

lemma prime_of_mem_prime_Icc {a b n : ℕ} (h : n ∈ prime_Icc a b) : n.Prime := by
  rw [prime_Icc, mem_filter] at h
  exact h.right

lemma prime_of_mem_prime_Ico {a b n : ℕ} (h : n ∈ prime_Ico a b) : n.Prime := by
  rw [prime_Ico, mem_filter] at h
  exact h.right

lemma prime_Ico_succ_right : prime_Ico a b.succ = prime_Icc a b := by
  rw [prime_Ico, Ico_succ_right, prime_Icc]

lemma prime_Ico_succ_right_eq_insert_prime_Ico (h : a ≤ b) :
    prime_Ico a b.succ = if b.Prime then insert b (prime_Ico a b) else prime_Ico a b := by
  rw [prime_Ico, Ico_succ_right_eq_insert_Ico h, filter_insert]
  rfl

/- Number of z-smooth numbers ≤ x -/
def Ψ := ((Icc 1 x).filter (smooth z)).card
alias num_smooth := Ψ

/- Number of z-rough numbers ≤ x -/
def Φ := ((Icc 1 x).filter (rough z)).card
alias num_rough := Φ

/- Primorial of primes < z -/
def Pr := ∏ p in prime_Ico 1 z, p

lemma Pr_succ : Pr z.succ = if z.Prime then z * Pr z else Pr z := by
  by_cases hz : 1 ≤ z
  · rw [Pr, prime_Ico_succ_right_eq_insert_prime_Ico hz]
    by_cases hz' : z.Prime
    · simp only [hz', ite_true, prod_insert $ right_not_mem_prime_Ico, Pr]
    · simp only [hz', ite_false, Pr]
  · rw [lt_one_iff.mp (not_le.mp hz)]
    trivial

lemma Pr_ne_zero : Pr z ≠ 0 := by
  rw [Pr, Finset.prod_ne_zero_iff]
  exact fun _ ha ↦ Nat.pos_iff_ne_zero.mp (mem_Ico.mp (mem_prime_Ico.mp ha).left).left

lemma prime_dvd_Pr_iff (hd : d.Prime) : d ∣ Pr z ↔ d ∈ Ico 1 z := by
  constructor <;> intro h
  · exact mem_of_mem_filter d
      $ prime_dvd_prod_prime_of_mem _ hd _ (fun _ ↦ prime_of_mem_prime_Ico) h
  · exact dvd_prod_of_mem _ $ mem_filter.mpr ⟨h, hd⟩

lemma Pr_squarefree : Squarefree (Pr z) := by
  apply squarefree_prod_coprime_squarefree
  · intro a ha
    exact (mem_prime_Ico.mp ha).right.squarefree
  · intro a ha b hb h
    exact (coprime_primes (mem_prime_Ico.mp ha).right (mem_prime_Ico.mp hb).right).mpr h

/- (Deduplicated) Prime divisors of Pr z -/
lemma Pr_prime_divisors : (Pr z).factors.toFinset = prime_Ico 1 z := by
  ext t
  rw [List.mem_toFinset, mem_prime_Ico, mem_factors (Pr_ne_zero _)]
  constructor <;> intro ⟨h₁, h₂⟩
  · exact ⟨(prime_dvd_Pr_iff _ h₁).mp h₂, h₁⟩
  · exact ⟨h₂, (prime_dvd_Pr_iff _ h₂).mpr h₁⟩

lemma Pr_factors_nodup : List.Nodup (factors (Pr z)) :=
  (Nat.squarefree_iff_nodup_factors $ Pr_ne_zero _).mp $ Pr_squarefree _

/- Factors of Pr z -/
lemma Pr_factors : (Pr z).factors = (List.Ico 1 z).filter Nat.Prime := by
  apply @List.eq_of_perm_of_sorted _ LE.le
  /- permutation -/
  · apply List.perm_of_nodup_nodup_toFinset_eq
    /- nodup (Pr z).factors -/
    · exact Pr_factors_nodup _
    /- nodup prime_Ico 1 z -/
    · exact List.Nodup.filter _ $ List.Ico.nodup _ _
    /- toFinset equal -/
    · rw [Pr_prime_divisors, List.toFinset_filter_Ico, prime_Ico]
  · exact factors_sorted (Pr z)
  · unfold List.Sorted
    apply List.Pairwise.filter _
    rw [List.Ico]
    apply List.pairwise_le_range'

lemma mem_Pr_factors : p ∈ (Pr z).factors ↔ p ∈ prime_Ico 1 z := by
  rw [Pr_factors, List.mem_filter, mem_prime_Ico, List.Ico.mem, mem_Ico, decide_eq_true_eq]

lemma Pr_factorization (p : ℕ) :
    (Pr z).factorization p = if p ∈ prime_Ico 1 z then 1 else 0 := by
  simp_rw [mem_prime_Ico]
  by_cases hp : p.Prime
  · simp only [hp, ite_true, true_and]
    by_cases hp' : p ∈ Ico 1 z
    · simp only [hp', ite_true]
      rw [←Nat.factors_count_eq]
      apply List.count_eq_one_of_mem
      · exact Pr_factors_nodup z
      · rw [Pr_factors, List.mem_filter]
        exact ⟨hp', decide_eq_true hp⟩
    · simp only [hp', ite_false]
      rw [←Nat.factors_count_eq, Pr_factors]
      apply List.count_eq_zero_of_not_mem
      exact fun h ↦ hp' (List.mem_filter.mp h).left
  · simp only [hp, false_and, ite_false]
    rw [←Nat.factors_count_eq, Pr_factors]
    simp_rw [and_false]
    apply List.count_eq_zero_of_not_mem
    exact fun h ↦ hp $ (decide_eq_true_iff _).mp (List.mem_filter.mp h).right

lemma Pr_factorization' (p : ℕ) (hp : p ∈ (Pr z).factorization.support) :
    (Pr z).factorization p = 1 := by
  replace hp := (mem_Pr_factors _).mp $ factor_iff_mem_factorization.mp hp
  simp only [Pr_factorization, hp, ite_true]

lemma Pr_factorization_support : (Pr z).factorization.support = prime_Ico 1 z := by
  ext p
  rw [factor_iff_mem_factorization, mem_Pr_factors]

lemma smooth_of_gcd_Pr_eq_self (h : n.gcd (Pr z) = n) : smooth z n := by
  replace h := gcd_eq_left_iff_dvd.mpr h
  intro p hp
  rw [mem_factors] at hp
  · exact (mem_Ico.mp $ (prime_dvd_Pr_iff z hp.left).mp (hp.right.trans h)).right
  · by_contra' h'
    rw [h', zero_dvd_iff] at h
    exact (Pr_ne_zero _) h

lemma gcd_Pr_eq_self_of_smooth (h : Squarefree n) (h' : smooth z n) : n.gcd (Pr z) = n := by
  apply gcd_eq_left_iff_dvd.mp
  /- If n is squarefree and z-smooth, then n divides product of primes < z -/
  rw [←prod_factors_toFinset_of_squarefree h]
  apply prod_dvd_prod_of_subset
  intro t ht
  rw [List.mem_toFinset] at ht
  rw [prime_Ico, mem_filter, mem_Ico]
  have h := prime_of_mem_factors ht
  refine ⟨⟨h.pos, h' t ht⟩, h⟩

lemma rough_of_gcd_Pr_eq_one (h : n.gcd (Pr z) = 1) : rough z n := by
  replace h := coprime_iff_gcd_eq_one.mpr h
  intro p hp
  have hp' := (mem_factors ?_).mp hp
  by_contra' hz
  · have h1 := (prime_dvd_Pr_iff z $ prime_of_mem_factors hp).mpr $ mem_Ico.mpr ⟨hp'.left.pos, hz⟩
    exact hp'.left.not_dvd_one $ h ▸ Nat.dvd_gcd (dvd_of_mem_factors hp) h1
  · by_contra' h'
    rw [h'] at hp
    exact List.not_mem_nil p hp

lemma gcd_Pr_eq_one_of_rough (h : n ≠ 0) (h' : rough z n) : n.gcd (Pr z) = 1 := by
  /- If n is z-rough, then n has no prime factors ≤ z -/
  rw [rough] at h'
  apply coprime_of_dvd
  intro p hp hp'
  specialize h' p $ (mem_factors h).mpr ⟨hp, hp'⟩
  exact fun hz ↦ not_lt_of_ge h' (mem_Ico.mp $ (prime_dvd_Pr_iff _ hp).mp hz).right

lemma squarefree_of_gcd_Pr_eq_self (h : n.gcd (Pr z) = n) : Squarefree n :=
  Squarefree.squarefree_of_dvd (gcd_eq_left_iff_dvd.mpr h) (Pr_squarefree z)

/- Taking gcd with Pr z works as a sieve.
   Note that one direction does not require squarefreeness, see `smooth_of_gcd_Pr_eq_self` -/
lemma smooth_iff_gcd_Pr_eq_self (h : Squarefree n) : n.gcd (Pr z) = n ↔ smooth z n := by
  refine ⟨smooth_of_gcd_Pr_eq_self _ _, gcd_Pr_eq_self_of_smooth _ _ h⟩

/- Refined version of `smooth_iff_gcd_Pr_eq_self`, absorbing the squarefreeness condition -/
lemma smooth_iff_gcd_Pr_eq_self' : n.gcd (Pr z) = n ↔ smooth z n ∧ Squarefree n := by
  constructor <;> intro h
  · exact ⟨smooth_of_gcd_Pr_eq_self _ _ h, squarefree_of_gcd_Pr_eq_self _ _ h⟩
  · exact (smooth_iff_gcd_Pr_eq_self _ _ h.right).mpr h.left

lemma rough_iff_gcd_Pr_eq_one (h : n ≠ 0) : n.gcd (Pr z) = 1 ↔ rough z n :=
  ⟨rough_of_gcd_Pr_eq_one _ _, gcd_Pr_eq_one_of_rough _ _ h⟩