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 591 research declarations. Search 10,000 more complete Mathlib declarations.
591 results
Clear filtersClassicalMechanics.DampedHarmonicOscillator.trajectory_equationOfMotion_of_overdamped
Plain-language statement
In the overdamped regime, the selected trajectory satisfies the damped equation of motion.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.DampedHarmonicOscillator.trajectory_equationOfMotion_of_underdamped
Plain-language statement
In the underdamped regime, the selected trajectory satisfies the damped equation of motion.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.DampedHarmonicOscillator.trajectory_velocity_at_zero
Plain-language statement
The selected trajectory has initial velocity IC.v₀.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.euler_lagrange_varGradient
Project documentation
The Euler Lagrange operator, for a trajectory q : Time → X, and a lagrangian Time → X → X → ℝ, the Euler-Lagrange operator is ∂L/∂q - dₜ(∂L/∂(dₜ q)). -/ noncomputable def eulerLagrangeOp (L : Time → X → X → ℝ) (q : Time → X) : Time → X := fun t => gradient (L t · (∂ₜ q t)) (q t) - ∂ₜ (fun t' => gradient (L t' (q t') ·) (∂ₜ q t')) t lemma eulerLagran...
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.HarmonicOscillator.AmplitudePhase.toInitialConditions_fromInitialConditions
Plain-language statement
fromInitialConditions is a right inverse of toInitialConditions: converting initial conditions to amplitude–phase form and back recovers them exactly.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_hamiltonEqOp_eq_zero
Project documentation
The operator on the momentum-position phase-space whose vanishing is equivalent to the hamilton's equations between the momentum and position. -/ noncomputable def hamiltonEqOp (p : Time → EuclideanSpace ℝ (Fin 1)) (q : Time → EuclideanSpace ℝ (Fin 1)) := ClassicalMechanics.hamiltonEqOp (hamiltonian S) p q /-! ### G.5. Equation of motion if and only if Ha...
Source project: Physlib
Person-level attribution pending.