Physlib.Relativity.LorentzGroup.ToVector

Imports

/-
Copyright (c) 2024 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.Tensors.RealTensor.Vector.MinkowskiProduct

Vectors from Lorentz group elements

Every element of the Lorentz group defines a Lorentz vector, but it's first column.

@[expose] public section

The Lorentz vector obtained by acting the Lorentz group element Λ on basis (Sum.inl 0).

def toVector {d : ℕ} (Λ : LorentzGroup d) : Lorentz.Vector d := Λ • basis (Sum.inl 0)

              

lemma toVector_mul {d : ℕ} (Λ₁ Λ₂ : LorentzGroup d) :
    toVector (Λ₁ * Λ₂) = Λ₁ • toVector Λ₂ := byd:ℕΛ₁:↑(𝓛 d)Λ₂:↑(𝓛 d)⊢ toVector (Λ₁ * Λ₂) = Λ₁ • toVector Λ₂
  rw [toVector,d:ℕΛ₁:↑(𝓛 d)Λ₂:↑(𝓛 d)⊢ (Λ₁ * Λ₂) • basis (Sum.inl 0) = Λ₁ • toVector Λ₂All goals completed! 🐙 toVector,d:ℕΛ₁:↑(𝓛 d)Λ₂:↑(𝓛 d)⊢ (Λ₁ * Λ₂) • basis (Sum.inl 0) = Λ₁ • Λ₂ • basis (Sum.inl 0)All goals completed! 🐙 smul_smuld:ℕΛ₁:↑(𝓛 d)Λ₂:↑(𝓛 d)⊢ (Λ₁ * Λ₂) • basis (Sum.inl 0) = (Λ₁ * Λ₂) • basis (Sum.inl 0)All goals completed! 🐙]All goals completed! 🐙lemma toVector_neg {d : ℕ} (Λ : LorentzGroup d) :
    toVector (-Λ) = -toVector Λ := byd:ℕΛ:↑(𝓛 d)⊢ toVector (-Λ) = -toVector Λ
  simp [toVector, neg_smul]All goals completed! 🐙@[simp]
lemma toVector_apply {d : ℕ} (Λ : LorentzGroup d)
    (i : Fin 1 ⊕ Fin d) : (toVector Λ) i = Λ.1 i (Sum.inl 0) := byd:ℕΛ:↑(𝓛 d)i:Fin 1 ⊕ Fin d⊢ toVector Λ i = ↑Λ i (Sum.inl 0)
  simp [toVector, smul_eq_sum]All goals completed! 🐙lemma toVector_eq_fun {d : ℕ} (Λ : LorentzGroup d) :
    toVector Λ = (fun i => Λ.1 i (Sum.inl 0)) := byd:ℕΛ:↑(𝓛 d)⊢ toVector Λ = fun i => ↑Λ i (Sum.inl 0)
  funext id:ℕΛ:↑(𝓛 d)i:Fin 1 ⊕ Fin d⊢ toVector Λ i = ↑Λ i (Sum.inl 0)
  simpAll goals completed! 🐙@[fun_prop]
lemma toVector_continuous {d : ℕ} : Continuous (toVector (d := d)) := byd:ℕ⊢ Continuous toVector
  change Continuous (fun Λ => toVector (d := d) Λ)d:ℕ⊢ Continuous fun Λ => toVector Λ
  conv =>d:ℕ| Continuous fun Λ => toVector Λ
    enter [1, Λ]d:ℕΛ:↑(𝓛 d)| toVector Λ
    rw [toVector_eq_fun]d:ℕΛ:↑(𝓛 d)| fun i => ↑Λ i (Sum.inl 0)
  refine Vector.continuous_of_apply _ ?_d:ℕ⊢ ∀ (i : Fin 1 ⊕ Fin d), Continuous fun x => ↑x i (Sum.inl 0)
  intro id:ℕi:Fin 1 ⊕ Fin d⊢ Continuous fun x => ↑x i (Sum.inl 0)
  refine Continuous.matrix_elem ?_ i (Sum.inl 0)d:ℕi:Fin 1 ⊕ Fin d⊢ Continuous Subtype.val
  fun_propAll goals completed! 🐙lemma toVector_timeComponent {d : ℕ} (Λ : LorentzGroup d) :
    (toVector Λ).timeComponent = Λ.1 (Sum.inl 0) (Sum.inl 0) := byd:ℕΛ:↑(𝓛 d)⊢ (toVector Λ).timeComponent = ↑Λ (Sum.inl 0) (Sum.inl 0)
  simpAll goals completed! 🐙@[simp]
lemma toVector_minkowskiProduct_self {d : ℕ} (Λ : LorentzGroup d) :
    ⟪toVector Λ, toVector Λ⟫ₘ = 1 := byd:ℕΛ:↑(𝓛 d)⊢ (minkowskiProduct (toVector Λ)) (toVector Λ) = 1
  simp [toVector, minkowskiMatrix.inl_0_inl_0]All goals completed! 🐙

lemma one_le_abs_timeComponent {d : ℕ} (Λ : LorentzGroup d) :
    1 ≤ |Λ.1 (Sum.inl 0) (Sum.inl 0)| := byd:ℕΛ:↑(𝓛 d)⊢ 1 ≤ |↑Λ (Sum.inl 0) (Sum.inl 0)|
  rw [← toVector_timeComponent Λ,d:ℕΛ:↑(𝓛 d)⊢ 1 ≤ |(toVector Λ).timeComponent|d:ℕΛ:↑(𝓛 d)⊢ (minkowskiProduct (toVector Λ)) (toVector Λ) ≤ (toVector Λ).timeComponent ^ 2 ← one_le_sq_iff_one_le_abs,d:ℕΛ:↑(𝓛 d)⊢ 1 ≤ (toVector Λ).timeComponent ^ 2d:ℕΛ:↑(𝓛 d)⊢ (minkowskiProduct (toVector Λ)) (toVector Λ) ≤ (toVector Λ).timeComponent ^ 2 ← toVector_minkowskiProduct_self Λd:ℕΛ:↑(𝓛 d)⊢ (minkowskiProduct (toVector Λ)) (toVector Λ) ≤ (toVector Λ).timeComponent ^ 2d:ℕΛ:↑(𝓛 d)⊢ (minkowskiProduct (toVector Λ)) (toVector Λ) ≤ (toVector Λ).timeComponent ^ 2]d:ℕΛ:↑(𝓛 d)⊢ (minkowskiProduct (toVector Λ)) (toVector Λ) ≤ (toVector Λ).timeComponent ^ 2
  exact minkowskiProduct_self_le_timeComponent_sq (toVector Λ)All goals completed! 🐙

lemma toVector_eq_basis_iff_timeComponent_eq_one {d : ℕ} (Λ : LorentzGroup d) :
    toVector Λ = basis (Sum.inl 0) ↔ Λ.1 (Sum.inl 0) (Sum.inl 0) = 1 := byd:ℕΛ:↑(𝓛 d)⊢ toVector Λ = basis (Sum.inl 0) ↔ ↑Λ (Sum.inl 0) (Sum.inl 0) = 1
  constructormpd:ℕΛ:↑(𝓛 d)⊢ toVector Λ = basis (Sum.inl 0) → ↑Λ (Sum.inl 0) (Sum.inl 0) = 1mprd:ℕΛ:↑(𝓛 d)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 → toVector Λ = basis (Sum.inl 0)
  ·mpd:ℕΛ:↑(𝓛 d)⊢ toVector Λ = basis (Sum.inl 0) → ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 intro hmpd:ℕΛ:↑(𝓛 d)h:toVector Λ = basis (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) = 1
    rw [← toVector_timeComponent Λ,mpd:ℕΛ:↑(𝓛 d)h:toVector Λ = basis (Sum.inl 0)⊢ (toVector Λ).timeComponent = 1mpd:ℕΛ:↑(𝓛 d)h:toVector Λ = basis (Sum.inl 0)⊢ (basis (Sum.inl 0)).timeComponent = 1 hmpd:ℕΛ:↑(𝓛 d)h:toVector Λ = basis (Sum.inl 0)⊢ (basis (Sum.inl 0)).timeComponent = 1mpd:ℕΛ:↑(𝓛 d)h:toVector Λ = basis (Sum.inl 0)⊢ (basis (Sum.inl 0)).timeComponent = 1]mpd:ℕΛ:↑(𝓛 d)h:toVector Λ = basis (Sum.inl 0)⊢ (basis (Sum.inl 0)).timeComponent = 1
    simpAll goals completed! 🐙
  ·mprd:ℕΛ:↑(𝓛 d)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 → toVector Λ = basis (Sum.inl 0) intro hmprd:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1⊢ toVector Λ = basis (Sum.inl 0)
    funext imprd:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin d⊢ toVector Λ i = basis (Sum.inl 0) i
    have h1 := toVector_minkowskiProduct_self Λmprd:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(minkowskiProduct (toVector Λ)) (toVector Λ) = 1⊢ toVector Λ i = basis (Sum.inl 0) i
    rw [minkowskiProduct_self_eq_timeComponent_spatialPartmprd:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:‖(toVector Λ).timeComponent‖ ^ 2 - ‖(toVector Λ).spatialPart‖ ^ 2 = 1⊢ toVector Λ i = basis (Sum.inl 0) imprd:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:‖(toVector Λ).timeComponent‖ ^ 2 - ‖(toVector Λ).spatialPart‖ ^ 2 = 1⊢ toVector Λ i = basis (Sum.inl 0) i] at h1mprd:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:‖(toVector Λ).timeComponent‖ ^ 2 - ‖(toVector Λ).spatialPart‖ ^ 2 = 1⊢ toVector Λ i = basis (Sum.inl 0) i
    simp [h] at h1mprd:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0⊢ toVector Λ i = basis (Sum.inl 0) i
    simp [toVector, smul_eq_sum]mprd:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0⊢ ↑Λ i (Sum.inl 0) = if Sum.inl 0 = i then 1 else 0
    match i with
    | Sum.inl 0 =>d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) = if Sum.inl 0 = Sum.inl 0 then 1 else 0 simp [h]All goals completed! 🐙
    | Sum.inr j =>d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0j:Fin d⊢ ↑Λ (Sum.inr j) (Sum.inl 0) = if Sum.inl 0 = Sum.inr j then 1 else 0
      simp only [Fin.isValue, reduceCtorEq, ↓reduceIte]d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0j:Fin d⊢ ↑Λ (Sum.inr j) (Sum.inl 0) = 0
      trans (toVector Λ).spatialPart jd:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0j:Fin d⊢ ↑Λ (Sum.inr j) (Sum.inl 0) = (toVector Λ).spatialPart.ofLp jd:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0j:Fin d⊢ (toVector Λ).spatialPart.ofLp j = 0
      ·d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0j:Fin d⊢ ↑Λ (Sum.inr j) (Sum.inl 0) = (toVector Λ).spatialPart.ofLp j simpAll goals completed! 🐙
      simp only [toVector_apply, Fin.isValue]d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0j:Fin d⊢ ↑Λ (Sum.inr j) (Sum.inl 0) = 0
      change (fun i => Λ.1 (Sum.inr i) (Sum.inl 0)) j = _d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0j:Fin d⊢ (fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) j = 0
      rw [h1d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0j:Fin d⊢ 0 j = 0d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0j:Fin d⊢ 0 j = 0]d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) = 1i:Fin 1 ⊕ Fin dh1:(fun i => ↑Λ (Sum.inr i) (Sum.inl 0)) = 0j:Fin d⊢ 0 j = 0
      simpAll goals completed! 🐙

lemma smul_timeComponent_eq_toVector_minkowskiProduct {d : ℕ} (Λ : LorentzGroup d)
    (v : Lorentz.Vector d) :
    (Λ • v).timeComponent = ⟪toVector Λ⁻¹, v⟫ₘ := byd:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ (Λ • v).timeComponent = (minkowskiProduct (toVector Λ⁻¹)) v
  simp [timeComponent]d:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ (Λ • v) (Sum.inl 0) = (minkowskiProduct (toVector Λ⁻¹)) v
  rw [smul_eq_sumd:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ∑ j, ↑Λ (Sum.inl 0) j * v j = (minkowskiProduct (toVector Λ⁻¹)) vd:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ∑ j, ↑Λ (Sum.inl 0) j * v j = (minkowskiProduct (toVector Λ⁻¹)) v]d:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ∑ j, ↑Λ (Sum.inl 0) j * v j = (minkowskiProduct (toVector Λ⁻¹)) v
  simp only [Fin.isValue, Fintype.sum_sum_type,
    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]d:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) * v (Sum.inl 0) + ∑ a₂, ↑Λ (Sum.inl 0) (Sum.inr a₂) * v (Sum.inr a₂) =
  (minkowskiProduct (toVector Λ⁻¹)) v
  rw [minkowskiProduct_eq_timeComponent_spatialPartd:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) * v (Sum.inl 0) + ∑ a₂, ↑Λ (Sum.inl 0) (Sum.inr a₂) * v (Sum.inr a₂) =
  (toVector Λ⁻¹).timeComponent * v.timeComponent - inner ℝ (toVector Λ⁻¹).spatialPart v.spatialPartd:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) * v (Sum.inl 0) + ∑ a₂, ↑Λ (Sum.inl 0) (Sum.inr a₂) * v (Sum.inr a₂) =
  (toVector Λ⁻¹).timeComponent * v.timeComponent - inner ℝ (toVector Λ⁻¹).spatialPart v.spatialPart]d:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) * v (Sum.inl 0) + ∑ a₂, ↑Λ (Sum.inl 0) (Sum.inr a₂) * v (Sum.inr a₂) =
  (toVector Λ⁻¹).timeComponent * v.timeComponent - inner ℝ (toVector Λ⁻¹).spatialPart v.spatialPart
  congre_a.e_ad:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) = (toVector Λ⁻¹).timeComponente_ad:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ∑ a₂, ↑Λ (Sum.inl 0) (Sum.inr a₂) * v (Sum.inr a₂) = -inner ℝ (toVector Λ⁻¹).spatialPart v.spatialPart
  ·e_a.e_ad:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) = (toVector Λ⁻¹).timeComponent simp [inv_eq_dual, minkowskiMatrix.dual_apply, minkowskiMatrix.inl_0_inl_0]All goals completed! 🐙
  ·e_ad:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ∑ a₂, ↑Λ (Sum.inl 0) (Sum.inr a₂) * v (Sum.inr a₂) = -inner ℝ (toVector Λ⁻¹).spatialPart v.spatialPart simp only [Fin.isValue, inv_eq_dual, PiLp.inner_apply, toVector_apply, RCLike.inner_apply,
      conj_trivial]e_ad:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ∑ a₂, ↑Λ (Sum.inl 0) (Sum.inr a₂) * v (Sum.inr a₂) =
  -∑ x, v (Sum.inr x) * minkowskiMatrix.dual (↑Λ) (Sum.inr x) (Sum.inl 0)
    rw [← Finset.sum_neg_distribe_ad:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ∑ a₂, ↑Λ (Sum.inl 0) (Sum.inr a₂) * v (Sum.inr a₂) =
  ∑ x, -(v (Sum.inr x) * minkowskiMatrix.dual (↑Λ) (Sum.inr x) (Sum.inl 0))e_ad:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ∑ a₂, ↑Λ (Sum.inl 0) (Sum.inr a₂) * v (Sum.inr a₂) =
  ∑ x, -(v (Sum.inr x) * minkowskiMatrix.dual (↑Λ) (Sum.inr x) (Sum.inl 0))]e_ad:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ ∑ a₂, ↑Λ (Sum.inl 0) (Sum.inr a₂) * v (Sum.inr a₂) =
  ∑ x, -(v (Sum.inr x) * minkowskiMatrix.dual (↑Λ) (Sum.inr x) (Sum.inl 0))
    congre_a.e_fd:ℕΛ:↑(𝓛 d)v:Lorentz.Vector d⊢ (fun a₂ => ↑Λ (Sum.inl 0) (Sum.inr a₂) * v (Sum.inr a₂)) = fun x =>
  -(v (Sum.inr x) * minkowskiMatrix.dual (↑Λ) (Sum.inr x) (Sum.inl 0))
    funext ie_a.e_fd:ℕΛ:↑(𝓛 d)v:Lorentz.Vector di:Fin d⊢ ↑Λ (Sum.inl 0) (Sum.inr i) * v (Sum.inr i) = -(v (Sum.inr i) * minkowskiMatrix.dual (↑Λ) (Sum.inr i) (Sum.inl 0))
    rw [minkowskiMatrix.dual_applye_a.e_fd:ℕΛ:↑(𝓛 d)v:Lorentz.Vector di:Fin d⊢ ↑Λ (Sum.inl 0) (Sum.inr i) * v (Sum.inr i) =
  -(v (Sum.inr i) *
      (minkowskiMatrix (Sum.inr i) (Sum.inr i) * ↑Λ (Sum.inl 0) (Sum.inr i) * minkowskiMatrix (Sum.inl 0) (Sum.inl 0)))e_a.e_fd:ℕΛ:↑(𝓛 d)v:Lorentz.Vector di:Fin d⊢ ↑Λ (Sum.inl 0) (Sum.inr i) * v (Sum.inr i) =
  -(v (Sum.inr i) *
      (minkowskiMatrix (Sum.inr i) (Sum.inr i) * ↑Λ (Sum.inl 0) (Sum.inr i) * minkowskiMatrix (Sum.inl 0) (Sum.inl 0)))]e_a.e_fd:ℕΛ:↑(𝓛 d)v:Lorentz.Vector di:Fin d⊢ ↑Λ (Sum.inl 0) (Sum.inr i) * v (Sum.inr i) =
  -(v (Sum.inr i) *
      (minkowskiMatrix (Sum.inr i) (Sum.inr i) * ↑Λ (Sum.inl 0) (Sum.inr i) * minkowskiMatrix (Sum.inl 0) (Sum.inl 0)))
    simp [minkowskiMatrix.inl_0_inl_0, minkowskiMatrix.inr_i_inr_i]e_a.e_fd:ℕΛ:↑(𝓛 d)v:Lorentz.Vector di:Fin d⊢ ↑Λ (Sum.inl 0) (Sum.inr i) * v (Sum.inr i) = v (Sum.inr i) * ↑Λ (Sum.inl 0) (Sum.inr i)
    ringAll goals completed! 🐙