LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

A closed smooth two-form on a star-shaped domain has the radial primitive $α_{x} (v) = \int_{0}^{1} t τ_{t x} (x, v) d t$

Statement

Let $n \geq 1$ , let $U \subseteq R^{n}$ be an open set star-shaped with respect to $0$ (Star-shaped open subsets of Euclidean space), and let $τ$ be a smooth closed two-form on $U$ (A smooth differential $k$ -form, Closed and exact differential forms). Write $τ = \sum_{i < j} τ_{i j} d x^{i} \land d x^{j}$ with smooth coefficient functions $τ_{i j}$ , and extend the coefficients by $τ_{j i} : = - τ_{i j}$ and $τ_{i i} : = 0$ . Define $α : U \to (R^{n})^{*}$ by

$α_{x} (v) : = \int_{0}^{1} t τ_{t x} (x, v) d t .$

Then $α$ is a smooth one-form on $U$ , in coordinates

$α = \sum_{i = 1}^{n} α_{i} d x^{i}, α_{i} (x) = \int_{0}^{1} t \sum_{j = 1}^{n} x^{j} τ_{j i} (t x) d t,$

and $d α = τ$ on $U$ . In particular every smooth closed two-form on a star-shaped open subset of $R^{n}$ is exact, with the displayed explicit primitive.

Facts & Assumptions

Given: The open star-shaped set $U$ , the smooth closed two-form $τ$ , and the coefficients $τ_{i j}$ with $τ_{j i} = - τ_{i j}$ , $τ_{i i} = 0$ (A smooth differential $k$ -form, $C^{k}$ Euclidean maps and diffeomorphisms).

[F1]

Poincare lemma for differential forms (Poincare lemma for differential forms on star shaped domains): every closed smooth $k$ -form on a star-shaped open domain is exact for $k \geq 1$ , and for centre $0$ one primitive is $η_{x} (v_{1}, \dots, v_{k - 1}) = \int_{0}^{1} t^{k - 1} ω_{t x} (x, v_{1}, \dots, v_{k - 1}) d t$ .

[F2]

Differentiation under the integral sign on a rectangle (Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral): if $g$ is continuous on $[a, b] \times [c, d]$ , if $x \mapsto g (x, t)$ is differentiable with continuous derivative $h$ , then $G (x) = \int_{c}^{d} g (x, t) d t$ is differentiable with $G^{'} (x) = \int_{c}^{d} h (x, t) d t$ .

[F3]

The fundamental theorem of calculus in the form $\int_{a}^{b} G^{'} = G (b) - G (a)$ for $G$ continuous on $[a, b]$ , differentiable on $(a, b)$ , with Riemann integrable derivative (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

[F4]

Chain rule, partial derivatives and coordinate formula for the exterior derivative (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ , The local coordinate formula for the exterior derivative): for a smooth curve $t \mapsto t x$ one has $\frac{d}{d t} τ_{k i} (t x) = \sum_{j} x^{j} \partial_{j} τ_{k i} (t x)$ , and for $α = \sum_{i} α_{i} d x^{i}$ the coefficients of $d α$ are $(d α)_{k i} = \partial_{k} α_{i} - \partial_{i} α_{k}$ .

Proof

technique · direct; first specialise the published $k$-form Poincare lemma to $k=2$, then verify the displayed coefficient formula by differentiating under the integral sign and using the fundamental theorem of calculus

1.1F1given

Specialise [F1] to $k = 2$ and $ω = τ$ : since $τ$ is a smooth closed two-form on the star-shaped domain $U$ with centre $0$ , it is exact and the one-form $η_{x} (v) = \int_{0}^{1} t τ_{t x} (x, v) d t$ is a smooth primitive with $d η = τ$ ; this $η$ is the displayed $α$ , so the claim holds.

1.2F2F3F4algebra

Independent coefficient verification of the display: fix an arbitrary $x_{0} \in U$ . The radial segment ${t x_{0} : 0 \leq t \leq 1}$ is compact and contained in $U$ . For each $t$ choose a product neighbourhood of $(t, x_{0})$ mapped into $U$ by $(s, x) \mapsto s x$ ; finitely many such neighbourhoods cover $[0, 1] \times {x_{0}}$ , and intersection of their $x$ -neighbourhoods contains a ball $B (x_{0}, r)$ whose closed ball still lies in that intersection. Hence $t x \in U$ for every $x \in \overline{B} (x_{0}, r)$ and $t \in [0, 1]$ . On the compact parameter set $\overline{B} (x_{0}, r) \times [0, 1]$ the integrand $(x, t) \mapsto t τ_{t x} (x, \cdot)$ and its $x$ -derivatives are continuous, so [F2], applied to the one-variable functions $s \mapsto x + s e_{k}$ along the coordinate directions $e_{k}$ , permits differentiation under the integral sign in every partial derivative, and $\partial_{k} α_{i} (x) - \partial_{i} α_{k} (x) = \int_{0}^{1} [2 t τ_{k i} (t x) + t^{2} \sum_{j} x^{j} (\partial_{k} τ_{j i} - \partial_{i} τ_{j k}) (t x)] d t$ . Closedness of $τ$ reads $\partial_{k} τ_{j i} + \partial_{j} τ_{i k} + \partial_{i} τ_{k j} = 0$ , which with $τ_{k j} = - τ_{j k}$ gives $\partial_{k} τ_{j i} - \partial_{i} τ_{j k} = \partial_{j} τ_{k i}$ ; hence the bracket equals $2 t τ_{k i} (t x) + t^{2} \frac{d}{d t} τ_{k i} (t x) = \frac{d}{d t} [t^{2} τ_{k i} (t x)]$ by [F4], and [F3] gives $\partial_{k} α_{i} (x) - \partial_{i} α_{k} (x) = τ_{k i} (x)$ ; by [F4] this says $d α = τ$ near the arbitrary point $x_{0}$ , hence on all of $U$ .

2.1step 1.1step 1.2∎

By step 1.1 the displayed $α$ is a smooth one-form with $d α = τ$ , and step 1.2 confirms the same identity coefficientwise for that explicit formula; both conclusions agree, so $α$ is a smooth primitive of $τ$ on $U$ .

Remarks

The coefficient computation of step 1.2 is the explicit form in which the local action-angle consumer uses this lemma: the two-form there is the pullback $σ^{*} ω$ of the symplectic form along a section, and the primitive produced is a one-form on a star-shaped ball of the action coordinates.
The published Liouville–Arnold action–angle theorem cites, at its step 5.2, the one-form Poincare lemma Poincare's lemma on a star-shaped domain: every closed C1 field is exact for a closed two-form. That direct supplier use is inadequate for the two-form; this lemma records the two-form case at $k = 2$ of [F1] with its explicit primitive, and the local theorem Action-angle coordinates on a saturated proper submersion neighbourhood of a compact connected regular fibre, with the two-form primitive supplied locally uses it instead. No published or imported item is edited by this page.

A closed smooth two-form on a star-shaped domain has the radial primitive $α_{x} (v) = \int_{0}^{1} t τ_{t x} (x, v) d t$

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

A closed smooth two-form on a star-shaped domain has the radial primitive αx(v)=∫01t τtx(x,v) dtαx​(v)=∫01​tτtx​(x,v)dt

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

A closed smooth two-form on a star-shaped domain has the radial primitive $α_{x} (v) = \int_{0}^{1} t τ_{t x} (x, v) d t$