OAI/NumberTheory/CubicMoment/Decomposition/StoppedBilinearOverlap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Shared-prime incidence for the literal support. Inactive stopped coefficients contribute zero, so only active rows require roughness.

  1. lemma OAI.CubicFirstMoment.active_noncoprime_bipartite_energy line 14
  2. lemma OAI.CubicFirstMoment.active_modelOverlap_norm_sq_le line 51