Skip to content

Commit

Permalink
feat(NumberTheory/LSeries): introduce notations (#11253)
Browse files Browse the repository at this point in the history
This just introduces `L` as a short notation for `LSeries` and `↗f` as notation for `fun n : ℕ ↦ (f n : ℂ)`,
both scoped to `LSeries.notation`. The latter makes it convenient to use arithmetic functions
or Dirichlet characters (or anything that coerces to a function `N → R`, where `ℕ` coerces
to `N` and `R` coerces to `ℂ`) as arguments to `LSeries` etc. The first is for convenience (and agreement with informal math, where we write "L(f, s)"), and the second one considerably simplifies statements involving Dirichlet characters or arithmetic functions like the von Mangoldt function and their L-series.

See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837) on Zulip.
  • Loading branch information
MichaelStollBayreuth committed Mar 11, 2024
1 parent bbdc3c0 commit f8a97cf
Showing 1 changed file with 22 additions and 1 deletion.
23 changes: 22 additions & 1 deletion Mathlib/NumberTheory/LSeries/Basic.lean
Expand Up @@ -36,6 +36,13 @@ Given a sequence `f: ℕ → ℂ`, we define the corresponding L-series.
* `LSeriesSummable.isBigO_rpow`: if the `LSeries` of `f` is summable at `s`,
then `f = O(n^(re s))`.
## Notation
We introduce `L` as notation for `LSeries` and `↗f` as notation for `fun n : ℕ ↦ (f n : ℂ)`,
both scoped to `LSeries.notation`. The latter makes it convenient to use arithmetic functions
or Dirichlet characters (or anything that coerces to a function `N → R`, where `ℕ` coerces
to `N` and `R` coerces to `ℂ`) as arguments to `LSeries` etc.
## Tags
L-series
Expand All @@ -48,7 +55,6 @@ L-series
* Move `LSeries_add` and friends to a new file on algebraic operations on L-series
-/


open scoped BigOperators

open Complex
Expand Down Expand Up @@ -186,6 +192,21 @@ theorem LSeriesSummable_iff_of_re_eq_re {f : ℕ → ℂ} {s s' : ℂ} (h : s.re
#align nat.arithmetic_function.l_series_summable_iff_of_re_eq_re LSeriesSummable_iff_of_re_eq_re


/-!
### Notation
-/

@[inherit_doc]
scoped[LSeries.notation] notation "L" => LSeries

/-- We introduce notation `↗f` for `f` interpreted as a function `ℕ → ℂ`.
Let `R` be a ring with a coercion to `ℂ`. Then we can write `↗χ` when `χ : DirichletCharacter R`
or `↗f` when `f : ArithmeticFunction R` or simply `f : N → R` with a coercion from `ℕ` to `N`
as an argument to `LSeries`, `LSeriesHasSum`, `LSeriesSummable` etc. -/
scoped[LSeries.notation] notation:max "↗" f:max => fun n : ℕ ↦ (f n : ℂ)


/-!
### Criteria for and consequences of summability of L-series
Expand Down

0 comments on commit f8a97cf

Please sign in to comment.