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.
Weinstein Lagrangian neighborhood theorem
Statement
Assume . If is a closed Lagrangian embedding, then there are neighbourhoods of in and of the zero section in and a symplectomorphism satisfying for every .
Facts & Assumptions
Given: and the closed Lagrangian embedding in the statement.
Under the assumed choice principle, admits a compatible almost-complex structure. Every symplectic manifold admits a compatible almost-complex structure.
The cotangent zero section with is the canonical model. Canonical symplectic model near the zero section of .
Closed embeddings have tubular neighbourhoods, and relative Moser corrects two forms agreeing as tensors along the submanifold. The tubular neighbourhood theorem in a smooth ambient manifold, Relative Moser theorem.
Proof
Choose a compatible by [F1]. Then is a Lagrangian complement to : it is Lagrangian because preserves , and if then forces . The map , with , is an isomorphism.
At the zero section, and . Hence step 1.1 gives a symplectic bundle isomorphism equal to the identity on . Use tubular neighbourhoods from [F3] to realize it as the differential of a diffeomorphism between neighbourhoods, fixed on .
The forms and agree as tensors along the zero section. Their convex interpolation is symplectic after shrinking, so relative Moser in [F3] gives a correction fixed on the zero section. Composing it with yields and proves the claim, including noncompact closed through variable-radius neighbourhoods.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
32 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
- Eckhard Meinrenken, Symplectic Geometry (standard reference, not scraped)
- Ana Cannas da Silva, Lectures on Symplectic Geometry (standard reference, not scraped)