OuterSieveNumerical.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Numerical minimization of the two cubic-sieve orientations for an outer frequency block. Variables p and q are the cube roots of its squarefree side lengths.

lemma OAI.CubicFirstMoment.outer_sieve_polynomial_min line 10