OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoreMassCompact.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compactness of the genuine global core bump multipliers. The weighted quotient norm is controlled by the proved compact local map.

  1. lemma OAI.CubicFirstMoment.cubicThetaLocalValue_norm_sq line 17
  2. lemma OAI.CubicFirstMoment.cubicThetaCoreMass_weighted_integral line 38
  3. lemma OAI.CubicFirstMoment.cubicThetaCoreMass_norm_domination line 54
  4. theorem OAI.CubicFirstMoment.cubicThetaCoreMass_compact line 78