Documentation

PhysLean.Relativity.LorentzGroup.Boosts.Basic

Boosts in the Lorentz group #

source
def LorentzGroup.γ (β : ℝ) :
ℝ

The Lorentz factor (aka gamma factor or Lorentz term).

Equations
    Instances For
      source
      theorem LorentzGroup.γ_sq (β : ℝ) (hβ : |β| < 1) :
      γ β ^ 2 = 1 / (1 - β ^ 2)
      source
      @[simp]
      theorem LorentzGroup.γ_zero :
      γ 0 = 1
      source
      @[simp]
      theorem LorentzGroup.γ_neg (β : ℝ) :
      γ (-β) = γ β
      source
      @[simp]
      theorem LorentzGroup.γ_det_not_zero (β : ℝ) (hβ : |β| < 1) :
      1 - β ^ 2 ≠ 0
      source
      def LorentzGroup.boost {d : ℕ} (i : Fin d) (β : ℝ) (hβ : |β| < 1) :
      ↑(LorentzGroup d)

      The Lorentz boost with in the space direction i with speed β with |β| < 1.

      Equations
        Instances For
          source
          theorem LorentzGroup.boost.h {d : ℕ} (i : Fin d) (β : ℝ) (hβ : |β| < 1) :
          (fun (j k : Fin 1 ⊕ Fin d) => if k = Sum.inl 0 ∧ j = Sum.inl 0 then γ β else if k = Sum.inl 0 ∧ j = Sum.inr i then -γ β * β else if k = Sum.inr i ∧ j = Sum.inl 0 then -γ β * β else if k = Sum.inr i ∧ j = Sum.inr i then γ β else if j = k then 1 else 0) ∈ LorentzGroup d
          source
          @[simp]
          theorem LorentzGroup.boost_transpose_eq_self {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
          transpose (boost i β hβ) = boost i β hβ
          source
          @[simp]
          theorem LorentzGroup.boost_transpose_matrix_eq_self {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
          (↑(boost i β hβ)).transpose = ↑(boost i β hβ)
          source
          @[simp]
          theorem LorentzGroup.boost_zero_eq_id {d : ℕ} (i : Fin d) :
          boost i 0 ⋯ = 1
          source
          theorem LorentzGroup.boost_inverse {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
          (boost i β hβ)⁻¹ = boost i (-β) ⋯
          source
          @[simp]
          theorem LorentzGroup.boost_inl_0_inl_0 {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
          ↑(boost i β hβ) (Sum.inl 0) (Sum.inl 0) = γ β
          source
          @[simp]
          theorem LorentzGroup.boost_inr_self_inr_self {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
          ↑(boost i β hβ) (Sum.inr i) (Sum.inr i) = γ β
          source
          @[simp]
          theorem LorentzGroup.boost_inl_0_inr_self {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
          ↑(boost i β hβ) (Sum.inl 0) (Sum.inr i) = -γ β * β
          source
          @[simp]
          theorem LorentzGroup.boost_inr_self_inl_0 {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
          ↑(boost i β hβ) (Sum.inr i) (Sum.inl 0) = -γ β * β
          source
          theorem LorentzGroup.boost_inl_0_inr_other {d : ℕ} {i j : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) :
          ↑(boost i β hβ) (Sum.inl 0) (Sum.inr j) = 0
          source
          theorem LorentzGroup.boost_inr_other_inl_0 {d : ℕ} {i j : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) :
          ↑(boost i β hβ) (Sum.inr j) (Sum.inl 0) = 0
          source
          theorem LorentzGroup.boost_inr_self_inr_other {d : ℕ} {i j : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) :
          ↑(boost i β hβ) (Sum.inr i) (Sum.inr j) = 0
          source
          theorem LorentzGroup.boost_inr_other_inr_self {d : ℕ} {i j : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) :
          ↑(boost i β hβ) (Sum.inr j) (Sum.inr i) = 0
          source
          theorem LorentzGroup.boost_inr_other_inr {d : ℕ} {i j k : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) :
          ↑(boost i β hβ) (Sum.inr j) (Sum.inr k) = if j = k then 1 else 0
          source
          theorem LorentzGroup.boost_inr_inr_other {d : ℕ} {i j k : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) :
          ↑(boost i β hβ) (Sum.inr k) (Sum.inr j) = if j = k then 1 else 0

          Properties of boosts in the zero-direction #

          source
          @[simp]
          theorem LorentzGroup.boost_zero_inl_0_inr_succ {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : Fin d) :
          ↑(boost 0 β hβ) (Sum.inl 0) (Sum.inr i.succ) = 0
          source
          @[simp]
          theorem LorentzGroup.boost_zero_inr_succ_inl_0 {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : Fin d) :
          ↑(boost 0 β hβ) (Sum.inr i.succ) (Sum.inl 0) = 0
          source
          @[simp]
          theorem LorentzGroup.boost_zero_inl_0_inr_nat_succ {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : ℕ) (h : i + 1 < d + 1) :
          ↑(boost 0 β hβ) (Sum.inl 0) (Sum.inr ⟨i + 1, h⟩) = 0
          source
          @[simp]
          theorem LorentzGroup.boost_zero_inr_nat_succ_inl_0 {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : ℕ) (h : i + 1 < d + 1) :
          ↑(boost 0 β hβ) (Sum.inr ⟨i + 1, h⟩) (Sum.inl 0) = 0
          source
          @[simp]
          theorem LorentzGroup.boost_zero_inr_0_inr_succ {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : Fin d) :
          ↑(boost 0 β hβ) (Sum.inr 0) (Sum.inr i.succ) = 0
          source
          @[simp]
          theorem LorentzGroup.boost_zero_inr_succ_inr_0 {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : Fin d) :
          ↑(boost 0 β hβ) (Sum.inr i.succ) (Sum.inr 0) = 0
          source
          @[simp]
          theorem LorentzGroup.boost_zero_inr_0_inr_nat_succ {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : ℕ) (h : i + 1 < d + 1) :
          ↑(boost 0 β hβ) (Sum.inr 0) (Sum.inr ⟨i + 1, h⟩) = 0
          source
          @[simp]
          theorem LorentzGroup.boost_zero_inr_nat_succ_inr_0 {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i : ℕ) (h : i + 1 < d + 1) :
          ↑(boost 0 β hβ) (Sum.inr ⟨i + 1, h⟩) (Sum.inr 0) = 0
          source
          theorem LorentzGroup.boost_zero_inr_succ_inr_succ {d : ℕ} {β : ℝ} (hβ : |β| < 1) (i1 i2 : Fin d) :
          ↑(boost 0 β hβ) (Sum.inr i1.succ) (Sum.inr i2.succ) = if i1 = i2 then 1 else 0