Research proof index

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...

The hamiltonian as a function of time, momentum and position. -/ noncomputable def hamiltonian (t : Time) (p : EuclideanSpace ℝ (Fin 1)) (x : EuclideanSpace ℝ (Fin 1)) : ℝ := ⟪p, (toCanonicalMomentum S t x).symm p⟫_ℝ - S.lagrangian t x ((toCanonicalMomentum S t x).symm p) /-! #### G.2.1. Equality for the Hamiltonian We prove a simple equality for the Hami...

The trajectories to the equation of motion for a given set of initial conditions are unique. Given any smooth x satisfying the equation of motion with the same initial position and velocity, the difference y = x - IC.trajectory S also solves the equation of motion with zero initial conditions; energy conservation then forces its energy, and hence y,...

For zero initial conditions, the trajectory is zero. -/ @[simp] lemma trajectory_zero : trajectory S 0 = fun _ => 0 := by simp [trajectory_eq] /-! ### B.3. Smoothness of the trajectories The trajectories for any initial conditions are smooth functions of time. -/ @[fun_prop] lemma trajectory_contDiff (S : HarmonicOscillator) (IC : InitialConditions) {n :...

For nonzero amplitude, the trajectory passes through zero exactly at phase times φ + (2n + 1)π / 2.

For a set of initial conditions IC the position of the solution at time 0 is IC.x₀. -/ @[simp] lemma trajectory_position_at_zero (IC : InitialConditions) : IC.trajectory S 0 = IC.x₀ := by simp [trajectory] @[simp] lemma trajectory_velocity_at_zero (IC : InitialConditions) : ∂ₜ (IC.trajectory S) 0 = IC.v₀ := by simp [trajectory_velocity] /-! ## C. Tr...