How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Formal Laurent series , their order, derivative, and residue
Definition
For a field , a formal Laurent series is a coefficient function whose support is bounded below. Write
Addition is coefficientwise and multiplication is finite convolution in each degree. If the supports of two factors are bounded below by and , then their product is bounded below by , and a fixed coefficient has only finitely many contributing pairs. For nonzero , define
and set . Define for every integer , extending coefficientwise, and define the formal residue
This generalizes the real-coefficient construction of The formal Laurent series : support bounded below, valuation, leading coefficient and uses the same finite-convolution and least-support conventions proved in is a commutative ring: the product is a finite sum and both operations preserve support bounded below and Valuation and leading coefficient in : , and the behaviour of under sums. It changes the indeterminate notation from that page's to .
Depends on
- Field
- The formal Laurent series $\mathbb{R}((t^{-1}))$: support bounded below, valuation, leading coefficient
- $\mathbb{R}((t^{-1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below
- Valuation and leading coefficient in $\mathbb{R}((t^{-1}))$: $v(fg) = v(f) + v(g)$, and the behaviour of $v$ under sums
Used by
- Formal distributions and fields on a vector space Definition
- Residue of a rational differential at a separable closed point Definition
- The formal hyperbolic tangent series and the even series x/tanh x Definition
- Vertex algebra in the state–field convention Definition
- Residues on the projective line and the vanishing of their sum Example
- Formal residues satisfy integration by parts, logarithmic differentiation, and change of variables Lemma
- Residues of exact differentials vanish Lemma
- The coefficient identity [z²ᵏ](z/tanh z)²ᵏ⁺¹=1 for every k Lemma
- The residue is independent of the uniformizer Lemma
- K⟦ x⟧ embeds in K((x)) as the nonnegative-order subring; every nonzero Laurent series is uniquely x^vₓ(h)u with u∈ K⟦ x⟧^× and inverse x^-vₓ(h)u⁻¹ Theorem
Dependency tree · two levels
13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Benjamin Sambale, An Invitation to Formal Power Series (standard reference, not scraped)