Arithmetic.lean

theorem pow_padicValNat_le_self
    [Fact p.Prime] (hn : n ≠ 0) :
    p ^ padicValNat p n ≤ n

theorem padicValNat_le_real_logb
    [Fact p.Prime] (n : ℕ) :
    (padicValNat p n : ℝ) ≤ Real.logb p n

theorem tendsto_nat_mul_const_sub_logb_atTop
    {c : ℝ} (hc : 0 < c) :
    Tendsto (fun n : ℕ => (n : ℝ) * c - Real.logb p n) atTop atTop := by
  have hhalf : 0 < c / 2 := by positivity
  have hsmall :
      (fun n : ℕ => Real.logb (p : ℝ) (n : ℝ)) =o[atTop]
        (fun n : ℕ => (n : ℝ)) := by
    simpa [Function.comp_def] using
      (Real.isLittleO_logb_id_atTop (b := (p : ℝ))).comp_tendsto
        tendsto_natCast_atTop_atTop
  have hbound :
      ∀ᶠ n : ℕ in atTop,
        ‖Real.logb (p : ℝ) (n : ℝ)‖ ≤
          (c / 2) * ‖(n : ℝ)‖ :=
    hsmall.def hhalf
  have hle :
      (fun n : ℕ => (c / 2) * (n : ℝ)) ≤ᶠ[atTop]
        (fun n : ℕ => (n : ℝ) * c - Real.logb (p : ℝ) (n : ℝ)) := by
    filter_upwards [hbound] with n hn
    have hnnonneg : 0 ≤ (n : ℝ) := Nat.cast_nonneg n
    have hlog_le :
        Real.logb (p : ℝ) (n : ℝ) ≤ (c / 2) * (n : ℝ) := by
      calc
        Real.logb (p : ℝ) (n : ℝ) ≤
            ‖Real.logb (p : ℝ) (n : ℝ)‖ :=
          le_abs_self _
        _ ≤ (c / 2) * ‖(n : ℝ)‖ := hn
        _ = (c / 2) * (n : ℝ) := by
          rw [Real.norm_eq_abs, abs_of_nonneg hnnonneg]
    calc
      (c / 2) * (n : ℝ) =
          (n : ℝ) * c - (c / 2) * (n : ℝ) := by
        ring
      _ ≤ (n : ℝ) * c - Real.logb (p : ℝ) (n : ℝ) :=
        sub_le_sub_left hlog_le ((n : ℝ) * c)
  have hlin :
      Tendsto (fun n : ℕ => (c / 2) * (n : ℝ)) atTop atTop :=
    Tendsto.const_mul_atTop hhalf tendsto_natCast_atTop_atTop
  exact tendsto_atTop_mono' atTop hle hlin

theorem tendsto_nat_succ_mul_const_sub_logb_atTop
    {c : ℝ} (hc : 0 < c) :
    Tendsto
      (fun n : ℕ => ((n + 1 : ℕ) : ℝ) * c - Real.logb p (n + 1))
      atTop atTop := by
  simpa [Function.comp_def] using
    (tendsto_nat_mul_const_sub_logb_atTop (p := p) hc).comp
      (tendsto_add_atTop_nat 1)

theorem tendsto_nat_succ_mul_const_sub_const_mul_logb_atTop
    {c C : ℝ} (hc : 0 < c) :
    Tendsto
      (fun n : ℕ =>
        ((n + 1 : ℕ) : ℝ) * c -
          C * Real.logb (p : ℝ) ((n + 1 : ℕ) : ℝ))
      atTop atTop := by
  have hhalf : 0 < c / 2 := by positivity
  have htend :
      Tendsto (fun n : ℕ => ((n + 1 : ℕ) : ℝ)) atTop atTop :=
    tendsto_natCast_atTop_atTop.comp (tendsto_add_atTop_nat 1)
  have hsmall :
      (fun n : ℕ => C * Real.logb (p : ℝ) ((n + 1 : ℕ) : ℝ)) =o[atTop]
        (fun n : ℕ => ((n + 1 : ℕ) : ℝ)) := by
    have hlog :
        (fun n : ℕ => Real.logb (p : ℝ) ((n + 1 : ℕ) : ℝ)) =o[atTop]
          (fun n : ℕ => ((n + 1 : ℕ) : ℝ)) := by
      simpa [Function.comp_def] using
        (Real.isLittleO_logb_id_atTop (b := (p : ℝ))).comp_tendsto
          htend
    simpa using hlog.const_mul_left C
  have hbound :
      ∀ᶠ n : ℕ in atTop,
        ‖C * Real.logb (p : ℝ) ((n + 1 : ℕ) : ℝ)‖ ≤
          (c / 2) * ‖((n + 1 : ℕ) : ℝ)‖ :=
    hsmall.def hhalf
  have hle :
      (fun n : ℕ => (c / 2) * ((n + 1 : ℕ) : ℝ)) ≤ᶠ[atTop]
        (fun n : ℕ =>
          ((n + 1 : ℕ) : ℝ) * c -
            C * Real.logb (p : ℝ) ((n + 1 : ℕ) : ℝ)) := by
    filter_upwards [hbound] with n hn
    have hnnonneg : 0 ≤ ((n + 1 : ℕ) : ℝ) := Nat.cast_nonneg _
    have hlog_le :
        C * Real.logb (p : ℝ) ((n + 1 : ℕ) : ℝ) ≤
          (c / 2) * ((n + 1 : ℕ) : ℝ) := by
      calc
        C * Real.logb (p : ℝ) ((n + 1 : ℕ) : ℝ) ≤
            ‖C * Real.logb (p : ℝ) ((n + 1 : ℕ) : ℝ)‖ :=
          le_abs_self _
        _ ≤ (c / 2) * ‖((n + 1 : ℕ) : ℝ)‖ := hn
        _ = (c / 2) * ((n + 1 : ℕ) : ℝ) := by
          rw [Real.norm_eq_abs, abs_of_nonneg hnnonneg]
    calc
      (c / 2) * ((n + 1 : ℕ) : ℝ) =
          ((n + 1 : ℕ) : ℝ) * c -
            (c / 2) * ((n + 1 : ℕ) : ℝ) := by
        ring
      _ ≤ ((n + 1 : ℕ) : ℝ) * c -
          C * Real.logb (p : ℝ) ((n + 1 : ℕ) : ℝ) :=
        sub_le_sub_left hlog_le (((n + 1 : ℕ) : ℝ) * c)
  have hlin :
      Tendsto (fun n : ℕ => (c / 2) * ((n + 1 : ℕ) : ℝ)) atTop atTop :=
    Tendsto.const_mul_atTop hhalf htend
  exact tendsto_atTop_mono' atTop hle hlin

theorem tendsto_nat_mul_const_sub_padicValNat_factorial_atTop
    [Fact p.Prime] {c : ℝ} (hc : 1 < c) :
    Tendsto
      (fun n : ℕ => (n : ℝ) * c - (padicValNat p n.factorial : ℝ))
      atTop atTop := by
  have hpos : 0 < c - 1 := sub_pos.mpr hc
  have hsource :
      Tendsto (fun n : ℕ => (n : ℝ) * (c - 1)) atTop atTop := by
    simpa [mul_comm] using
      Tendsto.const_mul_atTop hpos tendsto_natCast_atTop_atTop
  have hle :
      (fun n : ℕ => (n : ℝ) * (c - 1)) ≤ᶠ[atTop]
        (fun n : ℕ =>
          (n : ℝ) * c - (padicValNat p n.factorial : ℝ)) := by
    exact Eventually.of_forall fun n => by
      have hdenNat : padicValNat p n.factorial ≤ n :=
        padicValNat_factorial_le (p := p) n
      have hden : (padicValNat p n.factorial : ℝ) ≤ (n : ℝ) :=
        Nat.cast_le.mpr hdenNat
      nlinarith
  exact tendsto_atTop_mono' atTop hle hsource

theorem padicValNat_factorial_digits
    [Fact p.Prime] (n : ℕ) :
    (p - 1) * padicValNat p n.factorial =
      Nat.ofDigits p (p.digits n) - (p.digits n).sum

theorem padicValNat_factorial_digits_sum
    [Fact p.Prime] (n : ℕ) :
    (p - 1) * padicValNat p n.factorial =
      ((p.digits n).mapIdx fun i a => a * p ^ i).sum -
        (p.digits n).sum := by
  simpa [Nat.ofDigits_eq_sum_mapIdx] using
    padicValNat_factorial_digits (p := p) n

theorem digits_sum_pos_of_ne_zero (hn : n ≠ 0) :
    0 < (p.digits n).sum

theorem sub_one_mul_padicValNat_factorial_le_sub_one
    [Fact p.Prime] (hn : n ≠ 0) :
    (p - 1) * padicValNat p n.factorial ≤ n - 1

theorem padicValNat_factorial_div_sub_one_le_inv_sub_one
    [Fact p.Prime] (hn : 1 < n) :
    (padicValNat p n.factorial : ℚ) / ((n : ℚ) - 1) ≤
      1 / ((p : ℚ) - 1)

theorem padicValNat_factorial_le_sub_one_div_sub_one_real
    [Fact p.Prime] (hn : n ≠ 0) :
    (padicValNat p n.factorial : ℝ) ≤
      ((n : ℝ) - 1) / ((p : ℝ) - 1)

theorem tendsto_nat_mul_const_sub_const_mul_padicValNat_factorial_atTop
    [Fact p.Prime] {c C : ℝ} (hC : 0 ≤ C)
    (hc : C / ((p : ℝ) - 1) < c) :
    Tendsto
      (fun n : ℕ =>
        (n : ℝ) * c - C * (padicValNat p n.factorial : ℝ))
      atTop atTop := by
  have hpNat : Nat.Prime p := Fact.out
  have hp : (1 : ℝ) < p := by
    exact_mod_cast hpNat.one_lt
  have hpden : 0 < (p : ℝ) - 1 := by
    linarith
  have hdelta : 0 < c - C / ((p : ℝ) - 1) := sub_pos.mpr hc
  have hsource :
      Tendsto
        (fun n : ℕ => (n : ℝ) * (c - C / ((p : ℝ) - 1)))
        atTop atTop := by
    simpa [mul_comm] using
      Tendsto.const_mul_atTop hdelta tendsto_natCast_atTop_atTop
  have hle :
      (fun n : ℕ => (n : ℝ) * (c - C / ((p : ℝ) - 1))) ≤ᶠ[atTop]
        (fun n : ℕ =>
          (n : ℝ) * c - C * (padicValNat p n.factorial : ℝ)) := by
    filter_upwards [eventually_ge_atTop 1] with n hn
    have hn0 : n ≠ 0 := by omega
    have hfac :=
      padicValNat_factorial_le_sub_one_div_sub_one_real
        (p := p) (n := n) hn0
    have hCfac :
        C * (padicValNat p n.factorial : ℝ) ≤
          C * (((n : ℝ) - 1) / ((p : ℝ) - 1)) :=
      mul_le_mul_of_nonneg_left hfac hC
    have hCp_nonneg : 0 ≤ C / ((p : ℝ) - 1) :=
      div_nonneg hC hpden.le
    have hden_bound :
        C * (((n : ℝ) - 1) / ((p : ℝ) - 1)) ≤
          (n : ℝ) * (C / ((p : ℝ) - 1)) := by
      calc
        C * (((n : ℝ) - 1) / ((p : ℝ) - 1)) =
            ((n : ℝ) - 1) * (C / ((p : ℝ) - 1)) := by
          ring
        _ ≤ (n : ℝ) * (C / ((p : ℝ) - 1)) :=
          mul_le_mul_of_nonneg_right (by linarith) hCp_nonneg
    calc
      (n : ℝ) * (c - C / ((p : ℝ) - 1)) =
          (n : ℝ) * c - (n : ℝ) * (C / ((p : ℝ) - 1)) := by
        ring
      _ ≤ (n : ℝ) * c - C * (padicValNat p n.factorial : ℝ) := by
        linarith [hCfac.trans hden_bound]
  exact tendsto_atTop_mono' atTop hle hsource

theorem exp_higher_term_integer_valuation_gt
    [Fact p.Prime] {n : ℕ} (hn : 2 ≤ n) {m : ℤ} (hm : 2 ≤ m) :
    m < (n : ℤ) * m - (padicValNat p n.factorial : ℤ)

theorem exp_higher_term_integer_valuation_gt_scaled
    [Fact p.Prime] {n e : ℕ} (hn : 2 ≤ n) {m : ℤ}
    (hm : (e : ℚ) / ((p : ℚ) - 1) < (m : ℚ)) :
    m < (n : ℤ) * m - (e : ℤ) * (padicValNat p n.factorial : ℤ)

theorem padicValNat_div_sub_one_le_inv_sub_one
    [Fact p.Prime] (hn : 1 < n) :
    (padicValNat p n : ℚ) / ((n : ℚ) - 1) ≤
      1 / ((p : ℚ) - 1)

theorem padicValNat_lt_sub_one_mul_of_inv_sub_one_lt
    [Fact p.Prime] (hn : 1 < n) {c : ℚ}
    (hc : 1 / ((p : ℚ) - 1) < c) :
    (padicValNat p n : ℚ) < ((n : ℚ) - 1) * c

theorem sub_padicValNat_pos_of_inv_sub_one_lt
    [Fact p.Prime] (hn : 1 < n) {c : ℚ}
    (hc : 1 / ((p : ℚ) - 1) < c) :
    0 < (n : ℚ) * c - (padicValNat p n : ℚ)

theorem log_higher_term_integer_valuation_gt
    [Fact p.Prime] {n : ℕ} (hn : 2 ≤ n) {m : ℤ}
    (hm : 1 / ((p : ℚ) - 1) < (m : ℚ)) :
    m < (n : ℤ) * m - (padicValNat p n : ℤ)

theorem log_higher_term_integer_valuation_gt_scaled
    [Fact p.Prime] {n e : ℕ} (hn : 2 ≤ n) {m : ℤ}
    (hm : (e : ℚ) / ((p : ℚ) - 1) < (m : ℚ)) :
    m < (n : ℤ) * m - (e : ℤ) * (padicValNat p n : ℤ)

theorem nat_div_gcd_eq_one_of_dvd {e e' : ℕ}
    (he : 0 < e) (hdiv : e ∣ e') :
    e / Nat.gcd e e' = 1

theorem nat_lcm_div_right_eq_div_gcd {a b : ℕ} (hb : 0 < b) :
    Nat.lcm a b / b = a / Nat.gcd a b

theorem nat_lcm_div_left_eq_div_gcd {a b : ℕ} (ha : 0 < a) :
    Nat.lcm a b / a = b / Nat.gcd a b

theorem nat_div_gcd_dvd_of_lcm_dvd_mul_left {a b c : ℕ}
    (ha : 0 < a) (hdiv : Nat.lcm a b ∣ a * c) :
    b / Nat.gcd a b ∣ c

theorem nat_div_gcd_dvd_of_lcm_dvd_mul_right {a b c : ℕ}
    (hb : 0 < b) (hdiv : Nat.lcm a b ∣ c * b) :
    a / Nat.gcd b a ∣ c

theorem nat_eq_div_gcd_of_right_mul_eq_lcm {a b c : ℕ}
    (hb : 0 < b) (h : b * c = Nat.lcm a b) :
    c = a / Nat.gcd a b

theorem nat_eq_div_gcd_of_left_mul_eq_lcm {a b c : ℕ}
    (ha : 0 < a) (h : a * c = Nat.lcm a b) :
    c = b / Nat.gcd a b

theorem nat_dvd_div_gcd_of_right_mul_dvd_lcm {a b c : ℕ}
    (hb : 0 < b) (h : b * c ∣ Nat.lcm a b) :
    c ∣ a / Nat.gcd a b

theorem nat_dvd_div_gcd_of_left_mul_dvd_lcm {a b c : ℕ}
    (ha : 0 < a) (h : a * c ∣ Nat.lcm a b) :
    c ∣ b / Nat.gcd a b

theorem nat_abhyankar_quotient_eq_of_right_mul_eq_lcm {e e' eTop : ℕ}
    (he' : 0 < e') (h : e' * eTop = Nat.lcm e e') :
    eTop = e / Nat.gcd e e'

theorem nat_abhyankar_quotient_dvd_of_right_mul_dvd_lcm {e e' eTop : ℕ}
    (he' : 0 < e') (h : e' * eTop ∣ Nat.lcm e e') :
    eTop ∣ e / Nat.gcd e e'

theorem nat_abhyankar_quotient_eq_one_of_dvd {e e' : ℕ}
    (he : 0 < e) (hdiv : e ∣ e') :
    e / Nat.gcd e e' = 1

theorem nat_abhyankar_index_eq_one_of_right_mul_eq_lcm_of_dvd
    {e e' eTop : ℕ} (he : 0 < e) (he' : 0 < e')
    (hdiv : e ∣ e') (h : e' * eTop = Nat.lcm e e') :
    eTop = 1