Fungrim home page

Fungrim entry: b63dce

Symbol: Sin sin(z)\sin(z) Sine
The sine function sin(z)\sin(z) (denoted by Sin(z) in the Fungrim formula language) is a function of a single variable. It can be defined for real and complex arguments by the series f340cb or by the differential equation 21f156 with appropriate initial values. The following table lists conditions such that Sin(z) is defined in Fungrim.
Domain Codomain
Numbers
zRz \in \mathbb{R} sin(z)[1,1]\sin(z) \in \left[-1, 1\right]
zCz \in \mathbb{C} sin(z)C\sin(z) \in \mathbb{C}
Formal power series
zR[[x]]z \in \mathbb{R}[[x]] sin(z)R[[x]]\sin(z) \in \mathbb{R}[[x]]
zC[[x]]z \in \mathbb{C}[[x]] sin(z)C[[x]]\sin(z) \in \mathbb{C}[[x]]
Table data: (P,Q)\left(P, Q\right) such that (P)        (Q)\left(P\right) \;\implies\; \left(Q\right)
Definitions:
Fungrim symbol Notation Short description
Sinsin(z)\sin(z) Sine
RRR\mathbb{R} Real numbers
ClosedInterval[a,b]\left[a, b\right] Closed interval
CCC\mathbb{C} Complex numbers
PowerSeriesK[[x]]K[[x]] Formal power series
Source code for this entry:
Entry(ID("b63dce"),
    SymbolDefinition(Sin, Sin(z), "Sine"),
    Description("The sine function", Sin(z), "(denoted by", SourceForm(Sin(z)), "in the Fungrim formula language)", "is a function of a single variable.", "It can be defined for real and complex arguments by the series", EntryReference("f340cb"), "or by the differential equation", EntryReference("21f156"), "with appropriate initial values.", "The following table lists conditions such that", SourceForm(Sin(z)), "is defined in Fungrim."),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(TableSection("Numbers"), Tuple(Element(z, RR), Element(Sin(z), ClosedInterval(-1, 1))), Tuple(Element(z, CC), Element(Sin(z), CC)), TableSection("Formal power series"), Tuple(Element(z, PowerSeries(RR, x)), Element(Sin(z), PowerSeries(RR, x))), Tuple(Element(z, PowerSeries(CC, x)), Element(Sin(z), PowerSeries(CC, x))))))

Topics using this entry

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2021-03-15 19:12:00.328586 UTC