Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 5 research declarations. Search 10,000 more complete Mathlib declarations.
5 results
Clear filtersClassicalMechanics.HarmonicOscillator.massMetricVal_contMDiff
Plain-language statement
The oscillator mass metric is constant in the global tangent-bundle chart.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.HarmonicOscillator.massMetricVal_isVonNBounded
Plain-language statement
The mass metric unit ball is bounded in the model norm.
Source project: Physlib
Person-level attribution pending.
RigidBody.rotationalKineticEnergy_eq_integral
Plain-language statement
The rotational kinetic energy equals the mass integral of the local rotational speed squared: T = ½ ∫ |ω × r|² dm.
Source project: Physlib
Person-level attribution pending.
RigidBodyMotion.kineticEnergy_eq_translational_add_bodyAngularVelocity
Project documentation
König's theorem in the body frame. The total kinetic energy M.kineticEnergy t, formed from the lab-frame point velocities, splits at the centre of mass (centerOfMass = 0) as T = ½ M ⟪V, V⟫ + rotationalKineticEnergy ω_body. The rotational energy is a frame-independent scalar, so it is evaluated here from the body-frame angular velocity ω_body...
Source project: Physlib
Person-level attribution pending.
RigidBodyMotion.kineticEnergy_integrand_split
Plain-language statement
The squared-speed integrand of kineticEnergy splits into the squared rotational speed |Ṙ (y − c)|², a term linear in the body-frame coordinate y − c, and the constant squared centre-of-mass speed ⟪V, V⟫.
Source project: Physlib
Person-level attribution pending.