scilib documentation

LeanChemicalTheories / physics.kinematic_equations

The equations of motion #

We define motion to be over an inner product space, which is a vector space endowed with an operator caleld the inner product. We generalize motion to be over a field that is either real or complex, and show that three of the four kinematic equations for constant acceleration hold in complex time. The fourth kinematic equation, as of now, can only be derived in real time.

We also define an extension of the motion class to require that our functions be continously differentiable n times. In the future, we plan to define another class extension which only requires the equations of motion to be differentiable on a set. These classes are defined seperatley from the motion class to give flexibility to motion's applicability. We also don't require the equations to be infinitley differentiable, but this can be achieved by using ⊤ for n.

Finally, at the end we derive the four equations of motion for the case of linear translation along a line. Currently, these derivations are independent of the motion class, but in the future, they will be unified with motion and shown to be examples of their vector coutner-part.

To-Do #

Show that the fourth kinematic equations hold in complex time with the nescessary assumptions
Show that the linear translation equations follow from the vector form

structure motion (𝕜 : Type u_1) (E : Type u_2) [normed_add_comm_group E] [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :

Type (max u_1 u_2)

position : 𝕜 → E
velocity : 𝕜 → E
acceleration : 𝕜 → E
hvel : self.velocity = deriv self.position
hacc : self.acceleration = deriv self.velocity

Instances for motion

motion.has_sizeof_inst

structure motion_cont_diff_everywhere (𝕜 : Type u_1) (E : Type u_2) [normed_add_comm_group E] [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :

Type (max u_1 u_2)

to_motion : motion 𝕜 E
contdiff : ∀ (n : with_top ℕ) (m : ℕ), ↑m < n → cont_diff 𝕜 n (deriv ^[m] self.to_motion.position)

Instances for motion_cont_diff_everywhere

motion_cont_diff_everywhere.has_sizeof_inst

theorem acceleration_eq_deriv2_position {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (M : motion 𝕜 E) :

M.acceleration = deriv ^[2] M.position

theorem acceleration_eq_deriv2_position_iff_acceleration_eq_deriv_velocity {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (M : motion 𝕜 E) :

M.acceleration = deriv ^[2] M.position ↔ M.acceleration = deriv M.velocity

theorem deriv2_position_eq_deriv_velocity {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (M : motion 𝕜 E) :

deriv ^[2] M.position = deriv M.velocity

theorem velocity_eq_deriv1_position {𝕜 : Type u_1} {E : Type u_2} [normed_add_comm_group E] [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {M : motion_cont_diff_everywhere 𝕜 E} :

M.to_motion.velocity = deriv ^[1] M.to_motion.position

theorem cont_diff_acceleration {𝕜 : Type u_1} {E : Type u_2} [normed_add_comm_group E] [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {M : motion_cont_diff_everywhere 𝕜 E} {n : with_top ℕ} (hn : 2 < n) :

cont_diff 𝕜 n M.to_motion.acceleration

theorem cont_diff_velocity {𝕜 : Type u_1} {E : Type u_2} [normed_add_comm_group E] [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {M : motion_cont_diff_everywhere 𝕜 E} {n : with_top ℕ} (hn : 1 < n) :

cont_diff 𝕜 n M.to_motion.velocity

theorem cont_diff_position {𝕜 : Type u_1} {E : Type u_2} [normed_add_comm_group E] [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {M : motion_cont_diff_everywhere 𝕜 E} {n : with_top ℕ} (hn : 0 < n) :

cont_diff 𝕜 n M.to_motion.position

theorem acceleration_differentiable {𝕜 : Type u_1} {E : Type u_2} [normed_add_comm_group E] [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {M : motion_cont_diff_everywhere 𝕜 E} {n : with_top ℕ} (hn : 2 < n) :

differentiable 𝕜 M.to_motion.acceleration

theorem velocity_differentiable {𝕜 : Type u_1} {E : Type u_2} [normed_add_comm_group E] [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {M : motion_cont_diff_everywhere 𝕜 E} {n : with_top ℕ} (hn : 1 < n) :

differentiable 𝕜 M.to_motion.velocity

theorem position_differentiable {𝕜 : Type u_1} {E : Type u_2} [normed_add_comm_group E] [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {M : motion_cont_diff_everywhere 𝕜 E} {n : with_top ℕ} (hn : 1 < n) :

differentiable 𝕜 M.to_motion.position

Kinematic equations for translation in a vector field #

theorem const_accel {𝕜 : Type u_1} {E : Type u_2} [normed_add_comm_group E] [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {M : motion_cont_diff_everywhere 𝕜 E} {𝔸 : E} (accel_const : M.to_motion.acceleration = λ (t : 𝕜), 𝔸) {n : with_top ℕ} (hn : 1 < n) :

M.to_motion.velocity = λ (t : 𝕜), t • 𝔸 + M.to_motion.velocity 0

theorem const_accel' {𝕜 : Type u_1} {E : Type u_2} [normed_add_comm_group E] [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {M : motion_cont_diff_everywhere 𝕜 E} {𝔸 : E} (accel_const : M.to_motion.acceleration = λ (t : 𝕜), 𝔸) {n : with_top ℕ} (hn : 1 < n) :

M.to_motion.position = λ (t : 𝕜), (t ^ 2 / 2) • 𝔸 + t • M.to_motion.velocity 0 + M.to_motion.position 0

theorem const_accel'' {𝕜 : Type u_1} {E : Type u_2} [normed_add_comm_group E] [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {M : motion_cont_diff_everywhere 𝕜 E} {𝔸 : E} (accel_const : M.to_motion.acceleration = λ (t : 𝕜), 𝔸) {n : with_top ℕ} (hn : 1 < n) (t : 𝕜) :

M.to_motion.position t = (t / 2) • (M.to_motion.velocity t + M.to_motion.velocity 0) + M.to_motion.position 0

theorem const_accel''' {E : Type u_2} [normed_add_comm_group E] {𝔸 : E} [inner_product_space ℝ E] {N : motion_cont_diff_everywhere ℝ E} (accel_const : N.to_motion.acceleration = λ (t : ℝ), 𝔸) {n : with_top ℕ} (hn : 1 < n) (t : ℝ) :

has_inner.inner (N.to_motion.velocity t) (N.to_motion.velocity t) = has_inner.inner (N.to_motion.velocity 0) (N.to_motion.velocity 0) + 2 * has_inner.inner 𝔸 (N.to_motion.position t - N.to_motion.position 0)

Kinematic equations for translation on a real line #

theorem velocity_eq_const_accel_mul_time {α : ℝ} (x v a : ℝ → ℝ) (hf' : ∀ (t : ℝ), has_deriv_at x (v t) t) (hf'' : ∀ (t : ℝ), has_deriv_at v (a t) t) (accel_const : a = λ (t : ℝ), α) :

v = λ (t : ℝ), α * t + v 0

theorem pos_eq_const_accel_mul_time_sqr_add_velocity_mul_time {α : ℝ} (x v a : ℝ → ℝ) (hf' : ∀ (t : ℝ), has_deriv_at x (v t) t) (hf'' : ∀ (t : ℝ), has_deriv_at v (a t) t) (accel_const : a = λ (t : ℝ), α) :

x = λ (t : ℝ), α * t ^ 2 / 2 + v 0 * t + x 0

theorem pos_eq_velocity_add_initial_mul_time {α : ℝ} (x v a : ℝ → ℝ) (hf' : ∀ (t : ℝ), has_deriv_at x (v t) t) (hf'' : ∀ (t : ℝ), has_deriv_at v (a t) t) (accel_const : a = λ (t : ℝ), α) (t : ℝ) :

x t = (v t + v 0) * t / 2 + x 0

theorem velocity_pow_two_eq_velocity_initial_pow_two_add_accel_mul_pos {α : ℝ} (x v a : ℝ → ℝ) (hf' : ∀ (t : ℝ), has_deriv_at x (v t) t) (hf'' : ∀ (t : ℝ), has_deriv_at v (a t) t) (accel_const : a = λ (t : ℝ), α) (t : ℝ) :

v t ^ 2 = v 0 ^ 2 + 2 * a t * (x t - x 0)