Combining local divisibility at distinct primes

Local powers of different primes multiply, and their weighted logarithms give a lower bound on the logarithm of a positive determinant gcd. Estimating these prime sums uniformly for curve reductions is a separate part of CCDN Proposition 3.2.6.

theorem CCDN.sum_log_prime_powers_le_log (P : Finset ℕ) (e : ℕ → ℕ) {D : ℤ} (hD : 0 < D) (hP : ∀ p ∈ P, Nat.Prime p) (hdiv : ∀ p ∈ P, ↑p ^ e p ∣ D) : ∑ p ∈ P, ↑(e p) * Real.log ↑p ≤ Real.log ↑D

If each prime p in the finite set P has p ^ e p dividing the positive integer D, then ∑ p ∈ P, e p * log p ≤ log D.