Revision #1139 → #1978 · back to history
modifiedStokes' theorem (curl form)bcef3e8d0890
| Field | From #1139 | To #1978 |
|---|
| mathlib.decl | MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable | — |
| mathlib.module | Mathlib.MeasureTheory.Integral.DivergenceTheorem | — |
| note | Mathlib has the divergence theorem for Henstock–Kurzweil/Bochner integrals and a Poincaré lemma for 1-forms, but no Stokes theorem stated in curl form. | Mathlib has the divergence theorem on Euclidean boxes but no Stokes/Kelvin–Stokes theorem stated in curl form. |
| provenance | ai | ai-moderated |
| status | partial | not_formalized |
modifiedCurl operator93c665fe31e9
| Field | From #1139 | To #1978 |
|---|
| note | No declaration named `curl` (or analog) on vector fields exists in Mathlib. | No declaration named `curl` (or analog) on vector fields exists in Mathlib; a grep over `Mathlib/` returns no curl operator. |
modifiedKelvin–Stokes theorem7baa4e6bbeff
| Field | From #1139 | To #1978 |
|---|
| note | Mathlib does not contain a Kelvin–Stokes theorem; only the divergence theorem and a Poincaré lemma for 1-forms exist. | Mathlib does not contain a Kelvin–Stokes theorem; only the divergence theorem on Euclidean boxes exists. |
modifiedCurl via surface integral over a shellca29f7844d7e
| Field | From #1139 | To #1978 |
|---|
| note | No surface-integral-over-a-shell definition of curl is present. | No surface-integral-over-a-shell definition of curl is present in Mathlib. |
modifiedCurl via exterior derivative9552d0e1e02f
| Field | From #1139 | To #1978 |
|---|
| mathlib.match_kind | — | generalization |
| provenance | ai | ai-moderated |
modifiedCurl of rotating disk velocity field7367abdfef2c
| Field | From #1139 | To #1978 |
|---|
| note | No formalization of the rotating-disk velocity field example. | No formalization of the rotating-disk velocity field example; in particular, the identity vorticity = curl(velocity) = 2·(angular velocity) is not formalized. |
| provenance | ai | ai-moderated |
modifiedDifferential k-forms in 3 dimensionsbbb1f108aac5
| Field | From #1139 | To #1978 |
|---|
| mathlib.module | Mathlib.Analysis.Calculus.DifferentialForm.Basic | Mathlib.Topology.Algebra.Module.Alternating.Basic |
| note | Mathlib represents differential `n`-forms as `E → E [⋀^Fin n]→L[𝕜] F`, generalizing the 3D 0/1/2/3-form classification. | Mathlib represents differential `n`-forms via `ContinuousAlternatingMap` (notation `E [⋀^Fin n]→L[𝕜] F`), generalizing the 3D 0/1/2/3-form classification. |
addedAngular speed equals half the curl magnitudef436f25d49ae
addedMagnetic vector potentialf273e733714d
addedGeneralized Stokes' theorem (for differential forms)8723026273de