OAI/NumberTheory/JointDickman/Analysis/CharacterLFunctionCutoff.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A bounded remainder after truncating a nonprincipal Dirichlet L-series

  1. lemma OAI.JointDickman.sum_nat_Icc_int_cast line 10
  2. lemma OAI.JointDickman.character_LFunction_cutoff_bound line 26
  3. lemma OAI.JointDickman.character_LFunction_head_bound line 79