PhysLean Documentation

PhysLean.Relativity.Tensors.RealTensor.Velocity.Basic

Lorentz Velocities #

In this module we define Lorentz velocities to be Lorentz vectors which have norm equal to one and which are future-directed.

source
def Lorentz.Velocity (d : ℕ := 3) :
Set (Vector d)

A Lorentz Velocity is a Lorentz vector which has norm equal to one and which is future-directed.

Equations
Instances For
    source
    instance Lorentz.Velocity.instTopologicalSpaceElemVector {d : ℕ} :
    TopologicalSpace ↑(Velocity d)

    The instance of a topological space on Velocity d defined as the subspace topology.

    Equations
    source
    theorem Lorentz.Velocity.ext {d : ℕ} {v w : ↑(Velocity d)} (h : ↑v = ↑w) :
    v = w
    source
    theorem Lorentz.Velocity.ext_iff {d : ℕ} {v w : ↑(Velocity d)} :
    v = w ↔ ↑v = ↑w
    source
    theorem Lorentz.Velocity.mem_iff {d : ℕ} {v : Vector d} :
    v ∈ Velocity d ↔ (Vector.minkowskiProduct v) v = 1 ∧ 0 < v.timeComponent
    source
    @[simp]
    theorem Lorentz.Velocity.minkowskiProduct_self_eq_one {d : ℕ} (v : ↑(Velocity d)) :
    (Vector.minkowskiProduct ↑v) ↑v = 1
    source
    @[simp]
    theorem Lorentz.Velocity.timeComponent_pos {d : ℕ} (v : ↑(Velocity d)) :
    0 < (↑v).timeComponent
    source
    @[simp]
    theorem Lorentz.Velocity.timeComponent_nonneg {d : ℕ} (v : ↑(Velocity d)) :
    0 ≤ (↑v).timeComponent
    source
    @[simp]
    theorem Lorentz.Velocity.timeComponent_abs {d : ℕ} (v : ↑(Velocity d)) :
    |(↑v).timeComponent| = (↑v).timeComponent
    source
    theorem Lorentz.Velocity.norm_spatialPart_le_timeComponent {d : ℕ} (v : ↑(Velocity d)) :
    ‖(↑v).spatialPart‖ ≤ ‖(↑v).timeComponent‖
    source
    theorem Lorentz.Velocity.norm_spatialPart_sq_eq {d : ℕ} (v : ↑(Velocity d)) :
    ‖(↑v).spatialPart‖ ^ 2 = Vector.toCoord (↑v) (Sum.inl 0) ^ 2 - 1
    source
    theorem Lorentz.Velocity.zero_le_minkowskiProduct {d : ℕ} (u v : ↑(Velocity d)) :
    0 ≤ (Vector.minkowskiProduct ↑u) ↑v
    source
    theorem Lorentz.Velocity.one_add_minkowskiProduct_neq_zero {d : ℕ} (u v : ↑(Velocity d)) :
    1 + (Vector.minkowskiProduct ↑u) ↑v ≠ 0
    source
    theorem Lorentz.Velocity.minkowskiProduct_continuous_snd {d : ℕ} (u : Vector d) :
    Continuous fun (x : ↑(Velocity d)) => (Vector.minkowskiProduct u) ↑x
    source
    theorem Lorentz.Velocity.minkowskiProduct_continuous_fst {d : ℕ} (u : Vector d) :
    Continuous fun (x : ↑(Velocity d)) => (Vector.minkowskiProduct ↑x) u

    Zero #

    source
    noncomputable def Lorentz.Velocity.zero {d : ℕ} :
    ↑(Velocity d)

    The Velcoity d which has all space components zero.

    Equations
    Instances For
      source
      noncomputable instance Lorentz.Velocity.instZeroElemVector {d : ℕ} :
      Zero ↑(Velocity d)
      Equations
      source
      noncomputable def Lorentz.Velocity.pathFromZero {d : ℕ} (u : ↑(Velocity d)) :
      Path zero u

      A continuous path from a velocity u to the zero velocity.

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

        Topology #

        source
        theorem Lorentz.Velocity.isPathConnected {d : ℕ} :
        IsPathConnected Set.univ