Lorentz vectors with norm one

def Lorentz.Contr.NormOne (d : ℕ) : Set ↑(Contr d).V

The set of Lorentz vectors with norm 1.

Equations

• Lorentz.Contr.NormOne d v = (Lorentz.contrContrContractField (v ⊗ₜ[ℝ] v) = 1)

theorem Lorentz.Contr.NormOne.mem_iff {d : ℕ} {v : ↑(Contr d).V} : v ∈ NormOne d ↔ contrContrContractField (v ⊗ₜ[ℝ] v) = 1

@[simp]

theorem Lorentz.Contr.NormOne.contr_self {d : ℕ} (v : ↑(NormOne d)) : contrContrContractField (↑v ⊗ₜ[ℝ] ↑v) = 1

theorem Lorentz.Contr.NormOne.mem_mulAction {d : ℕ} (g : ↑(LorentzGroup d)) (v : ↑(Contr d).V) : v ∈ NormOne d ↔ ((Contr d).ρ g) v ∈ NormOne d

instance Lorentz.Contr.NormOne.instTopologicalSpaceElemCarrierRealVModuleCatMatrixSumFinOfNatNatLorentzGroup {d : ℕ} : TopologicalSpace ↑(NormOne d)

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

Equations

• Lorentz.Contr.NormOne.instTopologicalSpaceElemCarrierRealVModuleCatMatrixSumFinOfNatNatLorentzGroup = instTopologicalSpaceSubtype

def Lorentz.Contr.NormOne.neg {d : ℕ} (v : ↑(NormOne d)) : ↑(NormOne d)

The negative of a NormOne as a NormOne.

Equations

• Lorentz.Contr.NormOne.neg v = ⟨-↑v, ⋯⟩

def LorentzGroup.toNormOne {d : ℕ} (Λ : ↑(LorentzGroup d)) : ↑(Lorentz.Contr.NormOne d)

The first column of a Lorentz matrix as a NormOneLorentzVector.

Equations

• LorentzGroup.toNormOne Λ = ⟨((Lorentz.Contr d).ρ Λ) (Lorentz.ContrMod.stdBasis (Sum.inl 0)), ⋯⟩

@[simp]

theorem LorentzGroup.toNormOne_coe_val {d : ℕ} (Λ : ↑(LorentzGroup d)) (a✝ : Fin 1 ⊕ Fin d) : (↑(toNormOne Λ)).val a✝ = (↑Λ).mulVec (⇑(Finsupp.single (Sum.inl 0) 1)) a✝

theorem LorentzGroup.toNormOne_inl {d : ℕ} (Λ : ↑(LorentzGroup d)) : (↑(toNormOne Λ)).val (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)

theorem LorentzGroup.toNormOne_inr {d : ℕ} (Λ : ↑(LorentzGroup d)) (i : Fin d) : (↑(toNormOne Λ)).val (Sum.inr i) = ↑Λ (Sum.inr i) (Sum.inl 0)

theorem LorentzGroup.inl_inl_mul {d : ℕ} (Λ Λ' : ↑(LorentzGroup d)) : ↑(Λ * Λ') (Sum.inl 0) (Sum.inl 0) = Lorentz.contrContrContractField (↑(toNormOne (transpose Λ)) ⊗ₜ[ℝ] ((Lorentz.Contr d).ρ parity) ↑(toNormOne Λ'))

theorem Lorentz.Contr.NormOne.inl_sq {d : ℕ} (v : ↑(NormOne d)) : (↑v).val (Sum.inl 0) ^ 2 = 1 + ‖ContrMod.toSpace ↑v‖ ^ 2

theorem Lorentz.Contr.NormOne.one_le_abs_inl {d : ℕ} (v : ↑(NormOne d)) : 1 ≤ |(↑v).val (Sum.inl 0)|

theorem Lorentz.Contr.NormOne.inl_le_neg_one_or_one_le_inl {d : ℕ} (v : ↑(NormOne d)) : (↑v).val (Sum.inl 0) ≤ -1 ∨ 1 ≤ (↑v).val (Sum.inl 0)

theorem Lorentz.Contr.NormOne.norm_space_le_abs_inl {d : ℕ} (v : ↑(NormOne d)) : ‖ContrMod.toSpace ↑v‖ < |(↑v).val (Sum.inl 0)|

theorem Lorentz.Contr.NormOne.norm_space_leq_abs_inl {d : ℕ} (v : ↑(NormOne d)) : ‖ContrMod.toSpace ↑v‖ ≤ |(↑v).val (Sum.inl 0)|

theorem Lorentz.Contr.NormOne.inl_abs_sub_space_norm {d : ℕ} (v w : ↑(NormOne d)) : 0 ≤ |(↑v).val (Sum.inl 0)| * |(↑w).val (Sum.inl 0)| - ‖ContrMod.toSpace ↑v‖ * ‖ContrMod.toSpace ↑w‖

Future pointing norm one Lorentz vectors

def Lorentz.Contr.NormOne.FuturePointing (d : ℕ) : Set ↑(NormOne d)

The future pointing Lorentz vectors with Norm one.

Equations

• Lorentz.Contr.NormOne.FuturePointing d x = (0 < (↑x).val (Sum.inl 0))

theorem Lorentz.Contr.NormOne.FuturePointing.mem_iff {d : ℕ} (v : ↑(NormOne d)) : v ∈ FuturePointing d ↔ 0 < (↑v).val (Sum.inl 0)

theorem Lorentz.Contr.NormOne.FuturePointing.mem_iff_inl_nonneg {d : ℕ} (v : ↑(NormOne d)) : v ∈ FuturePointing d ↔ 0 ≤ (↑v).val (Sum.inl 0)

theorem Lorentz.Contr.NormOne.FuturePointing.mem_iff_inl_one_le_inl {d : ℕ} (v : ↑(NormOne d)) : v ∈ FuturePointing d ↔ 1 ≤ (↑v).val (Sum.inl 0)

theorem Lorentz.Contr.NormOne.FuturePointing.mem_iff_parity_mem {d : ℕ} (v : ↑(NormOne d)) : v ∈ FuturePointing d ↔ ⟨((Contr d).ρ LorentzGroup.parity) ↑v, ⋯⟩ ∈ FuturePointing d

theorem Lorentz.Contr.NormOne.FuturePointing.not_mem_iff_inl_le_zero {d : ℕ} (v : ↑(NormOne d)) : v ∉ FuturePointing d ↔ (↑v).val (Sum.inl 0) ≤ 0

theorem Lorentz.Contr.NormOne.FuturePointing.not_mem_iff_inl_lt_zero {d : ℕ} (v : ↑(NormOne d)) : v ∉ FuturePointing d ↔ (↑v).val (Sum.inl 0) < 0

theorem Lorentz.Contr.NormOne.FuturePointing.not_mem_iff_inl_le_neg_one {d : ℕ} (v : ↑(NormOne d)) : v ∉ FuturePointing d ↔ (↑v).val (Sum.inl 0) ≤ -1

theorem Lorentz.Contr.NormOne.FuturePointing.not_mem_iff_neg {d : ℕ} (v : ↑(NormOne d)) : v ∉ FuturePointing d ↔ neg v ∈ FuturePointing d

theorem Lorentz.Contr.NormOne.FuturePointing.inl_nonneg {d : ℕ} (f : ↑(FuturePointing d)) : 0 ≤ (↑↑f).val (Sum.inl 0)

theorem Lorentz.Contr.NormOne.FuturePointing.abs_inl {d : ℕ} (f : ↑(FuturePointing d)) : |(↑↑f).val (Sum.inl 0)| = (↑↑f).val (Sum.inl 0)

theorem Lorentz.Contr.NormOne.FuturePointing.inl_eq_sqrt {d : ℕ} (f : ↑(FuturePointing d)) : (↑↑f).val (Sum.inl 0) = √(1 + ‖ContrMod.toSpace ↑↑f‖ ^ 2)

theorem Lorentz.Contr.NormOne.FuturePointing.metric_nonneg {d : ℕ} (f f' : ↑(FuturePointing d)) : 0 ≤ contrContrContractField (↑↑f ⊗ₜ[ℝ] ↑↑f')

theorem Lorentz.Contr.NormOne.FuturePointing.one_add_metric_non_zero {d : ℕ} (f f' : ↑(FuturePointing d)) : 1 + contrContrContractField (↑↑f ⊗ₜ[ℝ] ↑↑f') ≠ 0

theorem Lorentz.Contr.NormOne.FuturePointing.metric_reflect_mem_mem {d : ℕ} {v w : ↑(NormOne d)} (h : v ∈ FuturePointing d) (hw : w ∈ FuturePointing d) : 0 ≤ contrContrContractField (↑v ⊗ₜ[ℝ] ((Contr d).ρ LorentzGroup.parity) ↑w)

theorem Lorentz.Contr.NormOne.FuturePointing.metric_reflect_not_mem_not_mem {d : ℕ} {v w : ↑(NormOne d)} (h : v ∉ FuturePointing d) (hw : w ∉ FuturePointing d) : 0 ≤ contrContrContractField (↑v ⊗ₜ[ℝ] ((Contr d).ρ LorentzGroup.parity) ↑w)

theorem Lorentz.Contr.NormOne.FuturePointing.metric_reflect_mem_not_mem {d : ℕ} {v w : ↑(NormOne d)} (h : v ∈ FuturePointing d) (hw : w ∉ FuturePointing d) : contrContrContractField (↑v ⊗ₜ[ℝ] ((Contr d).ρ LorentzGroup.parity) ↑w) ≤ 0

theorem Lorentz.Contr.NormOne.FuturePointing.metric_reflect_not_mem_mem {d : ℕ} {v w : ↑(NormOne d)} (h : v ∉ FuturePointing d) (hw : w ∈ FuturePointing d) : contrContrContractField (↑v ⊗ₜ[ℝ] ((Contr d).ρ LorentzGroup.parity) ↑w) ≤ 0

Topology

noncomputable def Lorentz.Contr.NormOne.FuturePointing.timeVecNormOneFuture {d : ℕ} : ↑(FuturePointing d)

The FuturePointing d which has all space components zero.

Equations

• Lorentz.Contr.NormOne.FuturePointing.timeVecNormOneFuture = ⟨⟨Lorentz.ContrMod.stdBasis (Sum.inl 0), ⋯⟩, ⋯⟩

@[simp]

theorem Lorentz.Contr.NormOne.FuturePointing.timeVecNormOneFuture_coe_coe_val {d : ℕ} (a✝ : Fin 1 ⊕ Fin d) : (↑↑timeVecNormOneFuture).val a✝ = (Finsupp.single (Sum.inl 0) 1) a✝

noncomputable def Lorentz.Contr.NormOne.FuturePointing.pathFromTime {d : ℕ} (u : ↑(FuturePointing d)) : Path timeVecNormOneFuture u

A continuous path from timeVecNormOneFuture to any other.

Equations

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

theorem Lorentz.Contr.NormOne.FuturePointing.isPathConnected {d : ℕ} : IsPathConnected Set.univ

theorem Lorentz.Contr.NormOne.FuturePointing.metric_continuous {d : ℕ} (u : ↑(Contr d).V) : Continuous fun (a : ↑(FuturePointing d)) => contrContrContractField (u ⊗ₜ[ℝ] ↑↑a)