PhysLean Documentation

PhysLean.ClassicalMechanics.Mass.MassUnit

Units on Mass #

A unit of mass corresponds to a choice of translationally-invariant metric on the mass manifold (to be defined diffeomorphic to ℝ≥0). Such a choice is (non-canonically) equivalent to a choice of positive real number. We define the type MassUnit to be equivalent to the positive reals.

On MassUnit there is an instance of division giving a real number, corresponding to the ratio of the two scales of mass unit.

To define specific mass units, we first axiomise the existence of a a given mass unit, and then construct all other mass units from it. We choose to axiomise the existence of the mass unit of kilograms, and construct all other mass units from that.

structure MassUnit :

The choices of translationally-invariant metrics on the mass-manifold. Such a choice corresponds to a choice of units for mass.

  • val :

    The underlying scale of the unit.

  • property : 0 < self.val
Instances For
    @[simp]

    Division of MassUnit #

    Equations
    theorem MassUnit.div_eq_val (x y : MassUnit) :
    x / y = x.val / y.val,
    @[simp]
    theorem MassUnit.div_neq_zero (x y : MassUnit) :
    ¬x / y = 0
    @[simp]
    theorem MassUnit.div_self (x : MassUnit) :
    x / x = 1
    theorem MassUnit.div_symm (x y : MassUnit) :
    x / y = (y / x)⁻¹

    The scaling of a mass unit #

    def MassUnit.scale (r : ) (x : MassUnit) (hr : 0 < r := by norm_num) :

    The scaling of a mass unit by a positive real.

    Equations
    Instances For
      @[simp]
      theorem MassUnit.scale_div_self (x : MassUnit) (r : ) (hr : 0 < r) :
      scale r x hr / x = r,
      @[simp]
      theorem MassUnit.scale_one (x : MassUnit) :
      scale 1 x = x
      @[simp]
      theorem MassUnit.scale_div_scale (x1 x2 : MassUnit) {r1 r2 : } (hr1 : 0 < r1) (hr2 : 0 < r2) :
      scale r1 x1 hr1 / scale r2 x2 hr2 = r1, / r2, * (x1 / x2)
      @[simp]
      theorem MassUnit.scale_scale (x : MassUnit) (r1 r2 : ) (hr1 : 0 < r1) (hr2 : 0 < r2) :
      scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x

      Specific choices of mass units #

      To define a specific mass units, we must first axiomise the existence of a a given mass unit, and then construct all other mass units from it. We choose to axiomise the existence of the mass unit of kilograms.

      We need an axiom since this relates something to something in the physical world.

      The axiom corresponding to the definition of a mass unit of kilograms.

      noncomputable def MassUnit.micrograms :

      The mass unit of a microgram (10^(-9) of a kilogram).

      Equations
      Instances For
        noncomputable def MassUnit.milligrams :

        The mass unit of milligram (10^(-6) of a kilogram).

        Equations
        Instances For
          noncomputable def MassUnit.grams :

          The mass unit of grams (10^(-3) of a kilogram).

          Equations
          Instances For
            noncomputable def MassUnit.ounces :

            The mass unit of (avoirdupois) ounces (0.028 349 523 125 of a kilogram).

            Equations
            Instances For
              noncomputable def MassUnit.pounds :

              The mass unit of (avoirdupois) pounds (0.453 592 37 of a kilogram).

              Equations
              Instances For
                noncomputable def MassUnit.stones :

                The mass unit of stones (14 pounds).

                Equations
                Instances For
                  noncomputable def MassUnit.quarters :

                  The mass unit of a quarter (28 pounds).

                  Equations
                  Instances For

                    The mass unit of hundredweights (112 pounds).

                    Equations
                    Instances For
                      noncomputable def MassUnit.shortTons :

                      The mass unit of short tons (2000 pounds).

                      Equations
                      Instances For
                        noncomputable def MassUnit.metricTons :

                        The mass unit of metric tons (1000 kilograms).

                        Equations
                        Instances For
                          noncomputable def MassUnit.longTons :

                          The mass unit of long tons (2240 pounds). Also called shortweight tons.

                          Equations
                          Instances For

                            The mass unit of nominal solar masses (1.988416 × 10 ^ 30 kilograms). See: https://iopscience.iop.org/article/10.3847/0004-6256/152/2/41

                            Equations
                            Instances For

                              Relations between mass units #