The Riemann zeta function
is a function of one complex variable . It is a meromorphic function with a pole at . The following table lists all conditions such that RiemannZeta(s) is defined in Fungrim.
|
Table data:
such that
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
RiemannZeta | Riemann zeta function | |
OpenInterval | Open interval | |
Infinity | Positive infinity | |
RR | Real numbers | |
CC | Complex numbers | |
UnsignedInfinity | Unsigned infinity | |
FormalPowerSeries | Formal power series | |
FormalLaurentSeries | Formal Laurent series |
Source code for this entry:
Entry(ID("e0a6a2"), SymbolDefinition(RiemannZeta, RiemannZeta(s), "Riemann zeta function"), Description("The Riemann zeta function", RiemannZeta(s), "is a function of one complex variable", s, ". It is a meromorphic function with a pole at", Equal(s, 1), ".", "The following table lists all conditions such that", SourceForm(RiemannZeta(s)), "is defined in Fungrim."), Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(TableSection("Numbers"), Tuple(Element(s, OpenInterval(1, Infinity)), Element(RiemannZeta(s), OpenInterval(1, Infinity))), Tuple(Element(s, SetMinus(RR, Set(1))), Element(RiemannZeta(s), RR)), Tuple(Element(s, SetMinus(CC, Set(1))), Element(RiemannZeta(s), CC)), TableSection("Infinities"), Tuple(Element(s, Set(1)), Element(RiemannZeta(s), Set(UnsignedInfinity))), Tuple(Element(s, Set(Infinity)), Element(RiemannZeta(s), Set(1))), TableSection("Formal power series"), Tuple(And(Element(s, FormalPowerSeries(RR, x)), Unequal(SeriesCoefficient(s, x, 0), 1)), Element(RiemannZeta(s), FormalPowerSeries(RR, x))), Tuple(And(Element(s, FormalPowerSeries(CC, x)), Unequal(SeriesCoefficient(s, x, 0), 1)), Element(RiemannZeta(s), FormalPowerSeries(CC, x))), Tuple(And(Element(s, FormalPowerSeries(RR, x)), Unequal(s, 1)), Element(RiemannZeta(s), FormalLaurentSeries(RR, x))), Tuple(And(Element(s, FormalPowerSeries(CC, x)), Unequal(s, 1)), Element(RiemannZeta(s), FormalLaurentSeries(CC, x))))))