OAI/NumberTheory/JointDickman/Analysis/SquarefreePerronIntegrable.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Absolute integrability of the actual normalized Perron line

  1. theorem OAI.JointDickman.squarefreeLSeries_measurable line 12
  2. theorem OAI.JointDickman.squarefreeLSeries_vertical_bound line 19
  3. theorem OAI.JointDickman.squarefreeNormalizedPerron_integrable line 38