Speed

In this module we define the dimensionful type corresponding to an speed. We define specific insances of speed, such as miles per hour, kilometers per hour, etc.

@[reducible, inline]

abbrev DimSpeed : Type

The type of speeds in the absence of a choice of unit.

Equations

• DimSpeed = Dimensionful (WithDim (Dimension.L𝓭 * Dimension.T𝓭⁻¹) NNReal)

Basic speeds

noncomputable def DimSpeed.oneMeterPerSecond : DimSpeed

The dimensional speed corresponding to 1 meter per second.

Equations

• DimSpeed.oneMeterPerSecond = (CarriesDimension.toDimensionful UnitChoices.SI) { val := 1 }

noncomputable def DimSpeed.oneMilePerHour : DimSpeed

The dimensional speed corresponding to 1 mile per hour.

Equations

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

noncomputable def DimSpeed.oneKilometerPerHour : DimSpeed

The dimensional speed corresponding to 1 kilometer per hour.

Equations

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

noncomputable def DimSpeed.oneKnot : DimSpeed

The dimensional speed corresponding to 1 knot, aka, one nautical mile per hour.

Equations

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

noncomputable def DimSpeed.speedOfLight : Dimensionful (WithDim (Dimension.L𝓭 * Dimension.T𝓭⁻¹) ℝ)

The dimensionful speed of light correspnoding to 299792458 meters per second.

Equations

• DimSpeed.speedOfLight = (CarriesDimension.toDimensionful UnitChoices.SI) { val := 299792458 }

Speed in SI units

@[simp]

theorem DimSpeed.oneMeterPerSecond_in_SI : ↑oneMeterPerSecond UnitChoices.SI = { val := 1 }

@[simp]

theorem DimSpeed.oneMilePerHour_in_SI : ↑oneMilePerHour UnitChoices.SI = { val := 0.44704 }

@[simp]

theorem DimSpeed.oneKilometerPerHour_in_SI : ↑oneKilometerPerHour UnitChoices.SI = { val := 5 / 18 }

@[simp]

theorem DimSpeed.oneKnot_in_SI : ↑oneKnot UnitChoices.SI = { val := 463 / 900 }

@[simp]

theorem DimSpeed.speedOfLight_in_SI : ↑speedOfLight UnitChoices.SI = { val := 299792458 }

Relations between speeds

theorem DimSpeed.oneKnot_eq_mul_oneKilometerPerHour : oneKnot = 1.852 • oneKilometerPerHour

theorem DimSpeed.oneKilometerPerHour_eq_mul_oneKnot : oneKilometerPerHour = (250 / 463) • oneKnot

theorem DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour : oneMeterPerSecond = (3125 / 1397) • oneMilePerHour