instance instNormedAddCommGroupScalar {d : UnitsSystem.Dimensions} : NormedAddCommGroup (UnitsSystem.Scalar d)

Equations

• One or more equations did not get rendered due to their size.

theorem dist_def {d : UnitsSystem.Dimensions} (a1 a2 : UnitsSystem.Scalar d) : dist a1 a2 = |a1.val - a2.val|

theorem norm_def {d : UnitsSystem.Dimensions} (t : UnitsSystem.Scalar d) : ‖t‖ = |t.val|

instance instNormedSpaceRealScalar {d : UnitsSystem.Dimensions} : NormedSpace ℝ (UnitsSystem.Scalar d)

Equations

• instNormedSpaceRealScalar = { toMulAction := UnitsSystem.Scalar.instModule.toMulAction, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯, norm_smul_le := ⋯ }

theorem open_set_iff {d : UnitsSystem.Dimensions} (S : Set (UnitsSystem.Scalar d)) : IsOpen S ↔ IsOpen {x : ℝ | { val := x } ∈ S}

theorem differentiable_real_cast {d : UnitsSystem.Dimensions} : Differentiable ℝ fun (t : UnitsSystem.Scalar d) => t.val

theorem isdifferentiable_phys_lift {d : UnitsSystem.Dimensions} : Differentiable ℝ fun (t : ℝ) => { val := t }

theorem differ3 (K : Type u_1) [NormedAddCommGroup K] [NormedSpace ℝ K] (f : ℝ → ℝ) (g : ℝ → K) (h1 : Differentiable ℝ f) (h2 : Differentiable ℝ g) : Differentiable ℝ (g ∘ f)

def physlift (d1 d2 : UnitsSystem.Dimensions) (f : ℝ → ℝ) : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2

Equations

• physlift d1 d2 f t = { val := f t.val }

def mathcast {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) : ℝ → ℝ

Equations

• mathcast f t = (f { val := t }).val

theorem physlift_def (d1 d2 : UnitsSystem.Dimensions) (f : ℝ → ℝ) : physlift d1 d2 f = fun (t : UnitsSystem.Scalar d1) => { val := f t.val }

theorem mathcast_def {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) : mathcast f = fun (t : ℝ) => (f { val := t }).val

theorem physfunc_eq_iff {d1 d2 : UnitsSystem.Dimensions} (f1 f2 : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) : f1 = f2 ↔ mathcast f1 = mathcast f2

theorem lift_cast_inverse (d1 d2 : UnitsSystem.Dimensions) (f : ℝ → ℝ) : mathcast (physlift d1 d2 f) = f

theorem cast_lift_inverse {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) : physlift d1 d2 (mathcast f) = f

theorem physlift_dif (f : ℝ → ℝ) (d1 d2 : UnitsSystem.Dimensions) (h : Differentiable ℝ f) : Differentiable ℝ (physlift d1 d2 f)

theorem mathcast_dif {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) (h : Differentiable ℝ f) : Differentiable ℝ (mathcast f)

noncomputable def physderiv {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) : UnitsSystem.Scalar d1 → UnitsSystem.Scalar (d2 - d1)

Equations

• physderiv f x = { val := deriv (mathcast f) x.val }

theorem physderiv_def {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) : physderiv f = fun (x : UnitsSystem.Scalar d1) => { val := deriv (mathcast f) x.val }

theorem deriv_mathphys {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) : mathcast (physderiv f) = deriv (mathcast f)

def physmapmul {d1 d2 d3 : UnitsSystem.Dimensions} (f1 : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) (f2 : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d3) : UnitsSystem.Scalar d1 → UnitsSystem.Scalar (d2 + d3)

Equations

• physmapmul f1 f2 x = f1 x * f2 x

theorem phymapmul_def {d1 d2 d3 : UnitsSystem.Dimensions} (f1 : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) (f2 : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d3) : physmapmul f1 f2 = fun (x : UnitsSystem.Scalar d1) => f1 x * f2 x

noncomputable def physmapdiv {d1 d2 d3 : UnitsSystem.Dimensions} (f1 : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) (f2 : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d3) : UnitsSystem.Scalar d1 → UnitsSystem.Scalar (d2 - d3)

Equations

• physmapdiv f1 f2 x = f1 x / f2 x

theorem phymapmdiv_def {d1 d2 d3 : UnitsSystem.Dimensions} (f1 : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) (f2 : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d3) : physmapdiv f1 f2 = fun (x : UnitsSystem.Scalar d1) => f1 x / f2 x

def physmapsmul {d1 d2 d3 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d3) (a : UnitsSystem.Scalar d2) : UnitsSystem.Scalar d1 → UnitsSystem.Scalar (d2 + d3)

Equations

• physmapsmul f a x = a * f x

theorem phymapsmul_def {d1 d2 d3 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) (a : UnitsSystem.Scalar d3) : physmapsmul f a = fun (x : UnitsSystem.Scalar d1) => a * f x

theorem smul_cast {d1 d2 d3 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d3) (a : UnitsSystem.Scalar d2) : mathcast (physmapsmul f a) = a.val • mathcast f

def physmapcast {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) (d3 d4 : UnitsSystem.Dimensions) (h1 : d1 = d3) (h2 : d2 = d4) : UnitsSystem.Scalar d3 → UnitsSystem.Scalar d4

Equations

• physmapcast f d3 d4 h1 h2 a = (f (a.cast h1)).cast ⋯

theorem phymapcast_def {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) (d3 d4 : UnitsSystem.Dimensions) (h1 : d1 = d3) (h2 : d2 = d4) : physmapcast f d3 d4 h1 h2 = fun (a : UnitsSystem.Scalar d3) => (f (a.cast h1)).cast ⋯

theorem map_cast_matheq {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) (d3 d4 : UnitsSystem.Dimensions) (h1 : d1 = d3) (h2 : d2 = d4) : mathcast f = mathcast (physmapcast f d3 d4 h1 h2)

def physlift' (d1 : UnitsSystem.Dimensions) (f : ℝ → ℝ) : ℝ → UnitsSystem.Scalar d1

Equations

• physlift' d1 f t = { val := f t }

def mathcast' {d1 : UnitsSystem.Dimensions} (f : ℝ → UnitsSystem.Scalar d1) : ℝ → ℝ

Equations

• mathcast' f t = (f t).val

theorem physlift_def' (d1 : UnitsSystem.Dimensions) (f : ℝ → ℝ) : physlift' d1 f = fun (t : ℝ) => { val := f t }

theorem mathcast_def' {d1 : UnitsSystem.Dimensions} (f : ℝ → UnitsSystem.Scalar d1) : mathcast' f = fun (t : ℝ) => (f t).val

theorem physfunc_eq_iff' {d1 : UnitsSystem.Dimensions} (f1 f2 : ℝ → UnitsSystem.Scalar d1) : f1 = f2 ↔ mathcast' f1 = mathcast' f2

theorem lift_cast_inverse' {d1 : UnitsSystem.Dimensions} (f : ℝ → ℝ) : mathcast' (physlift' d1 f) = f

theorem cast_lift_inverse' {d1 : UnitsSystem.Dimensions} (f : ℝ → UnitsSystem.Scalar d1) : physlift' d1 (mathcast' f) = f

theorem physlift_dif' (f : ℝ → ℝ) (d1 : UnitsSystem.Dimensions) (h : Differentiable ℝ f) : Differentiable ℝ (physlift' d1 f)

theorem mathcast_dif' {d1 : UnitsSystem.Dimensions} (f : ℝ → UnitsSystem.Scalar d1) (h : Differentiable ℝ f) : Differentiable ℝ (mathcast' f)

noncomputable def physderiv' {d1 : UnitsSystem.Dimensions} (f : ℝ → UnitsSystem.Scalar d1) : ℝ → UnitsSystem.Scalar d1

Equations

• physderiv' f x = { val := deriv (mathcast' f) x }

theorem physderiv_def' {d1 : UnitsSystem.Dimensions} (f : ℝ → UnitsSystem.Scalar d1) : physderiv' f = fun (x : ℝ) => { val := deriv (mathcast' f) x }

theorem deriv_mathphys' {d1 : UnitsSystem.Dimensions} (f : ℝ → UnitsSystem.Scalar d1) : mathcast' (physderiv' f) = deriv (mathcast' f)

def physmapmul' {d1 d2 : UnitsSystem.Dimensions} (f1 : ℝ → UnitsSystem.Scalar d1) (f2 : ℝ → UnitsSystem.Scalar d2) : ℝ → UnitsSystem.Scalar (d1 + d2)

Equations

• physmapmul' f1 f2 x = f1 x * f2 x

theorem physmapmul_def' {d1 d2 : UnitsSystem.Dimensions} (f1 : ℝ → UnitsSystem.Scalar d1) (f2 : ℝ → UnitsSystem.Scalar d2) : physmapmul' f1 f2 = fun (x : ℝ) => f1 x * f2 x

noncomputable def physmapdiv' {d1 d2 : UnitsSystem.Dimensions} (f1 : ℝ → UnitsSystem.Scalar d1) (f2 : ℝ → UnitsSystem.Scalar d2) : ℝ → UnitsSystem.Scalar (d1 - d2)

Equations

• physmapdiv' f1 f2 x = f1 x / f2 x

theorem phymapmdiv_def' {d1 d2 : UnitsSystem.Dimensions} (f1 : ℝ → UnitsSystem.Scalar d1) (f2 : ℝ → UnitsSystem.Scalar d2) : physmapdiv' f1 f2 = fun (x : ℝ) => f1 x / f2 x

def physmapsmul' {d1 d2 : UnitsSystem.Dimensions} (f : ℝ → UnitsSystem.Scalar d1) (a : UnitsSystem.Scalar d2) : ℝ → UnitsSystem.Scalar (d1 + d2)

Equations

• physmapsmul' f a x = f x * a

theorem phymapsmul_def' {d1 d2 : UnitsSystem.Dimensions} (f : ℝ → UnitsSystem.Scalar d1) (a : UnitsSystem.Scalar d2) : physmapsmul' f a = fun (x : ℝ) => f x * a

theorem smul_cast' {d1 d2 : UnitsSystem.Dimensions} (f : ℝ → UnitsSystem.Scalar d1) (a : UnitsSystem.Scalar d2) : mathcast' (physmapsmul' f a) = a.val • mathcast' f

def physmapcast' {d1 d2 : UnitsSystem.Dimensions} (f : ℝ → UnitsSystem.Scalar d1) (h : d1 = d2) : ℝ → UnitsSystem.Scalar d2

Equations

• physmapcast' f h a = (f a).cast ⋯

theorem phymapcast_def' {d1 d2 : UnitsSystem.Dimensions} (f : ℝ → UnitsSystem.Scalar d1) (h : d1 = d2) : physmapcast' f h = fun (a : ℝ) => (f a).cast ⋯

theorem map_cast_matheq' {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2) (d3 d4 : UnitsSystem.Dimensions) (h1 : d1 = d3) (h2 : d2 = d4) : mathcast f = mathcast (physmapcast f d3 d4 h1 h2)

def physlift'' (d1 : UnitsSystem.Dimensions) (f : ℝ → ℝ) : UnitsSystem.Scalar d1 → ℝ

Equations

• physlift'' d1 f t = f t.val

def mathcast'' {d1 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → ℝ) : ℝ → ℝ

Equations

• mathcast'' f t = f { val := t }

theorem physlift_def'' (d1 : UnitsSystem.Dimensions) (f : ℝ → ℝ) : physlift'' d1 f = fun (t : UnitsSystem.Scalar d1) => f t.val

theorem mathcast_def'' {d1 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → ℝ) : mathcast'' f = fun (t : ℝ) => f { val := t }

theorem physfunc_eq_iff'' {d1 : UnitsSystem.Dimensions} (f1 f2 : UnitsSystem.Scalar d1 → ℝ) : f1 = f2 ↔ mathcast'' f1 = mathcast'' f2

theorem lift_cast_inverse'' (d1 : UnitsSystem.Dimensions) (f : ℝ → ℝ) : mathcast'' (physlift'' d1 f) = f

theorem cast_lift_inverse'' {d1 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → ℝ) : physlift'' d1 (mathcast'' f) = f

theorem physlift_dif'' (f : ℝ → ℝ) (d1 : UnitsSystem.Dimensions) (h : Differentiable ℝ f) : Differentiable ℝ (physlift'' d1 f)

theorem mathcast_dif'' {d1 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → ℝ) (h : Differentiable ℝ f) : Differentiable ℝ (mathcast'' f)

noncomputable def physderiv'' {d1 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → ℝ) : UnitsSystem.Scalar d1 → UnitsSystem.Scalar (-d1)

Equations

• physderiv'' f x = { val := deriv (mathcast'' f) x.val }

theorem physderiv_def'' {d1 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → ℝ) : physderiv'' f = fun (x : UnitsSystem.Scalar d1) => { val := deriv (mathcast'' f) x.val }

theorem deriv_mathphys'' {d1 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → ℝ) : mathcast (physderiv'' f) = deriv (mathcast'' f)

def physmapmul'' {d1 : UnitsSystem.Dimensions} (f1 f2 : ℝ → UnitsSystem.Scalar d1) : ℝ → UnitsSystem.Scalar (2 • d1)

Equations

• physmapmul'' f1 f2 x = (f1 x * f2 x).cast ⋯

theorem physmapmul_def'' {d1 : UnitsSystem.Dimensions} (f1 f2 : ℝ → UnitsSystem.Scalar d1) : physmapmul'' f1 f2 = fun (x : ℝ) => (f1 x * f2 x).cast ⋯

noncomputable def physmapdiv'' {d1 : UnitsSystem.Dimensions} (f1 f2 : UnitsSystem.Scalar d1 → ℝ) : ℝ → ℝ

Equations

• physmapdiv'' f1 f2 x = f1 { val := x } / f2 { val := x }

theorem phymapmdiv_def'' {d1 : UnitsSystem.Dimensions} (f1 f2 : UnitsSystem.Scalar d1 → ℝ) : physmapdiv'' f1 f2 = fun (x : ℝ) => f1 { val := x } / f2 { val := x }

def physmapsmul'' {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → ℝ) (a : UnitsSystem.Scalar d2) : UnitsSystem.Scalar d1 → UnitsSystem.Scalar d2

Equations

• physmapsmul'' f a x = f x • a

theorem phymapsmul_def'' {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → ℝ) (a : UnitsSystem.Scalar d2) : physmapsmul'' f a = fun (x : UnitsSystem.Scalar d1) => f x • a

theorem smul_cast'' {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → ℝ) (a : UnitsSystem.Scalar d2) : mathcast (physmapsmul'' f a) = a.val • mathcast'' f

def physmapcast'' {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → ℝ) (h : d1 = d2) : UnitsSystem.Scalar d2 → ℝ

Equations

• physmapcast'' f h a = f (a.cast h)

theorem phymapcast_def'' {d1 d2 : UnitsSystem.Dimensions} (f : UnitsSystem.Scalar d1 → ℝ) (h : d1 = d2) : physmapcast'' f h = fun (a : UnitsSystem.Scalar d2) => f (a.cast h)

structure OneDimMotion : Type

Basic Kinematics

• pos : SI.Time → SI.Length
• differentiable_pos : Differentiable ℝ self.pos
• vel : SI.Time → SI.Speed
• differentiable_vel : Differentiable ℝ self.vel
• acc : SI.Time → SI.Acceleration
• F : Finset (SI.Time → SI.Force)

structure point_1d : Type

• m : SI.Mass
• motion : OneDimMotion
• Newton (t : SI.Time) : self.m * self.motion.acc t = ∑ f ∈ self.motion.F, f t
• point_toreal : SI.Time → ℝ

structure point_2d : Type

• m : SI.Mass
• motion_x : OneDimMotion
• motion_y : OneDimMotion
• Newtonx (t : SI.Time) : self.m * self.motion_x.acc t = ∑ f ∈ self.motion_x.F, f t
• Newtony (t : SI.Time) : self.m * self.motion_y.acc t = ∑ f ∈ self.motion_y.F, f t
• point_toreal : SI.Time → ℝ × ℝ

structure point_3d : Type

• m : SI.Mass
• motion_x : OneDimMotion
• motion_y : OneDimMotion
• motion_z : OneDimMotion
• Newtonx (t : SI.Time) : self.m * self.motion_x.acc t = ∑ f ∈ self.motion_x.F, f t
• Newtony (t : SI.Time) : self.m * self.motion_y.acc t = ∑ f ∈ self.motion_y.F, f t
• Newtonz (t : SI.Time) : self.m * self.motion_z.acc t = ∑ f ∈ self.motion_z.F, f t
• point_toreal : SI.Time → ℝ × ℝ × ℝ

structure isolate_system_1d : Type

• points : Finset point_1d
• sumforce (t : SI.Time) : ∑ p ∈ self.points, ∑ f ∈ p.motion.F, f t = 0
• summomentum (t : SI.Time) : ∑ p ∈ self.points, p.m * p.motion.vel t = ∑ p ∈ self.points, p.m * p.motion.vel 0

structure isolate_system_2d : Type

• points : Finset point_2d
• sumforce_x (t : SI.Time) : ∑ p ∈ self.points, ∑ f ∈ p.motion_x.F, f t = 0
• summomentum_x (t : SI.Time) : ∑ p ∈ self.points, p.m * p.motion_x.vel t = ∑ p ∈ self.points, p.m * p.motion_x.vel 0
• sumforce_y (t : SI.Time) : ∑ p ∈ self.points, ∑ f ∈ p.motion_y.F, f t = 0
• summomentum_y (t : SI.Time) : ∑ p ∈ self.points, p.m * p.motion_y.vel t = ∑ p ∈ self.points, p.m * p.motion_y.vel 0

structure isolate_system_3d : Type

• points : Finset point_3d
• sumforce_x (t : SI.Time) : ∑ p ∈ self.points, ∑ f ∈ p.motion_x.F, f t = 0
• summomentum (t : SI.Time) : ∑ p ∈ self.points, p.m * p.motion_x.vel t = ∑ p ∈ self.points, p.m * p.motion_x.vel 0
• sumforce_y (t : SI.Time) : ∑ p ∈ self.points, ∑ f ∈ p.motion_y.F, f t = 0
• summomentum_y (t : SI.Time) : ∑ p ∈ self.points, p.m * p.motion_y.vel t = ∑ p ∈ self.points, p.m * p.motion_y.vel 0
• sumforce_z (t : SI.Time) : ∑ p ∈ self.points, ∑ f ∈ p.motion_z.F, f t = 0
• summomentum_z (t : SI.Time) : ∑ p ∈ self.points, p.m * p.motion_z.vel t = ∑ p ∈ self.points, p.m * p.motion_z.vel 0

class axis : Type

Rigid Body Mechanics

• A : Set (ℝ × ℝ × ℝ)
• affine : ∃ (a : ℝ × ℝ × ℝ) (v : ℝ × ℝ × ℝ), v ≠ 0 ∧ ∀ (x : ↑A), ∃ (t : ℝ), ↑x = a + t • v

noncomputable def distance_ptl (a : ℝ × ℝ × ℝ) (l : axis) : ℝ

Equations

• distance_ptl a l = sInf {r : ℝ | ∃ (b : ↑axis.A), dist a ↑b = r}

structure rotating_rigid_body : Type

• points : Set point_3d
• points_toreal : SI.Time → Set (ℝ × ℝ × ℝ)
• Mass' : ℝ × ℝ × ℝ → SI.Mass
• ang_vel : SI.Time → UnitsSystem.Scalar (-SI.time_unit)
• h (x : ℝ × ℝ × ℝ) : x ∉ self.points_toreal 0 → self.Mass' x = 0

noncomputable def rotation_inertia (A : axis) (B : rotating_rigid_body) : UnitsSystem.Scalar (SI.mass_unit + 2 • SI.length_unit)

Equations

• rotation_inertia A B = { val := ∫ (x : ℝ × ℝ × ℝ) in B.points_toreal 0, distance_ptl x A ^ 2 * (B.Mass' x).val }