refactor: Last batch of multi-goal proofs
This commit is contained in:
jstoobysmith
parent
b9479c904d
commit
c0499483a8
43 changed files with 910 additions and 955 deletions
|
|
@ -66,11 +66,11 @@ lemma mem_iff_norm : Λ ∈ LorentzGroup d ↔
|
|||
lemma mem_iff_on_right : Λ ∈ LorentzGroup d ↔
|
||||
∀ (x y : LorentzVector d), ⟪x, (dual Λ * Λ) *ᵥ y⟫ₘ = ⟪x, y⟫ₘ := by
|
||||
refine Iff.intro (fun h x y ↦ ?_) (fun h x y ↦ ?_)
|
||||
have h1 := h x y
|
||||
rw [← dual_mulVec_right, mulVec_mulVec] at h1
|
||||
exact h1
|
||||
rw [← dual_mulVec_right, mulVec_mulVec]
|
||||
exact h x y
|
||||
· have h1 := h x y
|
||||
rw [← dual_mulVec_right, mulVec_mulVec] at h1
|
||||
exact h1
|
||||
· rw [← dual_mulVec_right, mulVec_mulVec]
|
||||
exact h x y
|
||||
|
||||
lemma mem_iff_dual_mul_self : Λ ∈ LorentzGroup d ↔ dual Λ * Λ = 1 := by
|
||||
rw [mem_iff_on_right, matrix_eq_id_iff]
|
||||
|
|
@ -96,9 +96,9 @@ lemma mem_iff_transpose : Λ ∈ LorentzGroup d ↔ Λᵀ ∈ LorentzGroup d :=
|
|||
lemma mem_mul (hΛ : Λ ∈ LorentzGroup d) (hΛ' : Λ' ∈ LorentzGroup d) : Λ * Λ' ∈ LorentzGroup d := by
|
||||
rw [mem_iff_dual_mul_self, dual_mul]
|
||||
trans dual Λ' * (dual Λ * Λ) * Λ'
|
||||
noncomm_ring
|
||||
rw [(mem_iff_dual_mul_self).mp hΛ]
|
||||
simp [(mem_iff_dual_mul_self).mp hΛ']
|
||||
· noncomm_ring
|
||||
· rw [(mem_iff_dual_mul_self).mp hΛ]
|
||||
simp [(mem_iff_dual_mul_self).mp hΛ']
|
||||
|
||||
lemma one_mem : 1 ∈ LorentzGroup d := by
|
||||
rw [mem_iff_dual_mul_self]
|
||||
|
|
@ -140,18 +140,18 @@ lemma coe_inv : (Λ⁻¹).1 = Λ.1⁻¹:= (inv_eq_left_inv (mem_iff_dual_mul_sel
|
|||
@[simp]
|
||||
lemma subtype_inv_mul : (Subtype.val Λ)⁻¹ * (Subtype.val Λ) = 1 := by
|
||||
trans Subtype.val (Λ⁻¹ * Λ)
|
||||
rw [← coe_inv]
|
||||
simp only [lorentzGroupIsGroup_inv, lorentzGroupIsGroup_mul_coe]
|
||||
rw [inv_mul_self Λ]
|
||||
simp only [lorentzGroupIsGroup_one_coe]
|
||||
· rw [← coe_inv]
|
||||
simp only [lorentzGroupIsGroup_inv, lorentzGroupIsGroup_mul_coe]
|
||||
· rw [inv_mul_self Λ]
|
||||
simp only [lorentzGroupIsGroup_one_coe]
|
||||
|
||||
@[simp]
|
||||
lemma subtype_mul_inv : (Subtype.val Λ) * (Subtype.val Λ)⁻¹ = 1 := by
|
||||
trans Subtype.val (Λ * Λ⁻¹)
|
||||
rw [← coe_inv]
|
||||
simp only [lorentzGroupIsGroup_inv, lorentzGroupIsGroup_mul_coe]
|
||||
rw [mul_inv_self Λ]
|
||||
simp only [lorentzGroupIsGroup_one_coe]
|
||||
· rw [← coe_inv]
|
||||
simp only [lorentzGroupIsGroup_inv, lorentzGroupIsGroup_mul_coe]
|
||||
· rw [mul_inv_self Λ]
|
||||
simp only [lorentzGroupIsGroup_one_coe]
|
||||
|
||||
@[simp]
|
||||
lemma mul_minkowskiMatrix_mul_transpose :
|
||||
|
|
|
|||
|
|
@ -107,23 +107,22 @@ lemma toMatrix_continuous (u : FuturePointing d) : Continuous (toMatrix u) := by
|
|||
simp only [toMatrix_apply]
|
||||
refine (continuous_mul_left (η i i)).comp' ?_
|
||||
refine Continuous.sub ?_ ?_
|
||||
refine .comp' (continuous_add_left (minkowskiMetric (e i) (e j))) ?_
|
||||
refine .comp' (continuous_mul_left (2 * ⟪e j, u⟫ₘ)) ?_
|
||||
exact FuturePointing.metric_continuous _
|
||||
· refine .comp' (continuous_add_left (minkowskiMetric (e i) (e j))) ?_
|
||||
refine .comp' (continuous_mul_left (2 * ⟪e j, u⟫ₘ)) ?_
|
||||
exact FuturePointing.metric_continuous _
|
||||
refine .mul ?_ ?_
|
||||
refine .mul ?_ ?_
|
||||
simp only [(minkowskiMetric _).map_add]
|
||||
refine .comp' ?_ ?_
|
||||
exact continuous_add_left ((minkowskiMetric (stdBasis i)) ↑u)
|
||||
exact FuturePointing.metric_continuous _
|
||||
simp only [(minkowskiMetric _).map_add]
|
||||
refine .comp' ?_ ?_
|
||||
exact continuous_add_left _
|
||||
exact FuturePointing.metric_continuous _
|
||||
refine .inv₀ ?_ ?_
|
||||
refine .comp' (continuous_add_left 1) ?_
|
||||
exact FuturePointing.metric_continuous _
|
||||
exact fun x => FuturePointing.one_add_metric_non_zero u x
|
||||
· refine .mul ?_ ?_
|
||||
· simp only [(minkowskiMetric _).map_add]
|
||||
refine .comp' ?_ ?_
|
||||
· exact continuous_add_left ((minkowskiMetric (stdBasis i)) ↑u)
|
||||
· exact FuturePointing.metric_continuous _
|
||||
· simp only [(minkowskiMetric _).map_add]
|
||||
refine .comp' ?_ ?_
|
||||
· exact continuous_add_left _
|
||||
· exact FuturePointing.metric_continuous _
|
||||
· refine .inv₀ ?_ ?_
|
||||
· refine .comp' (continuous_add_left 1) (FuturePointing.metric_continuous _)
|
||||
exact fun x => FuturePointing.one_add_metric_non_zero u x
|
||||
|
||||
lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ LorentzGroup d:= by
|
||||
intro x y
|
||||
|
|
|
|||
|
|
@ -56,10 +56,10 @@ lemma not_orthochronous_iff_le_neg_one :
|
|||
lemma not_orthochronous_iff_le_zero :
|
||||
¬ IsOrthochronous Λ ↔ timeComp Λ ≤ 0 := by
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
rw [not_orthochronous_iff_le_neg_one] at h
|
||||
linarith
|
||||
rw [IsOrthochronous_iff_ge_one]
|
||||
linarith
|
||||
· rw [not_orthochronous_iff_le_neg_one] at h
|
||||
linarith
|
||||
· rw [IsOrthochronous_iff_ge_one]
|
||||
linarith
|
||||
|
||||
/-- The continuous map taking a Lorentz transformation to its `0 0` element. -/
|
||||
def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => timeComp Λ,
|
||||
|
|
@ -73,13 +73,13 @@ def stepFunction : ℝ → ℝ := fun t =>
|
|||
lemma stepFunction_continuous : Continuous stepFunction := by
|
||||
apply Continuous.if ?_ continuous_const (Continuous.if ?_ continuous_const continuous_id)
|
||||
<;> intro a ha
|
||||
rw [@Set.Iic_def, @frontier_Iic, @Set.mem_singleton_iff] at ha
|
||||
rw [ha]
|
||||
simp [neg_lt_self_iff, zero_lt_one, ↓reduceIte]
|
||||
have h1 : ¬ (1 : ℝ) ≤ 0 := by simp
|
||||
exact Eq.symm (if_neg h1)
|
||||
rw [Set.Ici_def, @frontier_Ici, @Set.mem_singleton_iff] at ha
|
||||
exact id (Eq.symm ha)
|
||||
· rw [@Set.Iic_def, @frontier_Iic, @Set.mem_singleton_iff] at ha
|
||||
rw [ha]
|
||||
simp [neg_lt_self_iff, zero_lt_one, ↓reduceIte]
|
||||
have h1 : ¬ (1 : ℝ) ≤ 0 := by simp
|
||||
exact Eq.symm (if_neg h1)
|
||||
· rw [Set.Ici_def, @frontier_Ici, @Set.mem_singleton_iff] at ha
|
||||
exact id (Eq.symm ha)
|
||||
|
||||
/-- The continuous map from `lorentzGroup` to `ℝ` wh
|
||||
taking Orthochronous elements to `1` and non-orthochronous to `-1`. -/
|
||||
|
|
@ -102,8 +102,8 @@ lemma orthchroMapReal_on_not_IsOrthochronous {Λ : LorentzGroup d} (h : ¬ IsOrt
|
|||
lemma orthchroMapReal_minus_one_or_one (Λ : LorentzGroup d) :
|
||||
orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1 := by
|
||||
by_cases h : IsOrthochronous Λ
|
||||
apply Or.inr $ orthchroMapReal_on_IsOrthochronous h
|
||||
apply Or.inl $ orthchroMapReal_on_not_IsOrthochronous h
|
||||
· exact Or.inr $ orthchroMapReal_on_IsOrthochronous h
|
||||
· exact Or.inl $ orthchroMapReal_on_not_IsOrthochronous h
|
||||
|
||||
local notation "ℤ₂" => Multiplicative (ZMod 2)
|
||||
|
||||
|
|
@ -158,18 +158,18 @@ def orthchroRep : LorentzGroup d →* ℤ₂ where
|
|||
simp only
|
||||
by_cases h : IsOrthochronous Λ
|
||||
<;> by_cases h' : IsOrthochronous Λ'
|
||||
rw [orthchroMap_IsOrthochronous h, orthchroMap_IsOrthochronous h',
|
||||
orthchroMap_IsOrthochronous (mul_othchron_of_othchron_othchron h h')]
|
||||
rfl
|
||||
rw [orthchroMap_IsOrthochronous h, orthchroMap_not_IsOrthochronous h',
|
||||
orthchroMap_not_IsOrthochronous (mul_not_othchron_of_othchron_not_othchron h h')]
|
||||
rfl
|
||||
rw [orthchroMap_not_IsOrthochronous h, orthchroMap_IsOrthochronous h',
|
||||
orthchroMap_not_IsOrthochronous (mul_not_othchron_of_not_othchron_othchron h h')]
|
||||
rfl
|
||||
rw [orthchroMap_not_IsOrthochronous h, orthchroMap_not_IsOrthochronous h',
|
||||
orthchroMap_IsOrthochronous (mul_othchron_of_not_othchron_not_othchron h h')]
|
||||
rfl
|
||||
· rw [orthchroMap_IsOrthochronous h, orthchroMap_IsOrthochronous h',
|
||||
orthchroMap_IsOrthochronous (mul_othchron_of_othchron_othchron h h')]
|
||||
rfl
|
||||
· rw [orthchroMap_IsOrthochronous h, orthchroMap_not_IsOrthochronous h',
|
||||
orthchroMap_not_IsOrthochronous (mul_not_othchron_of_othchron_not_othchron h h')]
|
||||
rfl
|
||||
· rw [orthchroMap_not_IsOrthochronous h, orthchroMap_IsOrthochronous h',
|
||||
orthchroMap_not_IsOrthochronous (mul_not_othchron_of_not_othchron_othchron h h')]
|
||||
rfl
|
||||
· rw [orthchroMap_not_IsOrthochronous h, orthchroMap_not_IsOrthochronous h',
|
||||
orthchroMap_IsOrthochronous (mul_othchron_of_not_othchron_not_othchron h h')]
|
||||
rfl
|
||||
|
||||
end LorentzGroup
|
||||
|
||||
|
|
|
|||
|
|
@ -60,19 +60,17 @@ def detContinuous : C(𝓛 d, ℤ₂) :=
|
|||
|
||||
lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup d) :
|
||||
detContinuous Λ = detContinuous Λ' ↔ Λ.1.det = Λ'.1.det := by
|
||||
apply Iff.intro
|
||||
intro h
|
||||
simp [detContinuous] at h
|
||||
cases' det_eq_one_or_neg_one Λ with h1 h1
|
||||
<;> cases' det_eq_one_or_neg_one Λ' with h2 h2
|
||||
<;> simp_all [h1, h2, h]
|
||||
rw [← toMul_zero, @Equiv.apply_eq_iff_eq] at h
|
||||
· change (0 : Fin 2) = (1 : Fin 2) at h
|
||||
simp only [Fin.isValue, zero_ne_one] at h
|
||||
· change (1 : Fin 2) = (0 : Fin 2) at h
|
||||
simp only [Fin.isValue, one_ne_zero] at h
|
||||
· intro h
|
||||
simp [detContinuous, h]
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
· simp [detContinuous] at h
|
||||
cases' det_eq_one_or_neg_one Λ with h1 h1
|
||||
<;> cases' det_eq_one_or_neg_one Λ' with h2 h2
|
||||
<;> simp_all [h1, h2, h]
|
||||
· rw [← toMul_zero, @Equiv.apply_eq_iff_eq] at h
|
||||
· change (0 : Fin 2) = (1 : Fin 2) at h
|
||||
simp only [Fin.isValue, zero_ne_one] at h
|
||||
· change (1 : Fin 2) = (0 : Fin 2) at h
|
||||
simp only [Fin.isValue, one_ne_zero] at h
|
||||
· simp [detContinuous, h]
|
||||
|
||||
/-- The representation taking a Lorentz matrix to its determinant. -/
|
||||
@[simps!]
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue