OAI/NumberTheory/CubicMoment/Estimates/InverseSquareTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrability from the precise inverse-square tail used by far cells.

  1. theorem OAI.CubicFirstMoment.integrable_of_inverse_square_tail line 10
  2. lemma OAI.CubicFirstMoment.norm_real_zpow_tail line 36