Boosts in the Lorentz group

def LorentzGroup.γ (β : ℝ) : ℝ

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

Equations

• LorentzGroup.γ β = 1 / √(1 - β ^ 2)

theorem LorentzGroup.γ_sq (β : ℝ) (hβ : |β| < 1) : γ β ^ 2 = 1 / (1 - β ^ 2)

@[simp]

theorem LorentzGroup.γ_zero : γ 0 = 1

@[simp]

theorem LorentzGroup.γ_neg (β : ℝ) : γ (-β) = γ β

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

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

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

@[simp]

theorem LorentzGroup.boost_transpose_eq_self {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) : transpose (boost i β hβ) = boost i β hβ

@[simp]

theorem LorentzGroup.boost_transpose_matrix_eq_self {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) : (↑(boost i β hβ)).transpose = ↑(boost i β hβ)

@[simp]

theorem LorentzGroup.boost_zero_eq_id {d : ℕ} (i : Fin d) : boost i 0 ⋯ = 1

theorem LorentzGroup.boost_inverse {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) : (boost i β hβ)⁻¹ = boost i (-β) ⋯

@[simp]

theorem LorentzGroup.boost_inl_0_inl_0 {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) : ↑(boost i β hβ) (Sum.inl 0) (Sum.inl 0) = γ β

@[simp]

theorem LorentzGroup.boost_inr_self_inr_self {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) : ↑(boost i β hβ) (Sum.inr i) (Sum.inr i) = γ β

@[simp]

theorem LorentzGroup.boost_inl_0_inr_self {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) : ↑(boost i β hβ) (Sum.inl 0) (Sum.inr i) = -γ β * β

@[simp]

theorem LorentzGroup.boost_inr_self_inl_0 {d : ℕ} (i : Fin d) {β : ℝ} (hβ : |β| < 1) : ↑(boost i β hβ) (Sum.inr i) (Sum.inl 0) = -γ β * β

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

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

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

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

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

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