PhysLean Documentation

PhysLean.ClassicalMechanics.HarmonicOscillator.Solution

Solutions to the classical harmonic oscillator #

i. Overview #

In this module we define the solutions to the classical harmonic oscillator, prove that they satisfy the equation of motion, and prove some properties of the solutions.

ii. Key results #

iii. Table of contents for this module #

iv. References #

References for the classical harmonic oscillator include:

A. The initial conditions #

We define the type of initial conditions for the harmonic oscillator. The initial conditions are currently defined as an initial position and an initial velocity, that is the values of the solution and its time derivative at time 0.

A.1. Definition of the initial conditions #

We start by defining the type of initial conditions for the harmonic oscillator.

The initial conditions for the harmonic oscillator specified by an initial position, and an initial velocity.

  • x₀ : Space 1

    The initial position of the harmonic oscillator.

  • v₀ : Space 1

    The initial velocity of the harmonic oscillator.

Instances For

    Part A.1.I #

    We prove an extensionality lemma for InitialConditions. That is, a lemma which states that two initial conditions are equal if their initial positions and initial velocities are equal.

    theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.ext {IC₁ IC₂ : InitialConditions} (h1 : IC₁.x₀ = IC₂.x₀) (h2 : IC₁.v₀ = IC₂.v₀) :
    IC₁ = IC₂

    A.2. Relation to other types of initial conditions #

    We relate the inital condition given by an initial position and an initial velocity to other specifications of initial conditions. This is currently not implemented, and is a TODO.

    A.3. The zero initial conditions #

    The zero initial conditions are the initial conditions with zero initial position and zero initial velocity.

    In the end, we will see that this corresponds to the solution which is identically zero, i.e. the particle remains at rest at the origin.

    Part A.3.I #

    Some simple results about the zero initial conditions.

    @[simp]

    The zero initial condition has zero starting point.

    @[simp]

    The zero initial condition has zero starting velocity.

    B. Trajectories associated with the initial conditions #

    To each initial condition we association a trajectory. We will prove some basic properties of these trajectories.

    Eventually we will show that these trajectories satisfy the equation of motion, for now we can think of them as some choice of trajectory associated with the initial conditions.

    B.1. The trajectory associated with the initial conditions #

    Given initial conditions, the solution to the classical harmonic oscillator.

    Equations
    Instances For

      Part B.1.I #

      We show a basic definitional equality for the trajectory.

      B.2. The trajectory for zero initial conditions #

      The trajectory for zero initial conditions is the zero function.

      @[simp]

      For zero initial conditions, the trajectory is zero.

      B.3. Smoothness of the trajectories #

      The trajectories for any initial conditions are smooth functions of time.

      B.4. Velocity of the trajectories #

      We give a simplification of the velocity of the trajectory.

      B.5. Acceleration of the trajectories #

      We give a simplification of the acceleration of the trajectory.

      ### B.6. The initial conditions of the trajectories

      We show that, unsurprisingly, the trajectories have the initial conditions used to define them.

      @[simp]

      For a set of initial conditions IC the position of the solution at time 0 is IC.x₀.

      C. Trajectories and Equation of motion #

      The trajectories satsify the equation of motion for the harmonic oscillator.

      C.1. Uniqueness of the solutions #

      We show that the trajectories are the unique solutions to the equation of motion for the given initial conditions. This is currently a TODO.

      The trajectories to the equation of motion for a given set of initial conditions are unique.

      Semiformal implmentation:

      • One may needed the added condition of smoothness on x here.
      • EquationOfMotion needs defining before this can be proved.

      D. The energy of the trajectories #

      For a given set of initial conditions, the enrgy of the trajectory is constant, due to the conservation of energy. Here we show it's value.

      E. The trajectories at zero velocity #

      We study the properties of the trajectories when the vleocity is zero.

      E.1. The times at which the velocity is zero #

      We show that if the velocity of the trajectory is zero, then the time satisfies the condition that

      tan (S.ω * t) = IC.v₀ 0 / (S.ω * IC.x₀ 0)
      

      E.2. A time when the velocity is zero #

      We show that as long as the inital position is non-zero, then at the time arctan (IC.v₀ 0 / (S.ω * IC.x₀ 0)) / S.ω the velocity is zero.

      E.3. The position when the velocity is zero #

      We show that the position is equal to √(‖IC.x₀‖^2 + (‖IC.v₀‖/S.ω)^2) when the velocity is zero, as long as the initial conditions are not both zero. This is currently a TODO.

      F. Some open TODOs #

      We give some open TODOs for the classical harmonic oscillator.