WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Vector field

Revision #1654 → #2189 · back to history

modifiedVector field (informal)1423e645a34f
FieldFrom #1654To #2189
mathlib.decl—TangentSpace
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Manifold.IsManifold.Basic
note—Informal notion; Mathlib formalizes the manifold version via `TangentSpace I` with vector fields encoded as functions `(x : M) → TangentSpace I x`.
status—partial
addedTensor fielddd47fe186fe4
modifiedVector field on a subset of Euclidean space35975c4f6440
FieldFrom #1654To #2189
mathlib.decl—VectorField.lieBracket
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.Calculus.VectorField
note—Mathlib uses `E → E` directly (no wrapping definition) — the convention is implicit in the `VectorField` namespace operations on functions `E → E`.
status—partial
modifiedContinuous vector field0bd2395687fa
FieldFrom #1654To #2189
mathlib.decl—Continuous
mathlib.match_kind—invocation
mathlib.module—Mathlib.Topology.Defs.Basic
note—Treated as `Continuous V` (or `ContinuousOn`) for the underlying function; no dedicated vector-field continuity class.
status—partial
modifiedSmooth vector fieldafdb713e0f94
FieldFrom #1654To #2189
mathlib.decl—ContDiff
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.Calculus.ContDiff.Defs
note—Encoded by applying `ContDiff 𝕜 n` to `V : E → E`; there is no dedicated `SmoothVectorField` predicate.
status—partial
modifiedCounterclockwise rotation vector fieldb79e6501b80a
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The specific rotation example `(-y, x)` is not formalized as a named declaration.
status—not_formalized
modifiedModule structure on smooth vector fields0b7418d95bf0
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `C^∞(M)`-module structure on smooth vector fields is defined; pointwise `Pi.module` exists but not over the ring of smooth functions specifically.
status—not_formalized
modifiedContravariant transformation lawae9811e4c565
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No explicit coordinate-change contravariance law for vector fields formalized in Mathlib.
status—not_formalized
modifiedVector field on a manifold0c1316db0490
FieldFrom #1654To #2189
mathlib.decl—TangentSpace
mathlib.match_kind—invocation
mathlib.module—Mathlib.Geometry.Manifold.IsManifold.Basic
note—Encoded throughout Mathlib as `(x : M) → TangentSpace I x` (used by `VectorField.mlieBracket`, `mpullback`, etc.) but with no top-level `VectorField` definition.
status—partial
addedVector field as section of the tangent bundle79f55b14da8b
modifiedVector field as derivation (alternative)bcd9545f50fd
FieldFrom #1654To #2189
mathlib.decl—Derivation
mathlib.match_kind—generalization
mathlib.module—Mathlib.RingTheory.Derivation.Basic
note—`Derivation` is defined for algebras generally, but the identification with vector fields on a smooth manifold via `C^∞(M)` is not formalized.
status—partial
modifiedSmooth/analytic vector fields on manifold1dcf8ca220c0
FieldFrom #1654To #2189
mathlib.decl—ContMDiffSection
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
note—Smooth sections of the tangent bundle are captured by `ContMDiffSection I E (TangentSpace I)`.
status—formalized
modifiedWind vector field on Earth3a28f447d4a1
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Physical example not formalized in Mathlib.
status—not_formalized
modifiedVelocity field of a moving fluid569c9c9abe4d
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Physical example not formalized in Mathlib.
status—not_formalized
modifiedStreamlines, streaklines, pathlines2462409471bd
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Fluid-dynamic curve concepts not formalized in Mathlib.
status—not_formalized
modifiedMagnetic field375f671512bb
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Physical example not formalized in Mathlib.
status—not_formalized
modifiedElectric field from Maxwell's equationsa910b631461d
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Maxwell's equations and the electric field are not formalized in Mathlib.
status—not_formalized
modifiedGravitational field63b4330b1932
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Physical example not formalized in Mathlib.
status—not_formalized
modifiedGradient field / conservative fieldda367dbe8bdd
FieldFrom #1654To #2189
mathlib.decl—gradient
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.Calculus.Gradient.Basic
note—The `gradient` of a scalar function is defined, but no `IsConservativeField`/`IsGradientField` predicate on vector fields is given.
status—partial
modifiedGradient flow36a7ef123773
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Gradient flow as a named concept is not formalized in Mathlib.
status—not_formalized
modifiedPath integral around closed curve in conservative field is zero1c24d4dae0f2
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Line integrals of vector fields and the closed-loop vanishing for conservative fields are not formalized.
status—not_formalized
modifiedCentral field7cce63669cf1
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Central (radial) vector fields are not defined in Mathlib.
status—not_formalized
modifiedCenter of the fielda85729f4a7ee
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No definition of center of a central field in Mathlib.
status—not_formalized
modifiedCentral fields are gradient fields2b56c82c598c
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized, since neither central nor gradient-field predicates exist in Mathlib.
status—not_formalized
modifiedLine integral of a vector fieldf30c4b2a7cc5
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No dedicated line integral of a vector field is defined in Mathlib (only complex/contour primitives in `Mathlib.Analysis.Complex.HasPrimitives`).
status—not_formalized
modifiedDivergenceae4eb907673d
FieldFrom #1654To #2189
mathlib.decl—BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.BoxIntegral.DivergenceTheorem
note—Divergence is only used inline as the sum `∑ i, f' x (Pi.single i 1) i` in divergence-theorem statements; no standalone `divergence` definition exists.
status—partial
modifiedDivergence theorem (reference)abbc867f7d02
FieldFrom #1654To #2189
mathlib.decl—MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Integral.DivergenceTheorem
note—The divergence theorem is formalized over rectangular boxes via `integral_divergence_of_hasFDerivAt_off_countable`.
status—formalized
modifiedCurlbd970c1e27ee
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Curl in 3D is not defined in Mathlib.
status—not_formalized
modifiedStokes' theorem (reference)68a64845b5b3
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The classical Stokes' theorem (curl form) is not formalized; only the divergence theorem version is available.
status—not_formalized
modifiedIndex of a vector field at a zero875092ae03ff
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Index of an isolated zero of a vector field is not formalized in Mathlib.
status—not_formalized
modifiedIndex as degree of map to unit sphere0950d49fbab0
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Neither the degree of a map to a sphere nor the index definition is formalized in Mathlib.
status—not_formalized
modifiedIndex of vector field as a whole90d82803371e
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Total index over finitely many zeros is not formalized.
status—not_formalized
modifiedHairy ball theorembe4f0b1f06f1
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Hairy ball theorem is not formalized in Mathlib.
status—not_formalized
modifiedPoincaré–Hopf theorem5451e9ff8733
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Poincaré–Hopf is not formalized; Euler characteristic of a manifold is also not available.
status—not_formalized
modifiedIntegral curves / trajectories33a41395c566
FieldFrom #1654To #2189
mathlib.decl—IsMIntegralCurve
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.IntegralCurve.Basic
note—Integral curves of vector fields on manifolds are defined as `IsMIntegralCurve` (and `IsIntegralCurve` in the Euclidean ODE setting).
status—formalized
modifiedPicard–Lindelöf theorem (uniqueness of integral curves)1b32337067f9
FieldFrom #1654To #2189
mathlib.decl—IsPicardLindelof.exists_eq_forall_mem_Icc_eq_picard
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.ODE.PicardLindelof
note—Picard–Lindelöf existence is formalized as `IsPicardLindelof.exists_eq_forall_mem_Icc_eq_picard`, with the manifold companion `exists_isMIntegralCurveAt_of_contMDiffAt`.
status—formalized
modifiedComplete vector field2a20c20ffad4
FieldFrom #1654To #2189
anchor.snippeta vector field onis called complete if each of its flow curves exists for all time
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `IsCompleteVectorField` predicate or equivalent is defined in Mathlib.
provenanceai-agent1ai-moderated
status—not_formalized
modifiedCompactly supported vector fields are completec6c032260eb6
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized, since completeness of vector fields is not defined.
status—not_formalized
modifiedSmooth vector fields on compact manifolds are complete6d420adad1e8
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
addedOne-parameter group of diffeomorphisms from a complete vector fieldd5ec445b8eb2
modifiedIncomplete vector field on the real line3f8b655ef6d3
FieldFrom #1654To #2189
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The standard `x^2` non-complete example is not formalized.
status—not_formalized
modifiedLie bracket of vector fieldsbd11c4deca1c
FieldFrom #1654To #2189
mathlib.decl—VectorField.mlieBracket
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.VectorField.LieBracket
note—The Lie bracket is `VectorField.mlieBracket` on manifolds (and `VectorField.lieBracket` on normed spaces).
status—formalized
modifiedf-relatedness of vector fields5b6afad45234
FieldFrom #1654To #2189
mathlib.decl—VectorField.mpullback
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Manifold.VectorField.Pullback
note—No predicate `IsFRelated` is defined; pullbacks (`VectorField.mpullback`) give the closest infrastructure, with f-relatedness expressible as `mpullback f W = V`.
status—partial
modifiedLie bracket preserves f-relatedness156f216c1cc6
FieldFrom #1654To #2189
mathlib.decl—VectorField.mpullback_mlieBracket
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.VectorField.LieBracket
note—Naturality of the Lie bracket under pullback is `VectorField.mpullback_mlieBracket`, equivalent to preservation of f-relatedness.
status—formalized
addedp-vector fielda82321988bd4
addedDifferential k-formf9063b512bcd
modifiedVector field on a commutative algebraf7566e47c9ab
FieldFrom #1654To #2189
mathlib.decl—Derivation
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.Derivation.Basic
note—Algebraic vector fields as derivations on a commutative algebra are formalized as `Derivation R A M`.
status—formalized