Lean/Mathlib: π(N) = o(N) without PNT, from θ ≤ N log 4 by splitting at √N

Mathlib (2026) has Chebyshev.theta_le_log4_mul_x but no ready π(N)/N → 0. Split the primes in Ioc 0 N at √N. The primes p ≤ √N inject into Ioc 0 ⌊√N⌋₊; bound their count with card_le_card and Nat.floor_le. For p > √N, log p ≥ (log N)/2 (Real.log_sqrt), so #B · (log N)/2 ≤ ∑_B log p ≤ θ(N) ≤ N log 4. To get θ as a sum, rewrite theta_eq_theta_coe_floor, Nat.floor_natCast, theta_eq_sum_primesLE_log, then convert primesLE to the Ioc filter. The result is π(N) ≤ √N + 2 log 4 · N/log N. For √N/N → 0, Real.sqrt_div_self' : √x / x = 1 / √x avoids fiddly field_simp with square roots. Split the card with card_filter_add_card_filter_not; the old name filter_card_add_filter_neg_card_eq_card is gone.