phiRungPrime

formal source

  59-/
  60
  61/-- The phi-rung of a prime `p`: the integer floor of `log_φ p`. -/
  62def phiRungPrime (p : ℕ) : ℤ :=
  63  Int.floor (Real.log (p : ℝ) / Real.log phi)
  64
  65/-- The phi-rung extended completely additively to all positive integers.
  66
  67    For `n ≥ 1`, this is `Σ_p v_p(n) · phiRungPrime(p)`, where `v_p`
  68    is the `p`-adic valuation. -/
  69def phiRung (n : ℕ) : ℤ :=
  70  (Nat.factorization n).sum (fun p k => k * phiRungPrime p)
  71
  72/-- `phiRung(1) = 0` (the empty product). -/
  73@[simp] theorem phiRung_one : phiRung 1 = 0 := by
  74  unfold phiRung
  75  simp [Nat.factorization_one]
  76
  77/-- `phiRung(0) = 0` by convention (factorization of 0 is the zero
  78    finsupp). -/
  79@[simp] theorem phiRung_zero : phiRung 0 = 0 := by
  80  unfold phiRung
  81  simp [Nat.factorization_zero]
  82
  83/-- The phi-rung at a prime: `phiRung p = phiRungPrime p`. -/
  84theorem phiRung_prime {p : ℕ} (hp : Nat.Prime p) :
  85    phiRung p = phiRungPrime p := by
  86  unfold phiRung
  87  rw [Nat.Prime.factorization hp]
  88  simp
  89
  90/-- Multiplicativity (completely additive form): for positive `m, n`,
  91    `phiRung (m · n) = phiRung m + phiRung n`. -/
  92theorem phiRung_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :