OAI/NumberTheory/CubicMoment/Estimates/PrimeMixedInterval.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Intersections of the half-open norm restrictions arising from the crossing test differ from the prime interval convention only at their two final endpoints.

  1. lemma OAI.CubicFirstMoment.mixed_norm_interval_away line 11