Physlib.Units.WithDim.Speed

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Units.WithDim.Basic

Speed

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

@[expose] public section

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

abbrev DimSpeed : Type := Dimensionful (WithDim (L𝓭 * T𝓭⁻¹) ℝ≥0)

Basic speeds

Speed in SI units

              @[simp]
lemma oneMeterPerSecond_in_SI : oneMeterPerSecond SI = ⟨1⟩ := by⊢ ↑oneMeterPerSecond SI = { val := 1 }
  simp [oneMeterPerSecond, toDimensionful_apply_apply]All goals completed! 🐙@[simp]
lemma oneMilePerHour_in_SI : oneMilePerHour SI = ⟨0.44704⟩ := by⊢ ↑oneMilePerHour SI = { val := 0.44704 }
  simp [oneMilePerHour, dimScale, LengthUnit.miles, TimeUnit.hours, toDimensionful_apply_apply]⊢ (⟨1609.344, ⋯⟩ * ⟨60 * 60, ⋯⟩ ^ (-1)) • { val := 1 } = { val := 0.44704 }
  ext⊢ ↑((⟨1609.344, ⋯⟩ * ⟨60 * 60, ⋯⟩ ^ (-1)) • { val := 1 }).val = ↑{ val := 0.44704 }.val
  simp [NNReal.coe_ofScientific]⊢ ↑⟨1609.344, ⋯⟩ * ↑⟨60 * 60, ⋯⟩ ^ (-1) = 0.44704
  norm_num [toReal]All goals completed! 🐙@[simp]
lemma oneKilometerPerHour_in_SI :
    oneKilometerPerHour SI = ⟨5/18⟩ := by⊢ ↑oneKilometerPerHour SI = { val := 5 / 18 }
  simp [oneKilometerPerHour, dimScale,
    LengthUnit.kilometers, TimeUnit.hours, toDimensionful_apply_apply]⊢ (⟨10 ^ 3, ⋯⟩ * ⟨60 * 60, ⋯⟩ ^ (-1)) • { val := 1 } = { val := 5 / 18 }
  ext⊢ ↑((⟨10 ^ 3, ⋯⟩ * ⟨60 * 60, ⋯⟩ ^ (-1)) • { val := 1 }).val = ↑{ val := 5 / 18 }.val
  simp only [WithDim.smul_val, smul_eq_mul, mul_one, NNReal.coe_mul, coe_rpow, NNReal.coe_div,
    NNReal.coe_ofNat]⊢ ↑⟨10 ^ 3, ⋯⟩ * ↑⟨60 * 60, ⋯⟩ ^ (-1) = 5 / 18
  norm_num [toReal]All goals completed! 🐙@[simp]
lemma oneKnot_in_SI : oneKnot SI = ⟨463/900⟩ := by⊢ ↑oneKnot SI = { val := 463 / 900 }
  simp [oneKnot, dimScale, LengthUnit.nauticalMiles, TimeUnit.hours, toDimensionful_apply_apply]⊢ (⟨1852, ⋯⟩ * ⟨60 * 60, ⋯⟩ ^ (-1)) • { val := 1 } = { val := 463 / 900 }
  ext⊢ ↑((⟨1852, ⋯⟩ * ⟨60 * 60, ⋯⟩ ^ (-1)) • { val := 1 }).val = ↑{ val := 463 / 900 }.val
  simp only [WithDim.smul_val, smul_eq_mul, mul_one, NNReal.coe_mul, coe_rpow, NNReal.coe_div,
    NNReal.coe_ofNat]⊢ ↑⟨1852, ⋯⟩ * ↑⟨60 * 60, ⋯⟩ ^ (-1) = 463 / 900
  norm_num [toReal]All goals completed! 🐙@[simp]
lemma speedOfLight_in_SI : speedOfLight SI = ⟨299792458⟩ := by⊢ ↑speedOfLight SI = { val := 299792458 }
  simp [speedOfLight, toDimensionful_apply_apply]All goals completed! 🐙

Relations between speeds

              lemma oneKnot_eq_mul_oneKilometerPerHour :
    oneKnot = (1.852 : ℝ≥0) • oneKilometerPerHour := by⊢ oneKnot = 1.852 • oneKilometerPerHour
  apply (toDimensionful SI).symm.injective⊢ (toDimensionful SI).symm oneKnot = (toDimensionful SI).symm (1.852 • oneKilometerPerHour)
  ext⊢ ↑((toDimensionful SI).symm oneKnot).val = ↑((toDimensionful SI).symm (1.852 • oneKilometerPerHour)).val
  norm_num [toDimensionful]All goals completed! 🐙lemma oneKilometerPerHour_eq_mul_oneKnot:
    oneKilometerPerHour = (250/463 : ℝ≥0) • oneKnot := by⊢ oneKilometerPerHour = (250 / 463) • oneKnot
  apply (toDimensionful SI).symm.injective⊢ (toDimensionful SI).symm oneKilometerPerHour = (toDimensionful SI).symm ((250 / 463) • oneKnot)
  ext⊢ ↑((toDimensionful SI).symm oneKilometerPerHour).val = ↑((toDimensionful SI).symm ((250 / 463) • oneKnot)).val
  norm_num [toDimensionful]All goals completed! 🐙lemma oneMeterPerSecond_eq_mul_oneMilePerHour :
    oneMeterPerSecond = (3125/1397 : ℝ≥0) • oneMilePerHour := by⊢ oneMeterPerSecond = (3125 / 1397) • oneMilePerHour
  apply (toDimensionful SI).symm.injective⊢ (toDimensionful SI).symm oneMeterPerSecond = (toDimensionful SI).symm ((3125 / 1397) • oneMilePerHour)
  ext⊢ ↑((toDimensionful SI).symm oneMeterPerSecond).val = ↑((toDimensionful SI).symm ((3125 / 1397) • oneMilePerHour)).val
  norm_num [toDimensionful]All goals completed! 🐙