Documentation

Mathlib.NumberTheory.LSeries.Injectivity

A converging L-series determines its coefficients #

We show that two functions f and g : โ„• โ†’ โ„‚ whose L-series agree and both converge somewhere must agree on all nonzero arguments. See LSeries_eq_iff_of_abscissaOfAbsConv_lt_top and LSeries_injOn.

source
๐Ÿ“ coverage
theorem LSeries.abscissaOfAbsConv_add_le (f g : โ„• โ†’ โ„‚) :
abscissaOfAbsConv (f + g) โ‰ค max (abscissaOfAbsConv f) (abscissaOfAbsConv g)

The abscissa of absolute convergence of f + g is at most the maximum of those of f and g.

source
๐Ÿ“ coverage
theorem LSeries.abscissaOfAbsConv_sub_le (f g : โ„• โ†’ โ„‚) :
abscissaOfAbsConv (f - g) โ‰ค max (abscissaOfAbsConv f) (abscissaOfAbsConv g)

The abscissa of absolute convergence of f - g is at most the maximum of those of f and g.

source
๐Ÿ“ coverage
theorem LSeries.tendsto_cpow_mul_atTop {f : โ„• โ†’ โ„‚} {n : โ„•} (h : โˆ€ m โ‰ค n, f m = 0) (ha : abscissaOfAbsConv f < โŠค) :
Filter.Tendsto (fun (x : โ„) => (โ†‘n + 1) ^ โ†‘x * LSeries f โ†‘x) Filter.atTop (nhds (f (n + 1)))

If the coefficients f m of an L-series are zero for m โ‰ค n and the L-series converges at some point, then f (n+1) is the limit of (n+1)^x * LSeries f x as x โ†’ โˆž.

source
๐Ÿ“ coverage
theorem LSeries.tendsto_atTop {f : โ„• โ†’ โ„‚} (ha : abscissaOfAbsConv f < โŠค) :
Filter.Tendsto (fun (x : โ„) => LSeries f โ†‘x) Filter.atTop (nhds (f 1))

If the L-series of f converges at some point, then f 1 is the limit of LSeries f x as x โ†’ โˆž.

source
๐Ÿ“ coverage
theorem LSeries_eq_zero_of_abscissaOfAbsConv_eq_top {f : โ„• โ†’ โ„‚} (h : LSeries.abscissaOfAbsConv f = โŠค) :
LSeries f = 0
source
๐Ÿ“ coverage
theorem LSeries_eventually_eq_zero_iff' {f : โ„• โ†’ โ„‚} :
(fun (x : โ„) => LSeries f โ†‘x) =แถ [Filter.atTop] 0 โ†” (โˆ€ (n : โ„•), n โ‰  0 โ†’ f n = 0) โˆจ LSeries.abscissaOfAbsConv f = โŠค

The LSeries of f is zero for large real arguments if and only if either f n = 0 for all n โ‰  0 or the L-series converges nowhere.

source
๐Ÿ“ coverage
theorem LSeries_eq_zero_iff {f : โ„• โ†’ โ„‚} (hf : f 0 = 0) :
LSeries f = 0 โ†” f = 0 โˆจ LSeries.abscissaOfAbsConv f = โŠค

Assuming f 0 = 0, the LSeries of f is zero if and only if either f = 0 or the L-series converges nowhere.

source
๐Ÿ“ coverage
theorem LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq {f g : โ„• โ†’ โ„‚} (hf : LSeries.abscissaOfAbsConv f < โŠค) (hg : LSeries.abscissaOfAbsConv g < โŠค) (h : (fun (x : โ„) => LSeries f โ†‘x) =แถ [Filter.atTop] fun (x : โ„) => LSeries g โ†‘x) :
(fun (x : โ„) => LSeries (f - g) โ†‘x) =แถ [Filter.atTop] 0

If the LSeries of f and of g converge somewhere and agree on large real arguments, then the L-series of f - g is zero for large real arguments.

source
theorem LSeries.eq_of_LSeries_eventually_eq {f g : โ„• โ†’ โ„‚} (hf : abscissaOfAbsConv f < โŠค) (hg : abscissaOfAbsConv g < โŠค) (h : (fun (x : โ„) => LSeries f โ†‘x) =แถ [Filter.atTop] fun (x : โ„) => LSeries g โ†‘x) {n : โ„•} (hn : n โ‰  0) :
f n = g n

If the LSeries of f and of g converge somewhere and agree on large real arguments, then f n = g n whenever n โ‰  0.

source
๐Ÿ“ coverage
theorem LSeries_eq_iff_of_abscissaOfAbsConv_lt_top {f g : โ„• โ†’ โ„‚} (hf : LSeries.abscissaOfAbsConv f < โŠค) (hg : LSeries.abscissaOfAbsConv g < โŠค) :
LSeries f = LSeries g โ†” โˆ€ (n : โ„•), n โ‰  0 โ†’ f n = g n

If the LSeries of f and of g both converge somewhere, then they are equal if and only if f n = g n whenever n โ‰  0.

source
๐Ÿ“ coverage
theorem LSeries_injOn :
Set.InjOn LSeries {f : โ„• โ†’ โ„‚ | f 0 = 0 โˆง LSeries.abscissaOfAbsConv f < โŠค}

The map f โ†ฆ LSeries f is injective on functions f such that f 0 = 0 and the L-series of f converges somewhere.