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.MinkowskiProductLorentz Velocities
In this module we define Lorentz velocities to be Lorentz vectors which have norm equal to one and which are future-directed.
@[expose] public sectionA Lorentz Velocity is a Lorentz vector which has norm equal to one and which is future-directed.
def Velocity (d : ℕ := 3) : Set (Vector d) := fun v => ⟪v, v⟫ₘ = (1 : ℝ)
∧ 0 < v.timeComponent@[ext]
lemma ext {v w : Velocity d} (h : v.1 = w.1) : v = w := d:ℕv:↑(Velocity d)w:↑(Velocity d)h:↑v = ↑w⊢ v = w
All goals completed! 🐙lemma mem_iff {v : Vector d} : v ∈ Velocity d ↔ ⟪v, v⟫ₘ = (1 : ℝ) ∧ 0 < v.timeComponent := d:ℕv:Vector d⊢ v ∈ Velocity d ↔ (minkowskiProduct v) v = 1 ∧ 0 < v.timeComponent
All goals completed! 🐙@[simp]
lemma minkowskiProduct_self_eq_one (v : Velocity d) : ⟪v.1, v.1⟫ₘ = (1 : ℝ) := v.2.1@[simp]
lemma timeComponent_pos (v : Velocity d) : 0 < v.1.timeComponent := v.2.2@[simp]
lemma timeComponent_nonneg (v : Velocity d) : 0 ≤ v.1.timeComponent := d:ℕv:↑(Velocity d)⊢ 0 ≤ (↑v).timeComponent
All goals completed! 🐙@[simp]
lemma timeComponent_abs (v : Velocity d) :
|v.1.timeComponent| = v.1.timeComponent := d:ℕv:↑(Velocity d)⊢ |(↑v).timeComponent| = (↑v).timeComponent
All goals completed! 🐙d:ℕv:↑(Velocity d)⊢ ‖(↑v).timeComponent‖ ^ 2 - ‖(↑v).spatialPart‖ ^ 2 + ‖(↑v).spatialPart‖ ^ 2 ≤ ‖(↑v).timeComponent‖ ^ 2
All goals completed! 🐙d:ℕv:↑(Velocity d)⊢ ‖(↑v).spatialPart‖ ^ 2 = ↑v (Sum.inl 0) ^ 2 - (‖(↑v).timeComponent‖ ^ 2 - ‖(↑v).spatialPart‖ ^ 2)
All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ ‖(↑u).timeComponent‖ * ‖(↑v).timeComponent‖ - ‖(↑u).spatialPart‖ * ‖(↑v).spatialPart‖ ≤
(↑u).timeComponent * (↑v).timeComponent - inner ℝ (↑u).spatialPart (↑v).spatialPart
d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ ‖(↑u).timeComponent‖ * ‖(↑v).timeComponent‖ ≤ (↑u).timeComponent * (↑v).timeComponentd:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ inner ℝ (↑u).spatialPart (↑v).spatialPart ≤ ‖(↑u).spatialPart‖ * ‖(↑v).spatialPart‖
d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ ‖(↑u).timeComponent‖ * ‖(↑v).timeComponent‖ ≤ (↑u).timeComponent * (↑v).timeComponent All goals completed! 🐙
d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ inner ℝ (↑u).spatialPart (↑v).spatialPart ≤ ‖(↑u).spatialPart‖ * ‖(↑v).spatialPart‖ All goals completed! 🐙lemma one_add_minkowskiProduct_ne_zero (u v : Velocity d) :
1 + ⟪u.1, v.1⟫ₘ ≠ 0 := d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ 1 + (minkowskiProduct ↑u) ↑v ≠ 0
All goals completed! 🐙lemma minkowskiProduct_continuous_snd (u : Vector d) :
Continuous fun (x : Velocity d) => ⟪u, x.1⟫ₘ := d:ℕu:Vector d⊢ Continuous fun x => (minkowskiProduct u) ↑x
All goals completed! 🐙d:ℕu:Vector dh1:(fun x => (minkowskiProduct ↑x) u) = fun x => (minkowskiProduct u) ↑x⊢ Continuous fun x => (minkowskiProduct u) ↑x
All goals completed! 🐙Zero
@[simp]
lemma zero_timeComponent : (0 : Velocity d).1.timeComponent = 1 := d:ℕ⊢ (↑0).timeComponent = 1
d:ℕ⊢ (basis (Sum.inl 0)).timeComponent = 1
All goals completed! 🐙Topology
lemma isPathConnected : IsPathConnected (@Set.univ (Velocity d)) := d:ℕ⊢ IsPathConnected Set.univ
d:ℕ⊢ zero ∈ Set.univ ∧ ∀ ⦃y : ↑(Velocity d)⦄, y ∈ Set.univ → JoinedIn Set.univ zero y
d:ℕ⊢ ∀ ⦃y : ↑(Velocity d)⦄, y ∈ Set.univ → JoinedIn Set.univ zero y
d:ℕy:↑(Velocity d)a:y ∈ Set.univ⊢ JoinedIn Set.univ zero y
d:ℕy:↑(Velocity d)a:y ∈ Set.univ⊢ ∀ (t : ↑unitInterval), (pathFromZero y) t ∈ Set.univ
All goals completed! 🐙