Revision #984 → #1970 · back to history
modifiedAction (informal)12f3df295cc2
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No notion of physical 'action' (kinetic minus potential energy along a trajectory) is formalized in Mathlib. |
| status | — | not_formalized |
modifiedAction for single particle (uniform motion)970db218bd98
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no formalization of momentum or particle action. |
| status | — | not_formalized |
modifiedAction as functional0a84ece47d2f
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No action functional is defined in Mathlib. |
| status | — | not_formalized |
modifiedAction of a ball in gravity188b159d9513
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | This concrete physics example has no Mathlib counterpart. |
| status | — | not_formalized |
addedLagrangian (generalization of KE − PE)50bd70b0b4f4
modifiedPlanck's quantum of action65544edf02ba
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The Planck constant is not formalized in Mathlib. |
| status | — | not_formalized |
addedReduced Planck constant ħ = h/2π85e9f1835739
modifiedAction integral with Lagrangiand3966020a0e9
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No action integral of a Lagrangian along a path is formalized. |
| status | — | not_formalized |
modifiedAction functional 𝒮[q(t)]76eed9f9b00e
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No definition of 𝒮[q(t)] as a Lagrangian time-integral exists in Mathlib. |
| status | — | not_formalized |
modifiedHamilton's principle704702d87511
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Hamilton's principle of stationary action is not in Mathlib (only Hamiltonian graphs/charpoly). |
| status | — | not_formalized |
modifiedAbbreviated actiona0b6bbe8e1e0
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No abbreviated action functional in Mathlib. |
| status | — | not_formalized |
modifiedMaupertuis's principle070eb1841e16
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No occurrences of Maupertuis in Mathlib. |
| status | — | not_formalized |
modifiedHamilton's characteristic function368a7fef30be
| Field | From #984 | To #1970 |
|---|
| anchor.section | Hamilton–Jacobi equation | Hamilton's characteristic function |
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Hamilton's characteristic function W is not formalized in Mathlib. |
| provenance | ai-agent1 | ai-moderated |
| status | — | not_formalized |
modifiedAction of generalized coordinate J_k41ae09144165
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Action-angle coordinates are not present in Mathlib. |
| status | — | not_formalized |
modifiedAction of relativistic point particle1803d23dc072
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No relativistic particle action, world line, or proper time in Mathlib. |
| status | — | not_formalized |
addedMetric tensor signature (mostly plus)c0b362a90d63
modifiedStationary action principle2e9a3636c818
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Stationary/least-action principle is not formalized in Mathlib. |
| status | — | not_formalized |
modifiedMaupertuis's principle (least length)dbe3ac96197c
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Maupertuis's principle has no Mathlib counterpart. |
| status | — | not_formalized |
modifiedHamilton's principle (integral equation)eef6cc3c2c09
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No formulation of Hamilton's variational principle exists in Mathlib. |
| status | — | not_formalized |
modifiedHamilton's principal function55fa5fa68327
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Hamilton's principal function S(q,t;q0,t0) is not in Mathlib. |
| status | — | not_formalized |
addedHamilton–Jacobi equationc3c97ce4bc42
modifiedEuler–Lagrange equations767d6daa04e4
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Euler–Lagrange equations are formalized in Mathlib (no calculus-of-variations infrastructure). |
| status | — | not_formalized |
addedMaxwell's equations from stationary action17c0a9484560
addedEinstein–Hilbert action1b6a52712963
addedFree-fall trajectory is a geodesic948c104b2521
modifiedNoether's theorem0ed9b230ca5b
| Field | From #984 | To #1970 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Noether's theorem (symmetry → conservation law) is not in Mathlib; all 'Noether' hits concern Noetherian rings/modules/spaces. |
| status | — | not_formalized |
addedPath integral (sum over paths)8872385872fb