Documentation

PhysLib.Mechanics.Motion

def SI.Mechanics.displacement_end_x_init_x (x2 x1 : Length) :

Equations

SI.Mechanics.displacement_end_x_init_x x2 x1 = x2 - x1

Instances For

@[simp]

theorem SI.Mechanics.displacement_end_x_init_x_eq (x2 x1 : Length) :

displacement_end_x_init_x x2 x1 = x2 - x1

theorem SI.Mechanics.displacement_init_x_to_end_x (x2 x1 dx : Length) (hΔx : dx = displacement_end_x_init_x x2 x1) :

x2 = x1 + dx

def SI.Mechanics.displacement_delta_t_const_v (v : Speed) (t : Time) :

Equations

SI.Mechanics.displacement_delta_t_const_v v t = v * t

Instances For

@[simp]

theorem SI.Mechanics.displacement_delta_t_const_v_eq (v : Speed) (t : Time) :

displacement_delta_t_const_v v t = v * t

theorem SI.Mechanics.displacement_eq (x2 x1 dx1 dx2 : Length) (v : Speed) (t : Time) (hΔx1 : dx1 = displacement_end_x_init_x x2 x1) (hΔx2 : dx2 = displacement_delta_t_const_v v t) (hΔx : dx1 = dx2) :

x2 - x1 = v * t

theorem SI.Mechanics.delta_t_const_v_init_x_to_end_x_version0 (x2 x1 dx1 dx2 : Length) (v : Speed) (t : Time) (hΔx1 : dx1 = displacement_end_x_init_x x2 x1) (hΔx2 : dx2 = displacement_delta_t_const_v v t / 1) (hΔx : dx1 = dx2) :

x2 = v * t / 1 + x1

theorem SI.Mechanics.delta_t_const_v_init_x_to_end_x_version1 (x2 x1 dx1 dx2 : Length) (v : Speed) (t : Time) (hΔx1 : dx1 = displacement_end_x_init_x x2 x1) (hΔx2 : dx2 = displacement_delta_t_const_v v t) (hΔx : dx1 = dx2) :

x2 = x1 + displacement_delta_t_const_v v t

def SI.Mechanics.delta_v_end_v_init_v (v2 v1 : Speed) :

Equations

SI.Mechanics.delta_v_end_v_init_v v2 v1 = v2 - v1

Instances For

@[simp]

theorem SI.Mechanics.delta_v_end_v_init_v_eq (v2 v1 : Speed) :

delta_v_end_v_init_v v2 v1 = v2 - v1

def SI.Mechanics.delta_v_delta_t_const_a (a : Acceleration) (t : Time) :

Equations

SI.Mechanics.delta_v_delta_t_const_a a t = a * t

Instances For

@[simp]

theorem SI.Mechanics.delta_v_delta_t_const_a_eq (a : Acceleration) (t : Time) :

delta_v_delta_t_const_a a t = a * t

theorem SI.Mechanics.delta_v_eq (v2 v1 dv1 dv2 : Speed) (a : Acceleration) (t : Time) (hΔv1 : dv1 = delta_v_end_v_init_v v2 v1) (hΔv2 : dv2 = delta_v_delta_t_const_a a t) (hΔv : dv1 = dv2) :

v2 - v1 = a * t

theorem SI.Mechanics.delta_v_const_a_init_v_to_end_v_version0 (v2 v1 dv1 dv2 : Speed) (a : Acceleration) (t : Time) (hΔv1 : dv1 = delta_v_end_v_init_v v2 v1) (hΔv2 : dv2 = delta_v_delta_t_const_a a t / 1) (hΔv : dv1 = dv2) :

v2 = a * t / 1 + v1

theorem SI.Mechanics.delta_v_const_a_init_v_to_end_v_version1 (v2 v1 dv1 dv2 : Speed) (a : Acceleration) (t : Time) (hΔv1 : dv1 = delta_v_end_v_init_v v2 v1) (hΔv2 : dv2 = delta_v_delta_t_const_a a t) (hΔv : dv1 = dv2) :

v2 = v1 + delta_v_delta_t_const_a a t

theorem SI.Mechanics.disp_const_a_forms_eq (v2 v1 : Speed) (a : Acceleration) (t : Time) (hv : delta_v_end_v_init_v v2 v1 = delta_v_delta_t_const_a a t) :

v1 * t + a * t**2 / 2 = (v2 + v1) / 2 * t

Under constant acceleration, the two displacement formulas are equivalent: v0 * t + (a * t^2)/2 = ((v + v0)/2) * t. This uses only the velocity increment relation v - v0 = a * t.

theorem SI.Mechanics.disp_const_a_forms_eq0 (v2 v1 : Speed) (a : Acceleration) (t : Time) (hv : delta_v_end_v_init_v v2 v1 = delta_v_delta_t_const_a a t) :

v1 * t + a * t**2 / 2 = (v2 + v1) / 2 * t

Under constant acceleration, the two displacement formulas are equivalent: v1 * t + (a * t^2)/2 = ((v2 + v1)/2) * t, using only v2 - v1 = a * t. This avoids having a * t appear directly inside addition.

theorem SI.Mechanics.Testfield.delta_t_const_v_init_x_to_end_x_origin0 (x2 x1 dx1 dx2 : Length) (v : Speed) (t : Time) (hΔx1 : dx1 = displacement_end_x_init_x x2 x1) (hΔx2 : dx2 = displacement_delta_t_const_v v t) (hΔx : dx1 = dx2) :

x2 = x1 + displacement_delta_t_const_v v t