OAI/NumberTheory/CubicMoment/Decomposition/DistinguishedComplementMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The complementary tuple mass for the literal smooth distinguished weights. Their rough support is proved from the detector difference.

  1. lemma OAI.CubicFirstMoment.distinguishedRadialWeight_eq_primeWeight line 14
  2. lemma OAI.CubicFirstMoment.distinguishedRadialWeight_prime_rough line 19
  3. theorem OAI.CubicFirstMoment.distinguished_complement_tuple_mass line 27