DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update Metric.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-06-08 04:14:13 +02:00
parent f259183222
commit 11aa512e80
1 changed files with 5 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

27
HepLean/SpaceTime/Metric.lean
View file

@ -85,40 +85,23 @@ lemma η_transpose : η.transpose = η := by
@[simp]
lemma det_η : η.det = - 1 := by
simp only [η_explicit, det_succ_row_zero, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue,
of_apply, cons_val', empty_val', cons_val_fin_one, cons_val_zero, submatrix_apply,
Fin.succ_zero_eq_one, cons_val_one, head_cons, submatrix_submatrix, Function.comp_apply,
Fin.succ_one_eq_two, cons_val_two, tail_cons, det_unique, Fin.default_eq_zero, cons_val_succ,
head_fin_const, Fin.sum_univ_succ, Fin.val_zero, pow_zero, one_mul, Fin.zero_succAbove,
Finset.univ_unique, Fin.val_succ, Fin.coe_fin_one, zero_add, pow_one, neg_mul,
Fin.succ_succAbove_zero, Finset.sum_neg_distrib, Finset.sum_singleton, Fin.succ_succAbove_one,
even_two, Even.neg_pow, one_pow, mul_one, mul_neg, neg_neg, mul_zero, neg_zero, add_zero,
zero_mul, Finset.sum_const_zero]
simp [η_explicit, det_succ_row_zero, Fin.sum_univ_succ]
@[simp]
lemma η_sq : η * η = 1 := by
funext μ ν
rw [mul_apply, Fin.sum_univ_four]
fin_cases μ <;> fin_cases ν <;>
simp [η_explicit, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one,
Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons,
Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one,
vecHead, vecTail, Function.comp_apply]
simp [η_explicit, vecHead, vecTail]
lemma η_diag_mul_self (μ : Fin 4) : η μ μ * η μ μ = 1 := by
fin_cases μ
<;> simp [η_explicit]
lemma η_mulVec (x : spaceTime) : η *ᵥ x = ![x 0, -x 1, -x 2, -x 3] := by
rw [explicit x]
rw [η_explicit]
rw [explicit x, η_explicit]
funext i
rw [mulVec, dotProduct, Fin.sum_univ_four]
fin_cases i <;>
simp [Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one,
Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons,
Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one,
vecHead, vecTail, Function.comp_apply]
simp [vecHead, vecTail]
/-- Given a point in spaceTime `x` the linear map `y → x ⬝ᵥ (η *ᵥ y)`. -/
@[simps!]
@ -128,7 +111,7 @@ def linearMapForSpaceTime (x : spaceTime) : spaceTime →ₗ[ℝ] ℝ where
simp only
rw [mulVec_add, dotProduct_add]
map_smul' c y := by
simp only
simp only [RingHom.id_apply, smul_eq_mul]
rw [mulVec_smul, dotProduct_smul]
rfl