Generalized

📁 Source: PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean

Statistics

Metric	Count
Definitions genBoostAux₁, genBoostAux₂, generalizedBoost	3
Theorems basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂, genBoostAux₁_add_genBoostAux₂_minkowskiProduct, genBoostAux₁_apply_basis, genBoostAux₁_basis_genBoostAux₂_minkowskiProduct, genBoostAux₁_basis_minkowskiProduct, genBoostAux₁_toMatrix_apply, genBoostAux₂_apply_basis, genBoostAux₂_basis_minkowskiProduct, genBoostAux₂_self, genBoostAux₂_toMatrix_apply, genearlizedBoost_apply_basis, generalizedBoost_apply, generalizedBoost_apply_eq_minkowskiProduct, generalizedBoost_apply_eq_toCoord, generalizedBoost_apply_expand, generalizedBoost_apply_fst, generalizedBoost_apply_mul_one_plus_contr, generalizedBoost_apply_snd, generalizedBoost_continuous_fst, generalizedBoost_continuous_snd, generalizedBoost_in_connected_component_of_id, generalizedBoost_inv, generalizedBoost_isOrthochronous, generalizedBoost_isProper, generalizedBoost_mem_restricted, generalizedBoost_self, generalizedBoost_timeComponent_eq, id_joined_generalizedBoost	28
Total	31
⚠️ With sorry generalizedBoost_timeComponent_eq	1

LorentzGroup

Definitions

Name	Category	Theorems
genBoostAux₁ 📖	CompOp	8 math math: genBoostAux₁_basis_genBoostAux₂_minkowskiProduct, generalizedBoost_apply, genBoostAux₁_toMatrix_apply, genBoostAux₁_add_genBoostAux₂_minkowskiProduct, genBoostAux₂_self, genBoostAux₁_basis_minkowskiProduct, genBoostAux₁_apply_basis, basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂
genBoostAux₂ 📖	CompOp	8 math math: genBoostAux₁_basis_genBoostAux₂_minkowskiProduct, generalizedBoost_apply, genBoostAux₁_add_genBoostAux₂_minkowskiProduct, genBoostAux₂_self, genBoostAux₂_toMatrix_apply, genBoostAux₂_basis_minkowskiProduct, genBoostAux₂_apply_basis, basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂
generalizedBoost 📖	CompOp	18 math math: generalizedBoost_isOrthochronous, id_joined_generalizedBoost, generalizedBoost_apply_expand, generalizedBoost_timeComponent_eq, generalizedBoost_apply, generalizedBoost_inv, generalizedBoost_self, genearlizedBoost_apply_basis, generalizedBoost_isProper, generalizedBoost_continuous_snd, generalizedBoost_apply_eq_minkowskiProduct, generalizedBoost_continuous_fst, generalizedBoost_apply_snd, generalizedBoost_apply_mul_one_plus_contr, generalizedBoost_in_connected_component_of_id, generalizedBoost_apply_eq_toCoord, generalizedBoost_mem_restricted, generalizedBoost_apply_fst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂ 📖	mathematical	—	Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct Lorentz.Vector.basis genBoostAux₁ genBoostAux₂ minkowskiMatrix Lorentz.Velocity	—	genBoostAux₁_apply_basis genBoostAux₂_apply_basis Lorentz.Vector.minkowskiProduct_basis_left Lorentz.Velocity.one_add_minkowskiProduct_neq_zero
genBoostAux₁_add_genBoostAux₂_minkowskiProduct 📖	mathematical	—	Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct genBoostAux₁ Lorentz.Vector.basis genBoostAux₂ minkowskiMatrix Lorentz.Velocity	—	genBoostAux₁_basis_minkowskiProduct genBoostAux₂_basis_minkowskiProduct genBoostAux₁_basis_genBoostAux₂_minkowskiProduct Lorentz.Vector.minkowskiProduct_symm
genBoostAux₁_apply_basis 📖	mathematical	—	Lorentz.Vector Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal genBoostAux₁ Lorentz.Vector.basis Lorentz.Vector.isNormedAddCommGroup minkowskiMatrix Lorentz.Velocity	—	Lorentz.Vector.minkowskiProduct_basis_left
genBoostAux₁_basis_genBoostAux₂_minkowskiProduct 📖	mathematical	—	Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct genBoostAux₁ Lorentz.Vector.basis genBoostAux₂ minkowskiMatrix Lorentz.Velocity	—	genBoostAux₁_apply_basis genBoostAux₂_apply_basis Lorentz.Velocity.minkowskiProduct_self_eq_one Lorentz.Vector.minkowskiProduct_symm Lorentz.Velocity.one_add_minkowskiProduct_neq_zero
genBoostAux₁_basis_minkowskiProduct 📖	mathematical	—	Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct genBoostAux₁ Lorentz.Vector.basis minkowskiMatrix Lorentz.Velocity	—	Lorentz.Vector.minkowskiProduct_basis_left Lorentz.Velocity.minkowskiProduct_self_eq_one
genBoostAux₁_toMatrix_apply 📖	mathematical	—	Lorentz.Vector Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.basis genBoostAux₁ minkowskiMatrix Lorentz.Velocity	—	Lorentz.Vector.basis_repr_apply Lorentz.Vector.minkowskiProduct_basis_left
genBoostAux₂_apply_basis 📖	mathematical	—	Lorentz.Vector Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal genBoostAux₂ Lorentz.Vector.basis Lorentz.Vector.isNormedAddCommGroup minkowskiMatrix Lorentz.Velocity Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct	—	Lorentz.Vector.minkowskiProduct_basis_left
genBoostAux₂_basis_minkowskiProduct 📖	mathematical	—	Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct genBoostAux₂ Lorentz.Vector.basis minkowskiMatrix Lorentz.Velocity	—	genBoostAux₂_apply_basis Lorentz.Velocity.minkowskiProduct_self_eq_one Lorentz.Vector.minkowskiProduct_symm Lorentz.Velocity.one_add_minkowskiProduct_neq_zero
genBoostAux₂_self 📖	mathematical	—	genBoostAux₂ Lorentz.Vector Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup genBoostAux₁	—	Lorentz.Velocity.minkowskiProduct_self_eq_one
genBoostAux₂_toMatrix_apply 📖	mathematical	—	Lorentz.Vector Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.basis genBoostAux₂ minkowskiMatrix Lorentz.Velocity Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct	—	Lorentz.Vector.basis_repr_apply Lorentz.Vector.minkowskiProduct_basis_left Lorentz.Velocity.one_add_minkowskiProduct_neq_zero
genearlizedBoost_apply_basis 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.tensorial generalizedBoost Lorentz.Vector.basis Lorentz.Vector.isNormedAddCommGroup minkowskiMatrix Lorentz.Velocity Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct	—	generalizedBoost_apply genBoostAux₁_apply_basis genBoostAux₂_apply_basis Lorentz.Vector.basis_apply Lorentz.Vector.apply_sub
generalizedBoost_apply 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.tensorial generalizedBoost genBoostAux₁ genBoostAux₂	—	Lorentz.Vector.smul_eq_mulVec Lorentz.Vector.map_apply_eq_basis_mulVec
generalizedBoost_apply_eq_minkowskiProduct 📖	mathematical	—	LorentzGroup generalizedBoost minkowskiMatrix Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct Lorentz.Vector.basis Lorentz.Velocity	—	generalizedBoost.eq_1 Lorentz.Vector.minkowskiProduct_basis_right Lorentz.Vector.basis_apply minkowskiMatrix.η_apply_mul_η_apply_diag genBoostAux₁_toMatrix_apply Lorentz.Vector.minkowskiProduct_basis_left minkowskiMatrix.η_apply_sq_eq_one genBoostAux₂_toMatrix_apply
generalizedBoost_apply_eq_toCoord 📖	mathematical	—	LorentzGroup generalizedBoost minkowskiMatrix Lorentz.Vector Lorentz.Velocity Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct	—	generalizedBoost.eq_1 genBoostAux₁_toMatrix_apply genBoostAux₂_toMatrix_apply
generalizedBoost_apply_expand 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.tensorial generalizedBoost Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct Lorentz.Velocity	—	Lorentz.Vector.instFiniteDimensionalReal Lorentz.Velocity.one_add_minkowskiProduct_neq_zero generalizedBoost_apply_mul_one_plus_contr
generalizedBoost_apply_fst 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.tensorial generalizedBoost Lorentz.Velocity	—	Lorentz.Vector.instFiniteDimensionalReal Lorentz.Velocity.one_add_minkowskiProduct_neq_zero generalizedBoost_apply_mul_one_plus_contr Lorentz.Velocity.minkowskiProduct_self_eq_one
generalizedBoost_apply_mul_one_plus_contr 📖	mathematical	—	Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct Lorentz.Velocity LorentzGroup TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.tensorial generalizedBoost	—	generalizedBoost_apply genBoostAux₁.eq_1 genBoostAux₂.eq_1 Lorentz.Velocity.one_add_minkowskiProduct_neq_zero
generalizedBoost_apply_snd 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.tensorial generalizedBoost Lorentz.Velocity Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct	—	Lorentz.Vector.instFiniteDimensionalReal Lorentz.Velocity.one_add_minkowskiProduct_neq_zero generalizedBoost_apply_mul_one_plus_contr Lorentz.Velocity.minkowskiProduct_self_eq_one Lorentz.Vector.minkowskiProduct_symm
generalizedBoost_continuous_fst 📖	mathematical	—	Lorentz.Vector Lorentz.Velocity LorentzGroup Lorentz.Velocity.instTopologicalSpaceElemVector instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup generalizedBoost	—	generalizedBoost_apply_eq_minkowskiProduct Lorentz.Velocity.minkowskiProduct_continuous_fst Lorentz.Velocity.one_add_minkowskiProduct_neq_zero
generalizedBoost_continuous_snd 📖	mathematical	—	Lorentz.Vector Lorentz.Velocity LorentzGroup Lorentz.Velocity.instTopologicalSpaceElemVector instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup generalizedBoost	—	generalizedBoost_apply_eq_minkowskiProduct Lorentz.Velocity.one_add_minkowskiProduct_neq_zero
generalizedBoost_in_connected_component_of_id 📖	mathematical	—	LorentzGroup instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup lorentzGroupIsGroup generalizedBoost	—	id_joined_generalizedBoost
generalizedBoost_inv 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup generalizedBoost	—	eq_of_action_vector_eq Lorentz.Vector.instFiniteDimensionalReal Lorentz.Velocity.one_add_minkowskiProduct_neq_zero generalizedBoost_apply_mul_one_plus_contr Lorentz.Vector.minkowskiProduct_symm generalizedBoost_apply_expand Lorentz.Velocity.minkowskiProduct_self_eq_one
generalizedBoost_isOrthochronous 📖	mathematical	—	IsOrthochronous generalizedBoost	—	isOrthochronous_on_connected_component generalizedBoost_in_connected_component_of_id id_isOrthochronous
generalizedBoost_isProper 📖	mathematical	—	IsProper generalizedBoost	—	isProper_on_connected_component generalizedBoost_in_connected_component_of_id isProper_id
generalizedBoost_mem_restricted 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup restricted generalizedBoost	—	restricted.eq_1 generalizedBoost_isProper generalizedBoost_isOrthochronous
generalizedBoost_self 📖	mathematical	—	generalizedBoost LorentzGroup lorentzGroupIsGroup	—	genBoostAux₂_self
generalizedBoost_timeComponent_eq 📖 ⚠️	mathematical	—	LorentzGroup generalizedBoost Lorentz.Vector.timeComponent Lorentz.Vector Lorentz.Velocity Lorentz.Vector.spatialPart Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct	—	—
id_joined_generalizedBoost 📖	mathematical	—	LorentzGroup instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup lorentzGroupIsGroup generalizedBoost	—	Lorentz.Velocity.isPathConnected generalizedBoost_continuous_snd generalizedBoost_self

---

← Back to Index