Physlib.Relativity.LorentzGroup.Boosts.Apply

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.Relativity.LorentzGroup.Boosts.Basic
public import Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial

Boosts applied to Lorentz vectors

These recover what one would describe as the ordinary Lorentz transformations of Lorentz vectors.

              @[expose] public section

lemma boost_time_eq (i : Fin d) (β : ℝ) (hβ : |β| < 1) (p : Vector d) :
    (boost i β hβ • p) (Sum.inl 0) = γ β * (p (Sum.inl 0) - β * p (Sum.inr i)) := byd:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ (boost i β hβ • p) (Sum.inl 0) = γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
  rw [smul_eq_sum,d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ j, ↑(boost i β hβ) (Sum.inl 0) j * p j = γ β * (p (Sum.inl 0) - β * p (Sum.inr i))d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inl 0) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inl 0) (Sum.inr i) * p (Sum.inr i) =
  γ β * (p (Sum.inl 0) - β * p (Sum.inr i)) Fintype.sum_sum_type,d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inl 0) (Sum.inl a₁) * p (Sum.inl a₁) +
    ∑ a₂, ↑(boost i β hβ) (Sum.inl 0) (Sum.inr a₂) * p (Sum.inr a₂) =
  γ β * (p (Sum.inl 0) - β * p (Sum.inr i))d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inl 0) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inl 0) (Sum.inr i) * p (Sum.inr i) =
  γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
    Fintype.sum_eq_single i fun b hb => byd:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector db:Fin dhb:b ≠ i⊢ ↑(boost i β hβ) (Sum.inl 0) (Sum.inr b) * p (Sum.inr b) = 0d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inl 0) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inl 0) (Sum.inr i) * p (Sum.inr i) =
  γ β * (p (Sum.inl 0) - β * p (Sum.inr i)) simp [boost_inl_0_inr_other hβ hb]All goals completed! 🐙d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inl 0) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inl 0) (Sum.inr i) * p (Sum.inr i) =
  γ β * (p (Sum.inl 0) - β * p (Sum.inr i))]d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inl 0) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inl 0) (Sum.inr i) * p (Sum.inr i) =
  γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
  simp only [Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton,
    boost_inl_0_inl_0, boost_inl_0_inr_self, neg_mul]d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ γ β * p (Sum.inl 0) + -(γ β * β * p (Sum.inr i)) = γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
  ringAll goals completed! 🐙

lemma boost_inr_self_eq (i : Fin d) (β : ℝ) (hβ : |β| < 1) (p : Vector d) :
    (boost i β hβ • p) (Sum.inr i) = γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) := byd:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ (boost i β hβ • p) (Sum.inr i) = γ β * (p (Sum.inr i) - β * p (Sum.inl 0))
  rw [smul_eq_sum,d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ j, ↑(boost i β hβ) (Sum.inr i) j * p j = γ β * (p (Sum.inr i) - β * p (Sum.inl 0))d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inr i) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inr i) (Sum.inr i) * p (Sum.inr i) =
  γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) Fintype.sum_sum_type,d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inr i) (Sum.inl a₁) * p (Sum.inl a₁) +
    ∑ a₂, ↑(boost i β hβ) (Sum.inr i) (Sum.inr a₂) * p (Sum.inr a₂) =
  γ β * (p (Sum.inr i) - β * p (Sum.inl 0))d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inr i) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inr i) (Sum.inr i) * p (Sum.inr i) =
  γ β * (p (Sum.inr i) - β * p (Sum.inl 0))
    Fintype.sum_eq_single i fun b hb => byd:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector db:Fin dhb:b ≠ i⊢ ↑(boost i β hβ) (Sum.inr i) (Sum.inr b) * p (Sum.inr b) = 0d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inr i) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inr i) (Sum.inr i) * p (Sum.inr i) =
  γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) simp [boost_inr_self_inr_other hβ hb]All goals completed! 🐙d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inr i) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inr i) (Sum.inr i) * p (Sum.inr i) =
  γ β * (p (Sum.inr i) - β * p (Sum.inl 0))]d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inr i) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inr i) (Sum.inr i) * p (Sum.inr i) =
  γ β * (p (Sum.inr i) - β * p (Sum.inl 0))
  simp only [Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton,
    boost_inr_self_inl_0, neg_mul, boost_inr_self_inr_self]d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ -(γ β * β * p (Sum.inl 0)) + γ β * p (Sum.inr i) = γ β * (p (Sum.inr i) - β * p (Sum.inl 0))
  ringAll goals completed! 🐙

lemma boost_inr_other_eq (i j : Fin d) (hji : j ≠ i) (β : ℝ) (hβ : |β| < 1) (p : Vector d) :
    (boost i β hβ • p) (Sum.inr j) = p (Sum.inr j) := byd:ℕi:Fin dj:Fin dhji:j ≠ iβ:ℝhβ:|β| < 1p:Vector d⊢ (boost i β hβ • p) (Sum.inr j) = p (Sum.inr j)
  rw [smul_eq_sum,d:ℕi:Fin dj:Fin dhji:j ≠ iβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ j_1, ↑(boost i β hβ) (Sum.inr j) j_1 * p j_1 = p (Sum.inr j)d:ℕi:Fin dj:Fin dhji:j ≠ iβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inr j) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inr j) (Sum.inr j) * p (Sum.inr j) =
  p (Sum.inr j) Fintype.sum_sum_type,d:ℕi:Fin dj:Fin dhji:j ≠ iβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inr j) (Sum.inl a₁) * p (Sum.inl a₁) +
    ∑ a₂, ↑(boost i β hβ) (Sum.inr j) (Sum.inr a₂) * p (Sum.inr a₂) =
  p (Sum.inr j)d:ℕi:Fin dj:Fin dhji:j ≠ iβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inr j) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inr j) (Sum.inr j) * p (Sum.inr j) =
  p (Sum.inr j)
    Fintype.sum_eq_single j fun b hb => byd:ℕi:Fin dj:Fin dhji:j ≠ iβ:ℝhβ:|β| < 1p:Vector db:Fin dhb:b ≠ j⊢ ↑(boost i β hβ) (Sum.inr j) (Sum.inr b) * p (Sum.inr b) = 0d:ℕi:Fin dj:Fin dhji:j ≠ iβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inr j) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inr j) (Sum.inr j) * p (Sum.inr j) =
  p (Sum.inr j) simp [boost_inr_other_inr hβ hji, Ne.symm hb]All goals completed! 🐙d:ℕi:Fin dj:Fin dhji:j ≠ iβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inr j) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inr j) (Sum.inr j) * p (Sum.inr j) =
  p (Sum.inr j)]d:ℕi:Fin dj:Fin dhji:j ≠ iβ:ℝhβ:|β| < 1p:Vector d⊢ ∑ a₁, ↑(boost i β hβ) (Sum.inr j) (Sum.inl a₁) * p (Sum.inl a₁) +
    ↑(boost i β hβ) (Sum.inr j) (Sum.inr j) * p (Sum.inr j) =
  p (Sum.inr j)
  simp [boost_inr_other_inl_0 hβ hji, boost_inr_other_inr hβ hji]All goals completed! 🐙

lemma boost_toCoord_eq (i : Fin d) (β : ℝ) (hβ : |β| < 1) (p : Vector d) :
    (boost i β hβ • p) = fun j =>
      match j with
      | Sum.inl 0 => γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
      | Sum.inr j =>
        if j = i then γ β * (p (Sum.inr i) - β * p (Sum.inl 0))
        else p (Sum.inr j) := byd:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector d⊢ boost i β hβ • p = fun j =>
  match j with
  | Sum.inl 0 => γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
  | Sum.inr j => if j = i then γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) else p (Sum.inr j)
  funext jd:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector dj:Fin 1 ⊕ Fin d⊢ (boost i β hβ • p) j =
  match j with
  | Sum.inl 0 => γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
  | Sum.inr j => if j = i then γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) else p (Sum.inr j)
  match j with
  | Sum.inl 0 =>d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector dj:Fin 1 ⊕ Fin d⊢ (boost i β hβ • p) (Sum.inl 0) =
  match Sum.inl 0 with
  | Sum.inl 0 => γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
  | Sum.inr j => if j = i then γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) else p (Sum.inr j) rw [boost_time_eqd:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector dj:Fin 1 ⊕ Fin d⊢ γ β * (p (Sum.inl 0) - β * p (Sum.inr i)) =
  match Sum.inl 0 with
  | Sum.inl 0 => γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
  | Sum.inr j => if j = i then γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) else p (Sum.inr j)All goals completed! 🐙]All goals completed! 🐙
  | Sum.inr j =>d:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector dj✝:Fin 1 ⊕ Fin dj:Fin d⊢ (boost i β hβ • p) (Sum.inr j) =
  match Sum.inr j with
  | Sum.inl 0 => γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
  | Sum.inr j => if j = i then γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) else p (Sum.inr j)
    by_cases hj : j = iposd:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector dj✝:Fin 1 ⊕ Fin dj:Fin dhj:j = i⊢ (boost i β hβ • p) (Sum.inr j) =
  match Sum.inr j with
  | Sum.inl 0 => γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
  | Sum.inr j => if j = i then γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) else p (Sum.inr j)negd:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector dj✝:Fin 1 ⊕ Fin dj:Fin dhj:¬j = i⊢ (boost i β hβ • p) (Sum.inr j) =
  match Sum.inr j with
  | Sum.inl 0 => γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
  | Sum.inr j => if j = i then γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) else p (Sum.inr j)
    ·posd:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector dj✝:Fin 1 ⊕ Fin dj:Fin dhj:j = i⊢ (boost i β hβ • p) (Sum.inr j) =
  match Sum.inr j with
  | Sum.inl 0 => γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
  | Sum.inr j => if j = i then γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) else p (Sum.inr j) simp [hj, boost_inr_self_eq]All goals completed! 🐙
    ·negd:ℕi:Fin dβ:ℝhβ:|β| < 1p:Vector dj✝:Fin 1 ⊕ Fin dj:Fin dhj:¬j = i⊢ (boost i β hβ • p) (Sum.inr j) =
  match Sum.inr j with
  | Sum.inl 0 => γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
  | Sum.inr j => if j = i then γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) else p (Sum.inr j) simp [hj, boost_inr_other_eq _ _ hj]All goals completed! 🐙