perf(Algebra/IsPrimePow): speed up decidability for Nat IsPrimePow (#30093)

Previously, this decidability instance was defined using `isPrimePow_nat_iff_bounded`, which (as I understand it) means that it undertook a search over all pairs `p, k` of numbers below `n` until it finds one where `p` is prime, and `p^k = n`, or else loops through all possibilities.

This PR creates a new theorem which instead searches over possible values of the exponent first, bounding the search at the binary logarithm of `n`, and then a further theorem which uses `n.minFac` for `p`. This massively reduces the time for large `n`.

In principle this could be made polynomial time, if we were to compute the putative prime factor for each `k` by taking the `k`th root and checking primality with AKS. But until that is implemented, this seems like a fine improvement.

Author: BoltonBailey

Mathlib/Algebra/IsPrimePow.lean

@@ -6,6 +6,8 @@ Authors: Bhavik Mehta
 import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Order.Nat
 import Mathlib.Data.Nat.Prime.Basic
+import Mathlib.Data.Nat.Log
+import Mathlib.Data.Nat.Prime.Pow
 
 /-!
 # Prime powers
@@ -76,8 +78,37 @@ theorem isPrimePow_nat_iff_bounded (n : ℕ) :
   conv => { lhs; rw [← (pow_one p)] }
   exact Nat.pow_le_pow_right hp.one_lt.le hk
 
+theorem isPrimePow_nat_iff_bounded_log (n : ℕ) :
+    IsPrimePow n
+      ↔ ∃ k : ℕ, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p : ℕ, p ≤ n ∧ n = p ^ k ∧ p.Prime := by
+  rw [isPrimePow_nat_iff]
+  constructor
+  · rintro ⟨p, k, hp', hk', rfl⟩
+    refine ⟨k, ?_, hk', ⟨p, Nat.le_pow hk', rfl, hp'⟩⟩
+    · calc
+        k = Nat.log 2 (2 ^ k) := by simp
+        _ ≤ Nat.log 2 (p ^ k) := Nat.log_mono Nat.one_lt_two Nat.AtLeastTwo.prop
+                                   (Nat.pow_le_pow_left (Nat.Prime.two_le hp') k)
+  · rintro ⟨k, hk, hk', ⟨p, hp, rfl, hp'⟩⟩
+    exact ⟨p, k, hp', hk', rfl⟩
+
+theorem isPrimePow_nat_iff_bounded_log_minFac (n : ℕ) :
+    IsPrimePow n
+      ↔ ∃ k : ℕ, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k := by
+  rw [isPrimePow_nat_iff_bounded_log]
+  obtain rfl | h := eq_or_ne n 1
+  · simp
+  constructor
+  · rintro ⟨k, hkle, hk_pos, p, hle, heq, hprime⟩
+    refine ⟨k, hkle, hk_pos, ?_⟩
+    rw [heq, hprime.pow_minFac hk_pos.ne']
+  · rintro ⟨k, hkle, hk_pos, heq⟩
+    refine ⟨k, hkle, hk_pos, n.minFac, Nat.minFac_le ?_, heq, ?_⟩
+    · grind [Nat.minFac_prime_iff, nonpos_iff_eq_zero, Nat.log_zero_right, lt_self_iff_false]
+    · grind [Nat.minFac_prime_iff]
+
 instance {n : ℕ} : Decidable (IsPrimePow n) :=
-  decidable_of_iff' _ (isPrimePow_nat_iff_bounded n)
+  decidable_of_iff' _ (isPrimePow_nat_iff_bounded_log_minFac n)
 
 theorem IsPrimePow.dvd {n m : ℕ} (hn : IsPrimePow n) (hm : m ∣ n) (hm₁ : m ≠ 1) : IsPrimePow m := by
   grind [isPrimePow_nat_iff, Nat.dvd_prime_pow, Nat.pow_eq_one]