OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterContinuation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The nonprincipal character Abel integral agrees with the existing L-function throughout re(s)>0, with explicit modulus dependence.

  1. def OAI.TwoPointCorrelations.mrtCharacterAbelInput line 18
  2. lemma OAI.TwoPointCorrelations.mrtCharacterAbelInput_measurable line 22
  3. lemma OAI.TwoPointCorrelations.mrtCharacterAbelInput_norm line 26
  4. lemma OAI.TwoPointCorrelations.mrtCharacterAbelInput_locallyIntegrable line 34
  5. lemma OAI.TwoPointCorrelations.mrtCharacterAbelInput_bigO_atTop line 40
  6. lemma OAI.TwoPointCorrelations.mrtCharacterAbelInput_bigO_zero line 46
  7. lemma OAI.TwoPointCorrelations.mrtCharacterAbelIntegral_eq_mellin line 55
  8. theorem OAI.TwoPointCorrelations.mrtCharacterAbelIntegral_differentiableAt line 72
  9. theorem OAI.TwoPointCorrelations.mrtCharacterAbelIntegral_eq_LFunction_of_pos line 89

    Source documentation

    The bounded-partial-sum integral is the existing L-function on the entire half-plane of convergence of that integral.

    theorem mrtCharacterAbelIntegral_eq_LFunction_of_pos (χ : DirichletCharacter ℂ q)
    (hχ : χ ≠ 1) {s : ℂ} (hs : 0 < s.re) :
    mrtCharacterAbelIntegral χ s = DirichletCharacter.LFunction χ s := by
…

    Mentions: OAI.TwoPointCorrelations.mrtCharacterAbelIntegral

  10. theorem OAI.TwoPointCorrelations.mrt_character_LFunction_norm_le line 108
  11. theorem OAI.TwoPointCorrelations.mrt_character_LFunction_norm_halfPlane line 114