OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialMeanIntegral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Change of height in the literal v^-3 radial mean integral.

  1. lemma OAI.CubicFirstMoment.cubicThetaSectionMean_weight_integrable line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaRadialIntegral_zero_extension line 36
  3. lemma OAI.CubicFirstMoment.cubicThetaRadialIntegral_dilate line 48
  4. lemma OAI.CubicFirstMoment.cubicThetaRadialIntegral_integrable_zero_extension line 69
  5. lemma OAI.CubicFirstMoment.cubicThetaRadialIntegral_dilate_integrable line 89