HalaszMixedGrouped.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The Perron estimate for one mixed logarithmic prime block. Both prime factors avoid the small deleted bands; the smooth coefficient retains the literal typical mask.

theorem OAI.TwoPointCorrelations.halasz_mixed_grouped_estimate line 15