Merge pull request #369 from HEPLean/bump-v4.17

Bump v4.17

PhysLean/CondensedMatter/Basic.lean

@@ -10,7 +10,6 @@ Authors: Joseph Tooby-Smith
 This directory is currently a place holder.
 Please feel free to contribute!
 
-
 Some directories which are NOT currently place holders are:
 - Mathematics
 - Meta
@@ -19,5 +18,4 @@ Some directories which are NOT currently place holders are:
 - Quantum Mechanics
 - Relativity
 
-
 -/

PhysLean/Mathematics/SO3/Basic.lean

@@ -117,7 +117,7 @@ lemma toGL_embedding : IsEmbedding toGL.toFun where
 
 /-- The instance of a topological group on `SO(3)`, defined through the embedding of `SO(3)`
   into `GL(n)`. -/
-instance : TopologicalGroup SO(3) :=
+instance : IsTopologicalGroup SO(3) :=
   IsInducing.topologicalGroup toGL toGL_embedding.toIsInducing
 
 /-- The determinant of an `SO(3)` matrix minus the identity is equal to zero. -/

PhysLean/Mathematics/SchurTriangulation.lean

@@ -85,27 +85,6 @@ variable [RCLike 𝕜]
 section
 variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
 
-section
-variable [FiniteDimensional 𝕜 E] [Fintype n] [DecidableEq n]
-
-lemma toMatrixOrthonormal_apply_apply (b : OrthonormalBasis n 𝕜 E) (f : Module.End 𝕜 E)
-    (i j : n) :
-    toMatrixOrthonormal b f i j = ⟪b i, f (b j)⟫_𝕜 :=
-  calc
-    _ = b.repr (f (b j)) i := f.toMatrix_apply ..
-    _ = ⟪b i, f (b j)⟫_𝕜 := b.repr_apply_apply ..
-
-lemma toMatrixOrthonormal_reindex [Fintype m] [DecidableEq m]
-    (b : OrthonormalBasis m 𝕜 E) (e : m ≃ n) (f : Module.End 𝕜 E) :
-    toMatrixOrthonormal (b.reindex e) f = Matrix.reindex e e (toMatrixOrthonormal b f) :=
-  Matrix.ext fun i j =>
-    calc toMatrixOrthonormal (b.reindex e) f i j
-      _ = (b.reindex e).repr (f (b.reindex e j)) i := f.toMatrix_apply ..
-      _ = b.repr (f (b (e.symm j))) (e.symm i) := by simp
-      _ = toMatrixOrthonormal b f (e.symm i) (e.symm j) := Eq.symm <| f.toMatrix_apply ..
-
-end
-
 /-- **Don't use this definition directly.** Instead, use `Matrix.schurTriangulationBasis`,
 `Matrix.schurTriangulationUnitary`, and `Matrix.schurTriangulation`. See also
 `LinearMap.SchurTriangulationAux.of` and `Matrix.schurTriangulationAux`. -/

PhysLean/Meta/Notes/ToHTML.lean

@@ -18,8 +18,8 @@ variable (N : NoteFile)
 
 /-- Sorts `NoteInfo`'s by file name then by line number. -/
 def sortLE (ni1 ni2 : HTMLNote) : Bool :=
-  if N.files.indexOf ni1.fileName ≠ N.files.indexOf ni2.fileName
-  then N.files.indexOf ni1.fileName ≤ N.files.indexOf ni2.fileName
+  if N.files.idxOf ni1.fileName ≠ N.files.idxOf ni2.fileName
+  then N.files.idxOf ni1.fileName ≤ N.files.idxOf ni2.fileName
   else
   ni1.line ≤ ni2.line
 

PhysLean/Optics/Basic.lean

@@ -18,5 +18,4 @@ Some directories which are NOT currently place holders are:
 - Quantum Mechanics
 - Relativity
 
-
 -/

PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean

@@ -69,14 +69,14 @@ lemma swap_fields : P.toFun Φ1 Φ2 =
     (conj P.𝓵₅) (conj P.𝓵₇) (conj P.𝓵₆)).toFun Φ2 Φ1 := by
   funext x
   simp only [toFun, normSq, Complex.add_re, Complex.mul_re, Complex.conj_re, Complex.conj_im,
-    neg_mul, sub_neg_eq_add, one_div, Complex.norm_eq_abs, Complex.inv_re, Complex.re_ofNat,
+    neg_mul, sub_neg_eq_add, one_div, Complex.inv_re, Complex.re_ofNat,
     Complex.normSq_ofNat, div_self_mul_self', Complex.inv_im, Complex.im_ofNat, neg_zero, zero_div,
     zero_mul, sub_zero, Complex.mul_im, add_zero, mul_neg, Complex.ofReal_pow, normSq_apply_re_self,
     normSq_apply_im_zero, mul_zero, zero_add, RingHomCompTriple.comp_apply, RingHom.id_apply]
   ring_nf
   simp only [one_div, add_left_inj, add_right_inj, mul_eq_mul_left_iff]
   left
-  rw [HiggsField.innerProd, HiggsField.innerProd, ← InnerProductSpace.conj_symm, Complex.abs_conj]
+  rw [HiggsField.innerProd, HiggsField.innerProd, ← InnerProductSpace.conj_symm, Complex.norm_conj]
 
 /-- If `Φ₂` is zero the potential reduces to the Higgs potential on `Φ₁`. -/
 lemma right_zero : P.toFun Φ1 0 =
@@ -103,7 +103,7 @@ lemma neg_left : P.toFun (- Φ1) Φ2
   simp only [toFun, normSq, ContMDiffSection.coe_neg, Pi.neg_apply, norm_neg,
     innerProd_neg_left, mul_neg, innerProd_neg_right, Complex.add_re, Complex.neg_re,
     Complex.mul_re, neg_sub, Complex.conj_re, Complex.conj_im, neg_mul, sub_neg_eq_add, neg_add_rev,
-    one_div, Complex.norm_eq_abs, even_two, Even.neg_pow, Complex.inv_re, Complex.re_ofNat,
+    one_div, even_two, Even.neg_pow, Complex.inv_re, Complex.re_ofNat,
     Complex.normSq_ofNat, div_self_mul_self', Complex.inv_im, Complex.im_ofNat, neg_zero, zero_div,
     zero_mul, sub_zero, Complex.mul_im, add_zero, Complex.ofReal_pow, map_neg]
 

PhysLean/Particles/FlavorPhysics/CKMMatrix/Basic.lean

@@ -304,7 +304,7 @@ end phaseShiftApply
 
 /-- The absolute value of the `(i,j)`th element of `V`. -/
 @[simp]
-def VAbs' (V : unitaryGroup (Fin 3) ℂ) (i j : Fin 3) : ℝ := Complex.abs (V i j)
+def VAbs' (V : unitaryGroup (Fin 3) ℂ) (i j : Fin 3) : ℝ := norm (V i j)
 
 /-- If two CKM matrices are equivalent (under phase shifts), then their absolute values
   are the same. -/
@@ -323,11 +323,11 @@ lemma VAbs'_equiv (i j : Fin 3) (V U : CKMMatrix) (h : V ≈ U) :
   fin_cases i <;> fin_cases j <;>
     simp only [Fin.zero_eta, Fin.isValue, cons_val_zero, zero_mul, add_zero, mul_zero,
       _root_.map_mul, mul_re, I_re, ofReal_re, I_im, ofReal_im, sub_self, Real.exp_zero,
-      one_mul, mul_one, Complex.abs_exp, Fin.mk_one, cons_val_one, head_cons, zero_add,
+      one_mul, mul_one,Fin.mk_one, cons_val_one, head_cons, zero_add,
       head_fin_const, Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons,
-      tail_val', head_val']
-  all_goals change Complex.abs (0 * _ + _) = _
-  all_goals simp [Complex.abs_exp]
+      tail_val', head_val', Complex.norm_exp, Complex.norm_mul]
+  all_goals change norm (0 * _ + _) = _
+  all_goals simp [Complex.norm_exp]
 
 /-- The absolute value of the `(i,j)`th any representative of `⟦V⟧`. -/
 def VAbs (i j : Fin 3) : Quotient CKMMatrixSetoid → ℝ :=

PhysLean/Particles/FlavorPhysics/CKMMatrix/PhaseFreedom.lean

@@ -28,7 +28,7 @@ variable (u c t d s b : ℝ)
 lemma shift_ud_phase_zero (V : CKMMatrix) (h1 : u + d = - arg [V]ud) :
     [phaseShiftApply V u c t d s b]ud = VudAbs ⟦V⟧ := by
   rw [phaseShiftApply.ud]
-  rw [← abs_mul_exp_arg_mul_I [V]ud]
+  rw [← norm_mul_exp_arg_mul_I [V]ud]
   rw [mul_comm, mul_assoc, ← exp_add]
   have h2 : ↑(arg (V.1 0 0)) * I + (↑u * I + ↑d * I) = ↑(arg (V.1 0 0) + (u + d)) * I := by
     simp only [Fin.isValue, ofReal_add]
@@ -40,7 +40,7 @@ lemma shift_ud_phase_zero (V : CKMMatrix) (h1 : u + d = - arg [V]ud) :
 
 lemma shift_us_phase_zero {V : CKMMatrix} (h1 : u + s = - arg [V]us) :
     [phaseShiftApply V u c t d s b]us = VusAbs ⟦V⟧ := by
-  rw [phaseShiftApply.us, ← abs_mul_exp_arg_mul_I [V]us, mul_comm, mul_assoc, ← exp_add]
+  rw [phaseShiftApply.us, ← norm_mul_exp_arg_mul_I [V]us, mul_comm, mul_assoc, ← exp_add]
   have h2 : ↑(arg [V]us) * I + (↑u * I + ↑s * I) = ↑(arg [V]us + (u + s)) * I := by
     simp only [Fin.isValue, ofReal_add]
     ring
@@ -52,7 +52,7 @@ lemma shift_us_phase_zero {V : CKMMatrix} (h1 : u + s = - arg [V]us) :
 lemma shift_ub_phase_zero {V : CKMMatrix} (h1 : u + b = - arg [V]ub) :
     [phaseShiftApply V u c t d s b]ub = VubAbs ⟦V⟧ := by
   rw [phaseShiftApply.ub]
-  rw [← abs_mul_exp_arg_mul_I [V]ub]
+  rw [← norm_mul_exp_arg_mul_I [V]ub]
   rw [mul_comm, mul_assoc, ← exp_add]
   have h2 : ↑(arg [V]ub) * I + (↑u * I + ↑b * I) = ↑(arg [V]ub + (u + b)) * I := by
     simp only [Fin.isValue, ofReal_add]
@@ -65,7 +65,7 @@ lemma shift_ub_phase_zero {V : CKMMatrix} (h1 : u + b = - arg [V]ub) :
 lemma shift_cs_phase_zero {V : CKMMatrix} (h1 : c + s = - arg [V]cs) :
     [phaseShiftApply V u c t d s b]cs = VcsAbs ⟦V⟧ := by
   rw [phaseShiftApply.cs]
-  rw [← abs_mul_exp_arg_mul_I [V]cs]
+  rw [← norm_mul_exp_arg_mul_I [V]cs]
   rw [mul_comm, mul_assoc, ← exp_add]
   have h2 : ↑(arg [V]cs) * I + (↑c * I + ↑s * I) = ↑(arg [V]cs + (c + s)) * I := by
     simp only [Fin.isValue, ofReal_add]
@@ -78,7 +78,7 @@ lemma shift_cs_phase_zero {V : CKMMatrix} (h1 : c + s = - arg [V]cs) :
 lemma shift_cb_phase_zero {V : CKMMatrix} (h1 : c + b = - arg [V]cb) :
     [phaseShiftApply V u c t d s b]cb = VcbAbs ⟦V⟧ := by
   rw [phaseShiftApply.cb]
-  rw [← abs_mul_exp_arg_mul_I [V]cb]
+  rw [← norm_mul_exp_arg_mul_I [V]cb]
   rw [mul_comm, mul_assoc, ← exp_add]
   have h2 : ↑(arg [V]cb) * I + (↑c * I + ↑b * I) = ↑(arg [V]cb + (c + b)) * I := by
     simp only [Fin.isValue, ofReal_add]
@@ -91,7 +91,7 @@ lemma shift_cb_phase_zero {V : CKMMatrix} (h1 : c + b = - arg [V]cb) :
 lemma shift_tb_phase_zero {V : CKMMatrix} (h1 : t + b = - arg [V]tb) :
     [phaseShiftApply V u c t d s b]tb = VtbAbs ⟦V⟧ := by
   rw [phaseShiftApply.tb]
-  rw [← abs_mul_exp_arg_mul_I [V]tb]
+  rw [← norm_mul_exp_arg_mul_I [V]tb]
   rw [mul_comm, mul_assoc, ← exp_add]
   have h2 : ↑(arg [V]tb) * I + (↑t * I + ↑b * I) = ↑(arg [V]tb + (t + b)) * I := by
     simp only [Fin.isValue, ofReal_add]
@@ -104,7 +104,7 @@ lemma shift_tb_phase_zero {V : CKMMatrix} (h1 : t + b = - arg [V]tb) :
 lemma shift_cd_phase_pi {V : CKMMatrix} (h1 : c + d = Real.pi - arg [V]cd) :
     [phaseShiftApply V u c t d s b]cd = - VcdAbs ⟦V⟧ := by
   rw [phaseShiftApply.cd]
-  rw [← abs_mul_exp_arg_mul_I [V]cd]
+  rw [← norm_mul_exp_arg_mul_I [V]cd]
   rw [mul_comm, mul_assoc, ← exp_add]
   have h2 : ↑(arg [V]cd) * I + (↑c * I + ↑d * I) = ↑(arg [V]cd + (c + d)) * I := by
     simp only [Fin.isValue, ofReal_add]
@@ -278,22 +278,22 @@ lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud
       have h1 : VudAbs ⟦U⟧ = 0 := by
         rw [hUV]
         simp [VAbs, hb]
-      simp only [VudAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, map_eq_zero] at h1
+      simp only [VudAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, norm_eq_zero] at h1
       exact h1
     apply And.intro
     · simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at hb
       have h1 : VusAbs ⟦U⟧ = 0 := by
         rw [hUV]
         simp [VAbs, hb]
-      simp only [VusAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, map_eq_zero] at h1
+      simp only [VusAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, norm_eq_zero] at h1
       exact h1
     apply And.intro
     · simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at hb
       have h3 := cb_eq_zero_of_ud_us_zero hb
       have h1 : VcbAbs ⟦U⟧ = 0 := by
         rw [hUV]
         simp [VAbs, h3]
-      simp only [VcbAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, map_eq_zero] at h1
+      simp only [VcbAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, norm_eq_zero] at h1
       exact h1
     apply And.intro
     · have hU1 : [U]ub = VubAbs ⟦V⟧ := by
@@ -333,7 +333,7 @@ lemma cd_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠
   have hx := Vabs_sq_add_neq_zero hb
   field_simp
   have h1 : conj [V]ub = VubAbs ⟦V⟧ * cexp (- arg [V]ub * I) := by
-    nth_rewrite 1 [← abs_mul_exp_arg_mul_I [V]ub]
+    nth_rewrite 1 [← norm_mul_exp_arg_mul_I [V]ub]
     rw [@RingHom.map_mul]
     simp [conj_ofReal, ← exp_conj, VAbs]
   rw [h1]
@@ -353,7 +353,7 @@ lemma cs_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠
   have hx := Vabs_sq_add_neq_zero hb
   field_simp
   have h1 : conj [V]ub = VubAbs ⟦V⟧ * cexp (- arg [V]ub * I) := by
-    nth_rewrite 1 [← abs_mul_exp_arg_mul_I [V]ub]
+    nth_rewrite 1 [← norm_mul_exp_arg_mul_I [V]ub]
     rw [@RingHom.map_mul]
     simp only [Fin.isValue, conj_ofReal, ← exp_conj, _root_.map_mul, conj_I, mul_neg, VubAbs, VAbs,
       VAbs', Quotient.lift_mk, neg_mul]