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 2,569 research declarations. Search 10,000 more complete Mathlib declarations.
Showing 481 to 486 of 2,569 results.
ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity_eq_zero_iff_exists_int
Mathematical statement
For nonzero amplitude, the velocity is zero exactly at phase times φ + nπ.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity_eq_zero_iff_norm_eq_amplitude
Mathematical statement
The velocity vanishes exactly when the trajectory has norm equal to the amplitude.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.HarmonicOscillator.kineticEnergy_deriv
Project documentation
The energy of the harmonic oscillator is the kinetic energy plus the potential energy. -/ noncomputable def energy (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : Time → ℝ := fun t => kineticEnergy S xₜ t + potentialEnergy S (xₜ t) /-! ### C.2. Simple equalities for the energies -/ lemma kineticEnergy_eq (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : kineticEnergy S x...
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.HarmonicOscillator.massMetricVal_contMDiff
Mathematical statement
The oscillator mass metric is constant in the global tangent-bundle chart.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.HarmonicOscillator.massMetricVal_isVonNBounded
Mathematical statement
The mass metric unit ball is bounded in the model norm.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.HarmonicOscillator.return_time
Mathematical statement
Assuming that the initial coordinate and velocity are not simultaneously zero, the time stamps when the harmonic oscillator returns to its initial coordinate and velocity is a multiple of its period
Source project: Physlib
Person-level attribution pending.