From 325d7d0c92df9edf460d017730c5fb975d08669d Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 4 Mar 2025 06:32:41 +0000 Subject: [PATCH 1/5] chore: lake update --- README.md | 2 +- lake-manifest.json | 38 +++++++++++++++++++------------------- lakefile.toml | 4 ++-- lean-toolchain | 2 +- 4 files changed, 23 insertions(+), 23 deletions(-) diff --git a/README.md b/README.md index 5f0e26b1..79ef755f 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ [![](https://img.shields.io/badge/Informal_dependencies-Graph-green)](https://heplean.com/InformalGraph) [![](https://img.shields.io/badge/View_The-Stats-blue)](https://heplean.com/Stats) -[![](https://img.shields.io/badge/Lean-v4.16.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.16.0) +[![](https://img.shields.io/badge/Lean-v4.17.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.17.0) [![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/HEPLean/HepLean) A project to digitalize physics. diff --git a/lake-manifest.json b/lake-manifest.json index 513e96ec..8b0c0fea 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,27 +5,27 @@ "type": "git", "subDir": null, "scope": "", - "rev": "af3e1046f897d2f22721413bb095e64849cc76a6", + "rev": "b031cb6aa39c6db80532975c43594f247b8d4b51", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.16.0", + "inputRev": "v4.17.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "a6276f4c6097675b1cf5ebd49b1146b735f38c02", + "rev": "5269898d6a51d047931107c8d72d934d8d5d3753", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.16.0", + "inputRev": "v4.17.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/mhuisi/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "d835296a6149acb9bd2ff65ec01b728b9cc99a1c", + "rev": "c53b3371dd0fe5f3dd75a2df543c3550e246465a", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e86d905bf1453554ea60a853e275bd9de30e0501", + "rev": "d890360c960358a42965bdc15defa3fd09feba38", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,12 +45,12 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9e99cb8cd9ba6906472634e6973c7e27482a70bb", + "rev": "63a4bd4ffa4b67dbd8cf5489a0f01bfdc084602c", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, @@ -65,17 +65,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155", + "rev": "c708be04267e3e995a14ac0d08b1530579c1525a", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.16.0-rc1", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531", + "rev": "0c169a0d55fef3763cfb3099eafd7b884ec7e41d", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1a6613663c3eb08c401ce0fd1a408412f2c2321e", + "rev": "0447b0a7b7f41f0a1749010db3f222e4a96f9d30", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,37 +95,37 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2", + "rev": "799f6986de9f61b784ff7be8f6a8b101045b8ffd", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.50", + "inputRev": "v0.0.52", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "79402ad9ab4be9a2286701a9880697e2351e4955", + "rev": "56a2c80b209c253e0281ac4562a92122b457dcc0", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.16.0-rc1", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32", + "rev": "95561f7a5811fae6a309e4a1bbe22a0a4a98bf03", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "01006c9e86bf9e397c026fef4190478dd1fd897e", + "rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index 0acf410e..323c19ab 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,12 +6,12 @@ defaultTargets = ["PhysLean"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" -rev = "v4.16.0" +rev = "v4.17.0" [[require]] name = "«doc-gen4»" git = "https://github.com/leanprover/doc-gen4" -rev = "v4.16.0" +rev = "v4.17.0" [[lean_lib]] name = "PhysLean" diff --git a/lean-toolchain b/lean-toolchain index 8b4f470c..9d729a35 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.16.0 \ No newline at end of file +leanprover/lean4:v4.17.0 \ No newline at end of file From e0a8cb99a2f084c26638273d843bf4f5d8c40615 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 4 Mar 2025 09:03:36 +0000 Subject: [PATCH 2/5] feat: building --- PhysLean/Mathematics/SO3/Basic.lean | 2 +- PhysLean/Mathematics/SchurTriangulation.lean | 21 ----- PhysLean/Meta/Notes/ToHTML.lean | 4 +- .../BeyondTheStandardModel/TwoHDM/Basic.lean | 6 +- .../FlavorPhysics/CKMMatrix/Basic.lean | 10 +-- .../FlavorPhysics/CKMMatrix/PhaseFreedom.lean | 24 +++--- .../FlavorPhysics/CKMMatrix/Relations.lean | 68 ++++++++------- .../FlavorPhysics/CKMMatrix/Rows.lean | 20 ++--- .../StandardParameterization/Basic.lean | 20 +++-- .../StandardParameters.lean | 62 +++++++------ .../HiggsBoson/PointwiseInnerProd.lean | 3 +- .../PerturbationTheory/CreateAnnihilate.lean | 1 + .../FeynmanDiagrams/Basic.lean | 2 +- .../WickContraction/UncontractedList.lean | 12 +-- .../HarmonicOscillator/Basic.lean | 1 - .../HarmonicOscillator/Completeness.lean | 38 ++++---- .../HarmonicOscillator/Eigenfunction.lean | 8 +- .../OneDimension/HilbertSpace/Basic.lean | 86 +++++++++---------- .../Lorentz/ComplexTensor/Units/Basis.lean | 20 ++--- .../Lorentz/ComplexVector/Metric.lean | 4 +- .../Lorentz/ComplexVector/Unit.lean | 16 ++-- PhysLean/Relativity/Lorentz/Group/Basic.lean | 2 +- PhysLean/Relativity/Lorentz/Group/Proper.lean | 2 +- .../Lorentz/PauliMatrices/AsTensor.lean | 2 +- .../Lorentz/RealVector/Contraction.lean | 9 +- PhysLean/Relativity/Lorentz/SL2C/Basic.lean | 10 +-- PhysLean/Relativity/Lorentz/Weyl/Metric.lean | 8 +- PhysLean/Relativity/Lorentz/Weyl/Unit.lean | 9 +- .../Tensors/OverColor/Discrete.lean | 2 +- .../Relativity/Tensors/OverColor/Lift.lean | 7 +- .../Contractions/Categorical.lean | 12 +-- PhysLean/Relativity/Tensors/Tree/Elab.lean | 34 ++++---- .../Tensors/Tree/NodeIdentities/Basic.lean | 2 - .../Tree/NodeIdentities/ContrContr.lean | 2 +- 34 files changed, 259 insertions(+), 270 deletions(-) diff --git a/PhysLean/Mathematics/SO3/Basic.lean b/PhysLean/Mathematics/SO3/Basic.lean index ddee0ef2..d545dda0 100644 --- a/PhysLean/Mathematics/SO3/Basic.lean +++ b/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. -/ diff --git a/PhysLean/Mathematics/SchurTriangulation.lean b/PhysLean/Mathematics/SchurTriangulation.lean index edb67282..297dbdaf 100644 --- a/PhysLean/Mathematics/SchurTriangulation.lean +++ b/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`. -/ diff --git a/PhysLean/Meta/Notes/ToHTML.lean b/PhysLean/Meta/Notes/ToHTML.lean index bb7bee22..912f49ee 100644 --- a/PhysLean/Meta/Notes/ToHTML.lean +++ b/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 diff --git a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean index 0a9892a9..63ef9dfe 100644 --- a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean +++ b/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] diff --git a/PhysLean/Particles/FlavorPhysics/CKMMatrix/Basic.lean b/PhysLean/Particles/FlavorPhysics/CKMMatrix/Basic.lean index 9db6ff20..c53fbf27 100644 --- a/PhysLean/Particles/FlavorPhysics/CKMMatrix/Basic.lean +++ b/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 → ℝ := diff --git a/PhysLean/Particles/FlavorPhysics/CKMMatrix/PhaseFreedom.lean b/PhysLean/Particles/FlavorPhysics/CKMMatrix/PhaseFreedom.lean index 77c7eb0e..f519d897 100644 --- a/PhysLean/Particles/FlavorPhysics/CKMMatrix/PhaseFreedom.lean +++ b/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,14 +278,14 @@ 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 @@ -293,7 +293,7 @@ lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud 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] diff --git a/PhysLean/Particles/FlavorPhysics/CKMMatrix/Relations.lean b/PhysLean/Particles/FlavorPhysics/CKMMatrix/Relations.lean index 02722c1a..a7d82a7a 100644 --- a/PhysLean/Particles/FlavorPhysics/CKMMatrix/Relations.lean +++ b/PhysLean/Particles/FlavorPhysics/CKMMatrix/Relations.lean @@ -32,38 +32,41 @@ lemma VAbs_sum_sq_row_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) : simp only [mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, Fin.isValue, one_apply_eq] at ht rw [mul_conj, mul_conj, mul_conj] at ht - repeat rw [← Complex.sq_abs] at ht + repeat rw [← Complex.sq_norm] at ht rw [← ofReal_inj] simpa using ht -/-- The absolute value squared of the first row of a CKM matrix is `1`, in terms of `abs`. -/ -lemma fst_row_normalized_abs (V : CKMMatrix) : abs [V]ud ^ 2 + abs [V]us ^ 2 + abs [V]ub ^ 2 = 1 := +/-- The absolute value squared of the first row of a CKM matrix is `1`, in terms of `norm`. -/ +lemma fst_row_normalized_abs (V : CKMMatrix) : + norm [V]ud ^ 2 + norm [V]us ^ 2 + norm [V]ub ^ 2 = 1 := VAbs_sum_sq_row_eq_one ⟦V⟧ 0 -/-- The absolute value squared of the second row of a CKM matrix is `1`, in terms of `abs`. -/ -lemma snd_row_normalized_abs (V : CKMMatrix) : abs [V]cd ^ 2 + abs [V]cs ^ 2 + abs [V]cb ^ 2 = 1 := +/-- The absolute value squared of the second row of a CKM matrix is `1`, in terms of `norm`. -/ +lemma snd_row_normalized_abs (V : CKMMatrix) : + norm [V]cd ^ 2 + norm [V]cs ^ 2 + norm [V]cb ^ 2 = 1 := VAbs_sum_sq_row_eq_one ⟦V⟧ 1 -/-- The absolute value squared of the third row of a CKM matrix is `1`, in terms of `abs`. -/ -lemma thd_row_normalized_abs (V : CKMMatrix) : abs [V]td ^ 2 + abs [V]ts ^ 2 + abs [V]tb ^ 2 = 1 := +/-- The absolute value squared of the third row of a CKM matrix is `1`, in terms of `norm`. -/ +lemma thd_row_normalized_abs (V : CKMMatrix) : + norm [V]td ^ 2 + norm [V]ts ^ 2 + norm [V]tb ^ 2 = 1 := VAbs_sum_sq_row_eq_one ⟦V⟧ 2 /-- The absolute value squared of the first row of a CKM matrix is `1`, in terms of `nomSq`. -/ lemma fst_row_normalized_normSq (V : CKMMatrix) : normSq [V]ud + normSq [V]us + normSq [V]ub = 1 := by - repeat rw [← Complex.sq_abs] + repeat rw [← Complex.sq_norm] exact V.fst_row_normalized_abs /-- The absolute value squared of the second row of a CKM matrix is `1`, in terms of `nomSq`. -/ lemma snd_row_normalized_normSq (V : CKMMatrix) : normSq [V]cd + normSq [V]cs + normSq [V]cb = 1 := by - repeat rw [← Complex.sq_abs] + repeat rw [← Complex.sq_norm] exact V.snd_row_normalized_abs /-- The absolute value squared of the third row of a CKM matrix is `1`, in terms of `nomSq`. -/ lemma thd_row_normalized_normSq (V : CKMMatrix) : normSq [V]td + normSq [V]ts + normSq [V]tb = 1 := by - repeat rw [← Complex.sq_abs] + repeat rw [← Complex.sq_norm] exact V.thd_row_normalized_abs lemma normSq_Vud_plus_normSq_Vus (V : CKMMatrix) : @@ -74,7 +77,7 @@ lemma VudAbs_sq_add_VusAbs_sq : VudAbs V ^ 2 + VusAbs V ^2 = 1 - VubAbs V ^2 := linear_combination VAbs_sum_sq_row_eq_one V 0 lemma ud_us_neq_zero_iff_ub_neq_one (V : CKMMatrix) : - [V]ud ≠ 0 ∨ [V]us ≠ 0 ↔ abs [V]ub ≠ 1 := by + [V]ud ≠ 0 ∨ [V]us ≠ 0 ↔ norm [V]ub ≠ 1 := by have h2 := V.fst_row_normalized_abs refine Iff.intro (fun h h1 => ?_) (fun h => ?_) · rw [h1] at h2 @@ -83,9 +86,9 @@ lemma ud_us_neq_zero_iff_ub_neq_one (V : CKMMatrix) : simp_all · by_contra hn rw [not_or] at hn - simp_all only [ne_eq, Decidable.not_not, map_zero, OfNat.ofNat_ne_zero, not_false_eq_true, + simp_all only [ne_eq, Decidable.not_not, norm_zero, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero, zero_add, sq_eq_one_iff, false_or] - have h1 := Complex.abs.nonneg [V]ub + have h1 := norm_nonneg [V]ub rw [h2] at h1 refine (?_ : ¬ 0 ≤ (-1 : ℝ)) h1 simp @@ -95,13 +98,13 @@ lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℝ {V : CKMMatrix} (hb : [V]ud ≠ 0 rw [normSq_Vud_plus_normSq_Vus V] rw [ud_us_neq_zero_iff_ub_neq_one] at hb by_contra hn - rw [← Complex.sq_abs] at hn - have h2 : Complex.abs (V.1 0 2) ^2 = 1 := by + rw [← Complex.sq_norm] at hn + have h2 : norm (V.1 0 2) ^2 = 1 := by linear_combination -(1 * hn) simp only [Fin.isValue, sq_eq_one_iff] at h2 cases' h2 with h2 h2 · exact hb h2 - · have h3 := Complex.abs.nonneg [V]ub + · have h3 := norm_nonneg [V]ub rw [h2] at h3 have h2 : ¬ 0 ≤ (-1 : ℝ) := by simp exact h2 h3 @@ -112,7 +115,7 @@ lemma VAbsub_neq_zero_Vud_Vus_neq_zero {V : Quotient CKMMatrixSetoid} change VubAbs ⟦V⟧ ≠ 1 at hV simp only [VubAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk] at hV rw [← ud_us_neq_zero_iff_ub_neq_one V] at hV - simpa [← Complex.sq_abs] using (normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hV) + simpa [← Complex.sq_norm] using (normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hV) lemma VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero {V : Quotient CKMMatrixSetoid} (hV : VAbs 0 2 V ≠ 1) : √(VudAbs V ^ 2 + VusAbs V ^ 2) ≠ 0 := by @@ -121,7 +124,7 @@ lemma VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero {V : Quotient CKMMatrixSetoid} change VubAbs ⟦V⟧ ≠ 1 at hV simp only [VubAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk] at hV rw [← ud_us_neq_zero_iff_ub_neq_one V] at hV - simpa [← Complex.sq_abs] using (normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hV) + simpa [← Complex.sq_norm] using (normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hV) lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℂ {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) : (normSq [V]ud : ℂ) + normSq [V]us ≠ 0 := by @@ -133,7 +136,7 @@ lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℂ {V : CKMMatrix} (hb : [V]ud ≠ 0 lemma Vabs_sq_add_neq_zero {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) : ((VudAbs ⟦V⟧ : ℂ) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧)) ≠ 0 := by have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℂ hb - rw [← Complex.sq_abs, ← Complex.sq_abs] at h1 + rw [← Complex.sq_norm, ← Complex.sq_norm] at h1 simp only [Fin.isValue, sq, ofReal_mul, ne_eq] at h1 exact h1 @@ -255,7 +258,7 @@ section individual lemma VAbs_ge_zero (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : 0 ≤ VAbs i j V := by obtain ⟨V, hV⟩ := Quot.exists_rep V rw [← hV] - exact Complex.abs.nonneg _ + exact norm_nonneg _ lemma VAbs_leq_one (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : VAbs i j V ≤ 1 := by have h := VAbs_sum_sq_row_eq_one V i @@ -281,12 +284,12 @@ lemma VAbs_sum_sq_col_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) : simp only [mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, Fin.isValue, one_apply_eq] at ht rw [mul_comm, mul_conj, mul_comm, mul_conj, mul_comm, mul_conj] at ht - repeat rw [← Complex.sq_abs] at ht + repeat rw [← Complex.sq_norm] at ht rw [← ofReal_inj] simpa using ht lemma thd_col_normalized_abs (V : CKMMatrix) : - abs [V]ub ^ 2 + abs [V]cb ^ 2 + abs [V]tb ^ 2 = 1 := by + norm [V]ub ^ 2 + norm [V]cb ^ 2 + norm [V]tb ^ 2 = 1 := by have h1 := VAbs_sum_sq_col_eq_one ⟦V⟧ 2 simp only [VAbs, VAbs', Fin.isValue, Quotient.lift_mk] at h1 exact h1 @@ -294,7 +297,7 @@ lemma thd_col_normalized_abs (V : CKMMatrix) : lemma thd_col_normalized_normSq (V : CKMMatrix) : normSq [V]ub + normSq [V]cb + normSq [V]tb = 1 := by have h1 := V.thd_col_normalized_abs - repeat rw [Complex.sq_abs] at h1 + repeat rw [Complex.sq_norm] at h1 exact h1 lemma cb_eq_zero_of_ud_us_zero {V : CKMMatrix} (h : [V]ud = 0 ∧ [V]us = 0) : @@ -304,10 +307,11 @@ lemma cb_eq_zero_of_ud_us_zero {V : CKMMatrix} (h : [V]ud = 0 ∧ [V]us = 0) : simp only [Fin.isValue, h, map_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero, zero_add] at h1 rw [add_assoc] at h1 - simp only [Fin.isValue, self_eq_add_right] at h1 + simp only [norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, Fin.isValue, + zero_add, add_assoc, self_eq_add_right] at h1 rw [add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)] at h1 simp only [Fin.isValue, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, - map_eq_zero] at h1 + norm_eq_zero] at h1 exact h1.1 lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) : @@ -317,7 +321,7 @@ lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) : rw [Real.sqrt_eq_iff_eq_sq] · simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at ha rw [cb_eq_zero_of_ud_us_zero ha] at h1 - simp only [Fin.isValue, map_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, + simp only [Fin.isValue, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero] at h1 simp only [VcdAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, VcsAbs] rw [← h1] @@ -336,12 +340,12 @@ lemma VcbAbs_sq_add_VtbAbs_sq (V : Quotient CKMMatrixSetoid) : linear_combination (VAbs_sum_sq_col_eq_one V 2) lemma cb_tb_neq_zero_iff_ub_neq_one (V : CKMMatrix) : - [V]cb ≠ 0 ∨ [V]tb ≠ 0 ↔ abs [V]ub ≠ 1 := by + [V]cb ≠ 0 ∨ [V]tb ≠ 0 ↔ norm [V]ub ≠ 1 := by have h2 := V.thd_col_normalized_abs refine Iff.intro (fun h h1 => ?_) (fun h => ?_) · rw [h1] at h2 simp only [one_pow, Fin.isValue] at h2 - have h2 : Complex.abs (V.1 1 2) ^ 2 + Complex.abs (V.1 2 2) ^ 2 = 0 := by + have h2 : norm (V.1 1 2) ^ 2 + norm (V.1 2 2) ^ 2 = 0 := by linear_combination h2 rw [add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)] at h2 simp_all @@ -350,9 +354,13 @@ lemma cb_tb_neq_zero_iff_ub_neq_one (V : CKMMatrix) : simp only [Fin.isValue, ne_eq, Decidable.not_not] at hn simp_all only [map_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero, sq_eq_one_iff, false_or, one_ne_zero] - have h1 := Complex.abs.nonneg [V]ub + simp only [Fin.isValue, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, + add_zero, sq_eq_one_iff] at h2 + simp_all only [false_or] + have h1 := norm_nonneg [V]ub rw [h2] at h1 - have h2 : ¬ 0 ≤ (-1 : ℝ) := by simp + simp only [Left.nonneg_neg_iff] at h1 + have h2 : ¬ 1 ≤ (0 : ℝ) := by simp exact h2 h1 lemma VAbs_fst_col_eq_one_snd_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} diff --git a/PhysLean/Particles/FlavorPhysics/CKMMatrix/Rows.lean b/PhysLean/Particles/FlavorPhysics/CKMMatrix/Rows.lean index 5e9475c0..ab62c302 100644 --- a/PhysLean/Particles/FlavorPhysics/CKMMatrix/Rows.lean +++ b/PhysLean/Particles/FlavorPhysics/CKMMatrix/Rows.lean @@ -223,25 +223,25 @@ lemma cRow_cross_tRow_eq_uRow (V : CKMMatrix) : funext i fin_cases i <;> simp simp only [h3, Fin.isValue, smul_dotProduct, Pi.conj_apply, smul_eq_mul, - uRow_normalized, Fin.isValue, mul_one, mul_conj, ← Complex.sq_abs] at h2 + uRow_normalized, Fin.isValue, mul_one, mul_conj, ← Complex.sq_norm] at h2 simp only [Fin.isValue, ofReal_pow, sq_eq_one_iff, ofReal_eq_one] at h2 cases' h2 with h2 h2 · have hx : [V]u = (g 0)⁻¹ • (conj ([V]c) ×₃ conj ([V]t)) := by rw [← hg, smul_smul, inv_mul_cancel₀, one_smul] by_contra hn simp [hn] at h2 - have hg2 : Complex.abs (g 0)⁻¹ = 1 := by + have hg2 : norm (g 0)⁻¹ = 1 := by simp [@map_inv₀, h2] have hg22 : ∃ (τ : ℝ), (g 0)⁻¹ = Complex.exp (τ * I) := by - rw [← abs_mul_exp_arg_mul_I (g 0)⁻¹, hg2] + rw [← norm_mul_exp_arg_mul_I (g 0)⁻¹, hg2] use arg (g 0)⁻¹ simp obtain ⟨τ, hτ⟩ := hg22 use τ rw [hx, hτ] - · have hx : Complex.abs (g 0) = -1 := by + · have hx : norm (g 0) = -1 := by simp [← ofReal_inj, Fin.isValue, ofReal_neg, ofReal_one, h2] - have h3 := Complex.abs.nonneg (g 0) + have h3 := norm_nonneg (g 0) simp_all only [ofReal_neg, ofReal_one, Left.nonneg_neg_iff] have h4 : (0 : ℝ) < 1 := by norm_num exact False.elim (lt_iff_not_le.mp h4 h3) @@ -268,13 +268,13 @@ lemma uRow_cross_cRow_eq_tRow (V : CKMMatrix) : funext i fin_cases i <;> simp simp only [h3, Fin.isValue, smul_dotProduct, Pi.conj_apply, smul_eq_mul, tRow_normalized, - Fin.isValue, mul_one, mul_conj, ← Complex.sq_abs, ofReal_pow, sq_eq_one_iff, + Fin.isValue, mul_one, mul_conj, ← Complex.sq_norm, ofReal_pow, sq_eq_one_iff, ofReal_eq_one] at h2 cases' h2 with h2 h2 swap - · have hx : Complex.abs (g 2) = -1 := by + · have hx : norm (g 2) = -1 := by simp [h2, ← ofReal_inj, Fin.isValue, ofReal_neg, ofReal_one] - have h3 := Complex.abs.nonneg (g 2) + have h3 := norm_nonneg (g 2) simp_all have h4 : (0 : ℝ) < 1 := by norm_num exact False.elim (lt_iff_not_le.mp h4 h3) @@ -282,10 +282,10 @@ lemma uRow_cross_cRow_eq_tRow (V : CKMMatrix) : rw [← hg, @smul_smul, inv_mul_cancel₀, one_smul] by_contra hn simp [hn] at h2 - have hg2 : Complex.abs (g 2)⁻¹ = 1 := by + have hg2 : norm (g 2)⁻¹ = 1 := by simp [@map_inv₀, h2] have hg22 : ∃ (τ : ℝ), (g 2)⁻¹ = Complex.exp (τ * I) := by - rw [← abs_mul_exp_arg_mul_I (g 2)⁻¹] + rw [← norm_mul_exp_arg_mul_I (g 2)⁻¹] use arg (g 2)⁻¹ simp [hg2] obtain ⟨τ, hτ⟩ := hg22 diff --git a/PhysLean/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/PhysLean/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean index 50d082c6..9cefd6b9 100644 --- a/PhysLean/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean +++ b/PhysLean/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean @@ -175,25 +175,29 @@ lemma VusVubVcdSq_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Rea VusVubVcdSq ⟦standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ = Real.sin θ₁₂ ^ 2 * Real.cos θ₁₃ ^ 2 * Real.sin θ₁₃ ^ 2 * Real.sin θ₂₃ ^ 2 := by simp only [VusVubVcdSq, VusAbs, VAbs, VAbs', Fin.isValue, standParam, standParamAsMatrix, - neg_mul, Quotient.lift_mk, cons_val', cons_val_one, head_cons, - empty_val', cons_val_fin_one, cons_val_zero, _root_.map_mul, VubAbs, cons_val_two, tail_cons, - VcbAbs, VudAbs, Complex.abs_ofReal] + neg_mul, Quotient.lift_mk, cons_val', cons_val_one, head_cons, + empty_val', cons_val_fin_one, cons_val_zero, Complex.norm_mul, VubAbs, cons_val_two, + Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, VcbAbs, VudAbs] by_cases hx : Real.cos θ₁₃ ≠ 0 - · rw [Complex.abs_exp] + · rw [Complex.norm_exp] simp only [neg_re, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero, sub_self, neg_zero, Real.exp_zero, mul_one, _root_.sq_abs] - rw [_root_.abs_of_nonneg h1, _root_.abs_of_nonneg h3, _root_.abs_of_nonneg h2, - _root_.abs_of_nonneg h4] + rw [Complex.norm_of_nonneg h1, Complex.norm_of_nonneg h3, Complex.norm_of_nonneg h2, + Complex.norm_of_nonneg h4] simp only [sq] ring_nf nth_rewrite 2 [Real.sin_sq θ₁₂] ring_nf + have h1 : ‖(Real.sin θ₁₃ : ℂ)‖ ^ 2 = Real.sin θ₁₃ ^ 2 := by + rw [@sq_eq_sq_iff_abs_eq_abs] + rw [Complex.norm_real] + simp + rw [h1] field_simp ring · simp only [ne_eq, Decidable.not_not] at hx rw [hx] - simp only [abs_zero, mul_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, - zero_mul, add_zero, div_zero] + simp open Invariant in lemma mulExpδ₁₃_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂) diff --git a/PhysLean/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean b/PhysLean/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean index ae7c1e7e..35336d7b 100644 --- a/PhysLean/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean +++ b/PhysLean/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean @@ -143,18 +143,21 @@ lemma S₂₃_eq_ℂsin_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.sin ( (ofReal_sin _).symm.trans (congrArg ofReal (S₂₃_eq_sin_θ₂₃ V)) lemma complexAbs_sin_θ₁₂ (V : Quotient CKMMatrixSetoid) : - Complex.abs (Complex.sin (θ₁₂ V)) = sin (θ₁₂ V) := by - rw [S₁₂_eq_ℂsin_θ₁₂, Complex.abs_ofReal, ofReal_inj, abs_eq_self] + norm (Complex.sin (θ₁₂ V)) = sin (θ₁₂ V) := by + rw [S₁₂_eq_ℂsin_θ₁₂, Complex.norm_real, ofReal_inj] + refine Real.norm_of_nonneg ?_ exact S₁₂_nonneg _ lemma complexAbs_sin_θ₁₃ (V : Quotient CKMMatrixSetoid) : - Complex.abs (Complex.sin (θ₁₃ V)) = sin (θ₁₃ V) := by - rw [S₁₃_eq_ℂsin_θ₁₃, Complex.abs_ofReal, ofReal_inj, abs_eq_self] + norm (Complex.sin (θ₁₃ V)) = sin (θ₁₃ V) := by + rw [S₁₃_eq_ℂsin_θ₁₃, Complex.norm_real, ofReal_inj] + refine Real.norm_of_nonneg ?_ exact S₁₃_nonneg _ lemma complexAbs_sin_θ₂₃ (V : Quotient CKMMatrixSetoid) : - Complex.abs (Complex.sin (θ₂₃ V)) = sin (θ₂₃ V) := by - rw [S₂₃_eq_ℂsin_θ₂₃, Complex.abs_ofReal, ofReal_inj, abs_eq_self] + norm (Complex.sin (θ₂₃ V)) = sin (θ₂₃ V) := by + rw [S₂₃_eq_ℂsin_θ₂₃, Complex.norm_real, ofReal_inj] + refine Real.norm_of_nonneg ?_ exact S₂₃_nonneg _ lemma S₁₂_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₁₂ V = 0 := by @@ -185,22 +188,25 @@ lemma C₁₃_eq_ℂcos_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.cos ( lemma C₂₃_eq_ℂcos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₂₃ V) = C₂₃ V := by simp [C₂₃] -lemma complexAbs_cos_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₁₂ V)) = +lemma complexAbs_cos_θ₁₂ (V : Quotient CKMMatrixSetoid) : norm (Complex.cos (θ₁₂ V)) = cos (θ₁₂ V) := by - rw [C₁₂_eq_ℂcos_θ₁₂, Complex.abs_ofReal] - simp only [ofReal_inj, abs_eq_self] + rw [C₁₂_eq_ℂcos_θ₁₂, Complex.norm_real] + simp only [ofReal_inj] + refine Real.norm_of_nonneg ?_ exact Real.cos_arcsin_nonneg _ -lemma complexAbs_cos_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₁₃ V)) = +lemma complexAbs_cos_θ₁₃ (V : Quotient CKMMatrixSetoid) : norm (Complex.cos (θ₁₃ V)) = cos (θ₁₃ V) := by - rw [C₁₃_eq_ℂcos_θ₁₃, Complex.abs_ofReal] - simp only [ofReal_inj, abs_eq_self] + rw [C₁₃_eq_ℂcos_θ₁₃, Complex.norm_real] + simp only [ofReal_inj] + refine Real.norm_of_nonneg ?_ exact Real.cos_arcsin_nonneg _ -lemma complexAbs_cos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₂₃ V)) = +lemma complexAbs_cos_θ₂₃ (V : Quotient CKMMatrixSetoid) : norm (Complex.cos (θ₂₃ V)) = cos (θ₂₃ V) := by - rw [C₂₃_eq_ℂcos_θ₂₃, Complex.abs_ofReal] - simp only [ofReal_inj, abs_eq_self] + rw [C₂₃_eq_ℂcos_θ₂₃, Complex.norm_real] + simp only [ofReal_inj] + refine Real.norm_of_nonneg ?_ exact Real.cos_arcsin_nonneg _ lemma S₁₂_sq_add_C₁₂_sq (V : Quotient CKMMatrixSetoid) : S₁₂ V ^ 2 + C₁₂ V ^ 2 = 1 := by @@ -360,12 +366,12 @@ lemma mulExpδ₁₃_on_param_eq_zero_iff (V : CKMMatrix) (δ₁₃ : ℝ) : aesop lemma mulExpδ₁₃_on_param_abs (V : CKMMatrix) (δ₁₃ : ℝ) : - Complex.abs (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) = + norm (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) = sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧) * cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) := by rw [mulExpδ₁₃_on_param_δ₁₃] - simp only [_root_.map_mul, map_pow, abs_exp, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, - mul_zero, sub_self, Real.exp_zero, mul_one, ofReal_mul, ofReal_pow] + simp only [Complex.norm_mul, norm_pow, norm_exp, mul_re, I_re, ofReal_re, zero_mul, I_im, + ofReal_im, mul_zero, sub_self, Real.exp_zero, mul_one, ofReal_mul, ofReal_pow] rw [complexAbs_sin_θ₁₃, complexAbs_cos_θ₁₃, complexAbs_sin_θ₁₂, complexAbs_cos_θ₁₂, complexAbs_sin_θ₂₃, complexAbs_cos_θ₂₃] @@ -375,15 +381,15 @@ lemma mulExpδ₁₃_on_param_neq_zero_arg (V : CKMMatrix) (δ₁₃ : ℝ) cexp (δ₁₃ * I) := by have h1a := mulExpδ₁₃_on_param_δ₁₃ V δ₁₃ have habs := mulExpδ₁₃_on_param_abs V δ₁₃ - have h2 : mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = Complex.abs + have h2 : mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = norm (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) * exp (δ₁₃ * I) := by rw [habs, h1a] ring_nf - nth_rewrite 1 [← abs_mul_exp_arg_mul_I (mulExpδ₁₃ + nth_rewrite 1 [← norm_mul_exp_arg_mul_I (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧)] at h2 have habs_neq_zero : - (Complex.abs (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) : ℂ) ≠ 0 := by - simp only [ne_eq, ofReal_eq_zero, map_eq_zero] + (norm (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) : ℂ) ≠ 0 := by + simp only [ne_eq, ofReal_eq_zero, norm_eq_zero] exact h1 rw [← mul_right_inj' habs_neq_zero] rw [← h2] @@ -552,8 +558,8 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 Nat.reduceAdd, tail_cons, head_cons, standParam, standParamAsMatrix, ofReal_cos, ofReal_sin, ofReal_neg, mul_neg, neg_mul, neg_neg, cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one] - nth_rewrite 1 [← abs_mul_exp_arg_mul_I (V.1 0 2)] - rw [show Complex.abs (V.1 0 2) = VubAbs ⟦V⟧ from rfl] + nth_rewrite 1 [← norm_mul_exp_arg_mul_I (V.1 0 2)] + rw [show norm (V.1 0 2) = VubAbs ⟦V⟧ from rfl] rw [VubAbs_eq_S₁₃, ← S₁₃_eq_sin_θ₁₃ ⟦V⟧] simp only [ofReal_sin, Fin.isValue, mul_eq_mul_left_iff] ring_nf @@ -599,7 +605,7 @@ lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) : have h1 : VubAbs ⟦V⟧ = 1 := by simp only [VubAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk] rw [hV.2.2.2.1] - exact AbsoluteValue.map_one Complex.abs + exact norm_one refine eq_rows V ?_ ?_ hV.2.2.2.2.1 · funext i fin_cases i @@ -622,7 +628,7 @@ lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) : rw [S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃] simp only [Fin.isValue, VubAbs, VAbs, VAbs', Quotient.lift_mk] rw [hV.2.2.2.1] - simp only [_root_.map_one, ofReal_one] + simp · funext i fin_cases i · simp only [cRow, Fin.isValue, Fin.zero_eta, cons_val_zero, standParam, standParamAsMatrix, @@ -665,7 +671,7 @@ theorem exists_δ₁₃ (V : CKMMatrix) : by_contra hn simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at hn have hna : VudAbs ⟦U⟧ = 0 ∧ VusAbs ⟦U⟧ =0 := by - simp only [VudAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, map_eq_zero, VusAbs] + simp only [VudAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, norm_eq_zero, VusAbs] exact hn rw [hUV] at hna simp only [VudAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, map_eq_zero, VusAbs] at hna @@ -679,7 +685,7 @@ theorem exists_δ₁₃ (V : CKMMatrix) : simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at ha have h1 : VudAbs ⟦U⟧ = 0 ∧ VusAbs ⟦U⟧ = 0 := by rw [hUV] - simp only [VudAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, map_eq_zero, VusAbs] + simp only [VudAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, norm_eq_zero, VusAbs] exact ha simpa [not_or, VAbs] using h1 have ⟨U2, hU2⟩ := ubOnePhaseCond_hold_up_to_equiv_of_ub_one haU hU.2 diff --git a/PhysLean/Particles/StandardModel/HiggsBoson/PointwiseInnerProd.lean b/PhysLean/Particles/StandardModel/HiggsBoson/PointwiseInnerProd.lean index 911c15f6..6d797457 100644 --- a/PhysLean/Particles/StandardModel/HiggsBoson/PointwiseInnerProd.lean +++ b/PhysLean/Particles/StandardModel/HiggsBoson/PointwiseInnerProd.lean @@ -130,8 +130,7 @@ scoped[StandardModel.HiggsField] notation "‖" φ1 "‖_H^2" => normSq φ1 lemma innerProd_self_eq_normSq (φ : HiggsField) (x : SpaceTime) : ⟪φ, φ⟫_H x = ‖φ‖_H^2 x := by erw [normSq, @PiLp.norm_sq_eq_of_L2, Fin.sum_univ_two] - simp only [innerProd, PiLp.inner_apply, RCLike.inner_apply, conj_mul', norm_eq_abs, - Fin.sum_univ_two, ofReal_add, ofReal_pow] + simp [innerProd, conj_mul'] lemma normSq_eq_innerProd_self (φ : HiggsField) (x : SpaceTime) : ‖φ x‖ ^ 2 = (⟪φ, φ⟫_H x).re := by diff --git a/PhysLean/QFT/PerturbationTheory/CreateAnnihilate.lean b/PhysLean/QFT/PerturbationTheory/CreateAnnihilate.lean index 2be5447b..4f66801e 100644 --- a/PhysLean/QFT/PerturbationTheory/CreateAnnihilate.lean +++ b/PhysLean/QFT/PerturbationTheory/CreateAnnihilate.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import Mathlib.Algebra.BigOperators.Group.Finset.Basic +import Mathlib.Data.Fintype.Card /-! # Creation and annihilation parts of fields diff --git a/PhysLean/QFT/PerturbationTheory/FeynmanDiagrams/Basic.lean b/PhysLean/QFT/PerturbationTheory/FeynmanDiagrams/Basic.lean index ddf4c129..11b8d775 100644 --- a/PhysLean/QFT/PerturbationTheory/FeynmanDiagrams/Basic.lean +++ b/PhysLean/QFT/PerturbationTheory/FeynmanDiagrams/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import Mathlib.Tactic.FinCases -import Mathlib.CategoryTheory.Comma.Over +import Mathlib.CategoryTheory.Comma.Over.Basic import Mathlib.CategoryTheory.IsomorphismClasses import Mathlib.Data.Fintype.Perm import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting diff --git a/PhysLean/QFT/PerturbationTheory/WickContraction/UncontractedList.lean b/PhysLean/QFT/PerturbationTheory/WickContraction/UncontractedList.lean index a584a095..b4d7bdf9 100644 --- a/PhysLean/QFT/PerturbationTheory/WickContraction/UncontractedList.lean +++ b/PhysLean/QFT/PerturbationTheory/WickContraction/UncontractedList.lean @@ -99,7 +99,7 @@ lemma fin_list_sorted_split : lemma fin_list_sorted_indexOf_filter_le_mem : (l : List (Fin n)) → (hl : l.Sorted (· ≤ ·)) → (i : Fin n) → (hl : i ∈ l) → - List.indexOf i (List.filter (fun x => decide (↑i ≤ ↑x)) l) = 0 + List.idxOf i (List.filter (fun x => decide (↑i ≤ ↑x)) l) = 0 | [], _, _, _ => by simp | a :: l, hl, i, hi => by simp only [List.sorted_cons] at hl @@ -125,10 +125,10 @@ lemma fin_list_sorted_indexOf_filter_le_mem : lemma fin_list_sorted_indexOf_mem : (l : List (Fin n)) → (hl : l.Sorted (· ≤ ·)) → (i : Fin n) → (hi : i ∈ l) → - l.indexOf i = (l.filter (fun x => x.1 < i.1)).length := by + l.idxOf i = (l.filter (fun x => x.1 < i.1)).length := by intro l hl i hi conv_lhs => rw [fin_list_sorted_split l hl i] - rw [List.indexOf_append_of_not_mem] + rw [List.idxOf_append_of_not_mem] erw [fin_list_sorted_indexOf_filter_le_mem l hl i hi] · simp · simp @@ -275,11 +275,11 @@ lemma filter_uncontractedList (c : WickContraction n) (p : Fin n → Prop) [Deci def uncontractedIndexEquiv (c : WickContraction n) : Fin (c.uncontractedList).length ≃ c.uncontracted where toFun i := ⟨c.uncontractedList.get i, c.uncontractedList_get_mem_uncontracted i⟩ - invFun i := ⟨List.indexOf i.1 c.uncontractedList, - List.indexOf_lt_length_iff.mpr ((c.uncontractedList_mem_iff i.1).mpr i.2)⟩ + invFun i := ⟨List.idxOf i.1 c.uncontractedList, + List.idxOf_lt_length_iff.mpr ((c.uncontractedList_mem_iff i.1).mpr i.2)⟩ left_inv i := by ext - exact List.get_indexOf (uncontractedList_nodup c) _ + exact List.get_idxOf (uncontractedList_nodup c) _ right_inv i := by ext simp diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean index 7e00f5ac..3d800c23 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean @@ -72,7 +72,6 @@ structure HarmonicOscillator where namespace HarmonicOscillator -open Nat open PhysLean HilbertSpace open MeasureTheory diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean index cbc747bd..b28ed4f0 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean @@ -303,7 +303,7 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) apply Filter.Tendsto.mul_const simp only [Complex.exp, Complex.exp'] haveI hi : CauSeq.IsComplete ℂ norm := - inferInstanceAs (CauSeq.IsComplete ℂ Complex.abs) + inferInstanceAs (CauSeq.IsComplete ℂ norm) exact CauSeq.tendsto_limit (Complex.exp' (Complex.I * c * y)) /- End of rewritting the intergrand as a limit. -/ /- Rewritting the integral as a limit using dominated_convergence -/ @@ -311,7 +311,7 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) (Complex.I * ↑c * ↑y) ^ r / r ! * (f y * Real.exp (- y^2 / (2 * Q.ξ^2)))) Filter.atTop (nhds (∫ y : ℝ, Complex.exp (Complex.I * c * y) * (f y * Real.exp (- y^2 / (2 * Q.ξ^2))))) := by - let bound : ℝ → ℝ := fun x => Real.exp (|c * x|) * Complex.abs (f x) * + let bound : ℝ → ℝ := fun x => Real.exp (|c * x|) * norm (f x) * (Real.exp (- x ^ 2 / (2 * Q.ξ^2))) apply MeasureTheory.tendsto_integral_of_dominated_convergence bound · intro n @@ -344,7 +344,7 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) apply guassian_integrable_polynomial simp · /- Prove the bound is integrable. -/ - have hbound : bound = (fun x => Real.exp |c * x| * Complex.abs (f x) * + have hbound : bound = (fun x => Real.exp |c * x| * norm (f x) * Real.exp (-(1/ (2 * Q.ξ^2)) * x ^ 2)) := by simp only [neg_mul, bound] funext x @@ -359,40 +359,40 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) intro y rw [← Finset.sum_mul] simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg, - Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat, norm_mul, Complex.norm_eq_abs, + Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat, norm_mul, bound] rw [mul_assoc] conv_rhs => rw [mul_assoc] - have h1 : (Complex.abs (f y) * Complex.abs (Complex.exp (-(↑y ^ 2) / (2 * Q.ξ^2)))) - = Complex.abs (f y) * Real.exp (-(y ^ 2) / (2 * Q.ξ^2)) := by + have h1 : (norm (f y) * norm (Complex.exp (-(↑y ^ 2) / (2 * Q.ξ^2)))) + = norm (f y) * Real.exp (-(y ^ 2) / (2 * Q.ξ^2)) := by simp only [mul_eq_mul_left_iff, map_eq_zero, bound] left - rw [Complex.abs_exp] + rw [Complex.norm_exp] congr trans (Complex.ofReal (- y ^ 2 / (2 * Q.ξ^2))).re · congr simp · rw [Complex.ofReal_re] rw [h1] - by_cases hf : Complex.abs (f y) = 0 + by_cases hf : norm (f y) = 0 · simp [hf] rw [_root_.mul_le_mul_right] · have h1 := Real.sum_le_exp_of_nonneg (x := |c * y|) (abs_nonneg (c * y)) n refine le_trans ?_ h1 - have h2 : Complex.abs (∑ i ∈ range n, (Complex.I * (↑c * ↑y)) ^ i / ↑i !) ≤ - ∑ i ∈ range n, Complex.abs ((Complex.I * (↑c * ↑y)) ^ i / ↑i !) := by - exact AbsoluteValue.sum_le _ _ _ + have h2 : norm (∑ i ∈ range n, (Complex.I * (↑c * ↑y)) ^ i / ↑i !) ≤ + ∑ i ∈ range n, norm ((Complex.I * (↑c * ↑y)) ^ i / ↑i !) := by + exact norm_sum_le _ _ refine le_trans h2 ?_ apply le_of_eq congr funext i - simp only [map_div₀, AbsoluteValue.map_pow, AbsoluteValue.map_mul, Complex.abs_I, - Complex.abs_ofReal, one_mul, Complex.abs_natCast, bound] + simp only [Complex.norm_div, norm_pow, Complex.norm_mul, Complex.norm_I, Complex.norm_real, + Real.norm_eq_abs, one_mul, RCLike.norm_natCast, bound] congr rw [abs_mul] · refine mul_pos ?_ ?_ - have h1 : 0 ≤ Complex.abs (f y) := by exact AbsoluteValue.nonneg Complex.abs (f y) + have h1 : 0 ≤ norm (f y) := norm_nonneg (f y) apply lt_of_le_of_ne h1 (fun a => hf (id (Eq.symm a))) exact Real.exp_pos (- y ^ 2 / (2 * Q.ξ^2)) · apply Filter.Eventually.of_forall @@ -463,7 +463,7 @@ lemma fourierIntegral_zero_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) lemma zero_of_orthogonal_mk (f : ℝ → ℂ) (hf : MemHS f) (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0) - (plancherel_theorem: ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : Memℒp f 2), + (plancherel_theorem: ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : MemLp f 2), eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume) : HilbertSpace.mk hf = 0 := by have hf' : (fun x => f x * ↑(rexp (- x ^ 2 / (2 * Q.ξ^2)))) @@ -480,7 +480,7 @@ lemma zero_of_orthogonal_mk (f : ℝ → ℂ) (hf : MemHS f) simp only [eLpNorm_zero] · /- f x * Real.exp (- x^2 / (2 * ξ^2)) is integrable -/ rw [hf'] - rw [← memℒp_one_iff_integrable] + rw [← memLp_one_iff_integrable] apply HilbertSpace.mul_gaussian_mem_Lp_one f hf (1/ (2 * Q.ξ^2)) 0 simp · /- f x * Real.exp (- x^2 / (2 * ξ^2)) is square-integrable -/ @@ -500,7 +500,7 @@ lemma zero_of_orthogonal_mk (f : ℝ → ℂ) (hf : MemHS f) · /- f x * Real.exp (- x^2 / (2 * ξ^2)) is strongly measurable -/ rw [hf'] apply Integrable.aestronglyMeasurable - rw [← memℒp_one_iff_integrable] + rw [← memLp_one_iff_integrable] apply HilbertSpace.mul_gaussian_mem_Lp_one f hf (1/ (2 * Q.ξ^2)) 0 simp · simp @@ -509,7 +509,7 @@ lemma zero_of_orthogonal_mk (f : ℝ → ℂ) (hf : MemHS f) lemma zero_of_orthogonal_eigenVector (f : HilbertSpace) (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), f⟫_ℂ = 0) - (plancherel_theorem: ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : Memℒp f 2), + (plancherel_theorem: ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : MemLp f 2), eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume) : f = 0 := by obtain ⟨f, hf, rfl⟩ := HilbertSpace.mk_surjective f exact zero_of_orthogonal_mk Q f hf hOrth plancherel_theorem @@ -527,7 +527,7 @@ lemma zero_of_orthogonal_eigenVector (f : HilbertSpace) is zero for `f` orthogonal to all eigenfunctions, and hence the norm of `f` is zero. -/ theorem eigenfunction_completeness - (plancherel_theorem : ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : Memℒp f 2), + (plancherel_theorem : ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : MemLp f 2), eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume) : (Submodule.span ℂ (Set.range (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n)))).topologicalClosure = ⊤ := by diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean index 9f592893..09ef79e6 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean @@ -89,15 +89,15 @@ lemma eigenfunction_point_norm (n : ℕ) (x : ℝ) : ‖Q.eigenfunction n x‖ = (1/√(2 ^ n * n !) * (1/ √(√Real.pi * Q.ξ))) * (|physHermite n (x / Q.ξ)| * Real.exp (- x ^ 2 / (2 * Q.ξ ^ 2))) := by rw [eigenfunction_eq] - simp only [neg_mul, Complex.ofReal_mul, Complex.norm_eq_abs] - rw [AbsoluteValue.map_mul, AbsoluteValue.map_mul] + simp only [neg_mul, Complex.ofReal_mul] + rw [norm_mul, norm_mul] congr · simp [Real.sqrt_nonneg, abs_of_nonneg] · simp [Real.sqrt_nonneg, abs_of_nonneg] - · rw [AbsoluteValue.map_mul] + · rw [norm_mul] congr 1 · simp - · rw [Complex.abs_ofReal] + · rw [Complex.norm_real] simp [abs_of_nonneg] lemma eigenfunction_point_norm_sq (n : ℕ) (x : ℝ) : diff --git a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean index 4dd56e8d..cf4716a3 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean @@ -33,7 +33,7 @@ open MeasureTheory /-- The proposition `MemHS f` for a function `f : ℝ → ℂ` is defined to be true if the function `f` can be lifted to the Hilbert space. -/ -def MemHS (f : ℝ → ℂ) : Prop := Memℒp f 2 MeasureTheory.volume +def MemHS (f : ℝ → ℂ) : Prop := MemLp f 2 MeasureTheory.volume lemma aeStronglyMeasurable_of_memHS {f : ℝ → ℂ} (h : MemHS f) : AEStronglyMeasurable f := by @@ -44,24 +44,24 @@ lemma aeStronglyMeasurable_of_memHS {f : ℝ → ℂ} (h : MemHS f) : lemma memHS_iff {f : ℝ → ℂ} : MemHS f ↔ AEStronglyMeasurable f ∧ Integrable (fun x => ‖f x‖ ^ 2) := by rw [MemHS] - simp only [Memℒp, Complex.norm_eq_abs, and_congr_right_iff] + simp [MemLp, and_congr_right_iff] intro h1 - rw [MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top + rw [MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (Ne.symm (NeZero.ne' 2)) ENNReal.ofNat_ne_top] simp only [ENNReal.toReal_ofNat, ENNReal.rpow_ofNat, Integrable] have h0 : MeasureTheory.AEStronglyMeasurable - (fun x => Complex.abs (f x) ^ 2) MeasureTheory.volume := by + (fun x => norm (f x) ^ 2) MeasureTheory.volume := by apply MeasureTheory.AEStronglyMeasurable.pow - exact Continuous.comp_aestronglyMeasurable Complex.continuous_abs h1 + exact Continuous.comp_aestronglyMeasurable continuous_norm h1 simp only [h0, true_and] simp only [HasFiniteIntegral, enorm_pow] - simp only [enorm, nnnorm, Complex.norm_eq_abs, Real.norm_eq_abs, Complex.abs_abs] + simp only [enorm, nnnorm, Real.norm_eq_abs, abs_norm] lemma aeEqFun_mk_mem_iff (f : ℝ → ℂ) (hf : AEStronglyMeasurable f volume) : AEEqFun.mk f hf ∈ HilbertSpace ↔ MemHS f := by rw [MemHS, HilbertSpace] - rw [MeasureTheory.Lp.mem_Lp_iff_memℒp] - apply MeasureTheory.memℒp_congr_ae + rw [MeasureTheory.Lp.mem_Lp_iff_memLp] + apply MeasureTheory.memLp_congr_ae exact AEEqFun.coeFn_mk f hf /-- Given a function `f : ℝ → ℂ` such that `MemHS f` is true via `hf`, then `HilbertSpace.mk hf` @@ -103,23 +103,23 @@ lemma mem_iff' {f : ℝ → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f Meas MeasureTheory.AEEqFun.mk f hf ∈ HilbertSpace ↔ MeasureTheory.Integrable (fun x => ‖f x‖ ^ 2) := by rw [HilbertSpace] - rw [MeasureTheory.Lp.mem_Lp_iff_memℒp] - simp only [Memℒp, eLpNorm_aeeqFun, Complex.norm_eq_abs] + rw [MeasureTheory.Lp.mem_Lp_iff_memLp] + simp only [MemLp, eLpNorm_aeeqFun] have h1 : MeasureTheory.AEStronglyMeasurable (MeasureTheory.AEEqFun.mk f hf) MeasureTheory.volume := by apply MeasureTheory.AEEqFun.aestronglyMeasurable simp only [h1, true_and] - rw [MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top (Ne.symm (NeZero.ne' 2)) + rw [MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (Ne.symm (NeZero.ne' 2)) ENNReal.ofNat_ne_top] simp only [ENNReal.toReal_ofNat, ENNReal.rpow_ofNat, Integrable] have h0 : MeasureTheory.AEStronglyMeasurable - (fun x => Complex.abs (f x) ^ 2) MeasureTheory.volume := by + (fun x => norm (f x) ^ 2) MeasureTheory.volume := by apply MeasureTheory.AEStronglyMeasurable.pow refine Continuous.comp_aestronglyMeasurable ?_ hf - exact Complex.continuous_abs + exact continuous_norm simp only [h0, true_and] simp only [HasFiniteIntegral, enorm_pow] - simp only [enorm, nnnorm, Complex.norm_eq_abs, Real.norm_eq_abs, Complex.abs_abs] + simp only [enorm, nnnorm, norm_norm] /-! @@ -149,7 +149,7 @@ lemma gaussian_memHS {b : ℝ} (c : ℝ) (hb : 0 < b) : apply And.intro · exact gaussian_aestronglyMeasurable c hb simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_neg, Complex.ofReal_mul, - Complex.ofReal_pow, Complex.ofReal_sub, Complex.norm_eq_abs, Complex.abs_exp, Complex.neg_re, + Complex.ofReal_pow, Complex.ofReal_sub, Complex.norm_exp, Complex.neg_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero] have h1 : (fun (x : ℝ) => Real.exp (-(b * ((x - c : ℂ) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (- (2 * b) * x ^ 2)) (y - c) := by @@ -216,8 +216,8 @@ lemma exp_abs_mul_gaussian_integrable (b c : ℝ) (hb : 0 < b) : rw [abs_of_nonneg hx] lemma mul_gaussian_mem_Lp_one (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : - MeasureTheory.Memℒp (fun x => f x * Real.exp (- b * (x - c) ^ 2)) 1 volume := by - refine memℒp_one_iff_integrable.mpr ?_ + MeasureTheory.MemLp (fun x => f x * Real.exp (- b * (x - c) ^ 2)) 1 volume := by + refine memLp_one_iff_integrable.mpr ?_ let g : HilbertSpace := mk (gaussian_memHS c hb) have h1 := MeasureTheory.L2.integrable_inner (𝕜 := ℂ) g (mk hf) refine (integrable_congr ?_).mp h1 @@ -239,50 +239,48 @@ lemma mul_gaussian_mem_Lp_one (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : simp lemma mul_gaussian_mem_Lp_two (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : - MeasureTheory.Memℒp (fun x => f x * Real.exp (- b * (x - c) ^ 2)) 2 volume := by - apply MeasureTheory.Memℒp.mul_of_top_left (p := 2) - · apply MeasureTheory.memℒp_top_of_bound (C := Real.exp (0)) + MeasureTheory.MemLp (fun x => f x * Real.exp (- b * (x - c) ^ 2)) 2 volume := by + refine MeasureTheory.MemLp.mul ?_ hf (q := ⊤) + · apply MeasureTheory.memLp_top_of_bound (C := Real.exp (0)) · exact gaussian_aestronglyMeasurable c hb · apply Filter.Eventually.of_forall intro x - simp only [neg_mul, Complex.norm_eq_abs, zero_sub, even_two, Even.neg_pow] - rw [Complex.abs_ofReal] - rw [abs_of_nonneg] - · simp only [Real.exp_zero, Real.exp_le_one_iff, Left.neg_nonpos_iff] - apply mul_nonneg - · exact le_of_lt hb - · exact sq_nonneg (x - c) - · exact Real.exp_nonneg (-(b * (x - c) ^ 2)) - · exact hf + simp only [neg_mul, zero_sub, even_two, Even.neg_pow] + rw [Complex.norm_real] + simp only [Real.norm_eq_abs, Real.abs_exp, Real.exp_zero, Real.exp_le_one_iff, + Left.neg_nonpos_iff] + apply mul_nonneg + · exact le_of_lt hb + · exact sq_nonneg (x - c) lemma abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : - MeasureTheory.Integrable (fun x => Complex.abs (f x) * Real.exp (- b * (x - c)^2)) := by - have h1 : (fun x => Complex.abs (f x) * Real.exp (- b * (x - c)^2)) = - (fun x => Complex.abs (f x * Real.exp (- b *(x - c)^2))) := by + MeasureTheory.Integrable (fun x => norm (f x) * Real.exp (- b * (x - c)^2)) := by + have h1 : (fun x => norm (f x) * Real.exp (- b * (x - c)^2)) = + (fun x => norm (f x * Real.exp (- b *(x - c)^2))) := by funext x simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_neg, Complex.ofReal_mul, - Complex.ofReal_pow, Complex.ofReal_sub, AbsoluteValue.map_mul, Complex.abs_exp, - Complex.neg_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero, - mul_eq_mul_left_iff, Real.exp_eq_exp, neg_inj, map_eq_zero] + Complex.ofReal_pow, Complex.ofReal_sub, Complex.norm_mul, Complex.norm_exp, Complex.neg_re, + Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero, mul_eq_mul_left_iff, + Real.exp_eq_exp, neg_inj, norm_eq_zero] left left rw [← Complex.ofReal_sub, ← Complex.ofReal_pow] rw [Complex.ofReal_re] rw [h1] - have h2 : MeasureTheory.Memℒp (fun x => f x * Real.exp (- b * (x- c)^2)) 1 volume := by + have h2 : MeasureTheory.MemLp (fun x => f x * Real.exp (- b * (x- c)^2)) 1 volume := by exact mul_gaussian_mem_Lp_one f hf b c hb - simpa using MeasureTheory.Memℒp.integrable_norm_rpow h2 (by simp) (by simp) + simpa using MeasureTheory.MemLp.integrable_norm_rpow h2 (by simp) (by simp) lemma exp_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : MeasureTheory.Integrable - (fun x => Real.exp (c * x) * Complex.abs (f x) * Real.exp (- b * x ^ 2)) := by + (fun x => Real.exp (c * x) * norm (f x) * Real.exp (- b * x ^ 2)) := by have h1 : (fun x => Real.exp (c * x) * - Complex.abs (f x) * Real.exp (- b * x ^ 2)) + norm (f x) * Real.exp (- b * x ^ 2)) = (fun x => Real.exp (c^2 /(4 * b)) * - (Complex.abs (f x) * Real.exp (- b * (x - c/(2 * b)) ^ 2))) := by + (norm (f x) * Real.exp (- b * (x - c/(2 * b)) ^ 2))) := by funext x rw [mul_comm,← mul_assoc] - trans (Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)) * Complex.abs (f x) + trans (Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)) * norm (f x) swap · ring rw [← Real.exp_add, ← Real.exp_add] @@ -295,13 +293,13 @@ lemma exp_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) lemma exp_abs_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : MeasureTheory.Integrable - (fun x => Real.exp (|c * x|) * Complex.abs (f x) * Real.exp (- b * x ^ 2)) := by + (fun x => Real.exp (|c * x|) * norm (f x) * Real.exp (- b * x ^ 2)) := by rw [← MeasureTheory.integrableOn_univ] have h1 : Set.univ (α := ℝ) = (Set.Iic 0) ∪ Set.Ici 0 := by exact Eq.symm Set.Iic_union_Ici rw [h1] apply MeasureTheory.IntegrableOn.union - · let g := fun x => Real.exp ((- |c|) * x) * Complex.abs (f x) * Real.exp (- b * x ^ 2) + · let g := fun x => Real.exp ((- |c|) * x) * norm (f x) * Real.exp (- b * x ^ 2) rw [integrableOn_congr_fun (g := g) _ measurableSet_Iic] · apply MeasureTheory.IntegrableOn.left_of_union (t := Set.Ici 0) rw [← h1, MeasureTheory.integrableOn_univ] @@ -314,7 +312,7 @@ lemma exp_abs_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) ( rw [abs_mul] rw [abs_of_nonpos hx] ring - · let g := fun x => Real.exp (|c| * x) * Complex.abs (f x) * Real.exp (- b * x ^ 2) + · let g := fun x => Real.exp (|c| * x) * norm (f x) * Real.exp (- b * x ^ 2) rw [integrableOn_congr_fun (g := g) _ measurableSet_Ici] · apply MeasureTheory.IntegrableOn.right_of_union (s := Set.Iic 0) rw [← h1, MeasureTheory.integrableOn_univ] diff --git a/PhysLean/Relativity/Lorentz/ComplexTensor/Units/Basis.lean b/PhysLean/Relativity/Lorentz/ComplexTensor/Units/Basis.lean index 9678e5d9..d1c18146 100644 --- a/PhysLean/Relativity/Lorentz/ComplexTensor/Units/Basis.lean +++ b/PhysLean/Relativity/Lorentz/ComplexTensor/Units/Basis.lean @@ -38,12 +38,12 @@ lemma coContrUnit_tensorBasis : coContrUnit = @OfNat.ofNat (Fin 4) n Fin.instOfNat := by rfl have hI2 : @DFunLike.coe (Basis (Fin 4) ℂ ↑Lorentz.complexCo.V) (Fin 4) (fun x => ↑Lorentz.complexCo.V) Basis.instFunLike - = @DFunLike.coe (Basis (Fin 4) ℂ (CoeSort.coe Lorentz.complexCo)) (Fin 4) - (fun x => CoeSort.coe Lorentz.complexCo) Basis.instFunLike := by rfl + = @DFunLike.coe (Basis (Fin 4) ℂ (Lorentz.complexCo)) (Fin 4) + (fun x => Lorentz.complexCo) Basis.instFunLike := by rfl have hI3 : @DFunLike.coe (Basis (Fin 4) ℂ ↑Lorentz.complexContr.V) (Fin 4) (fun x => ↑Lorentz.complexContr.V) Basis.instFunLike - = @DFunLike.coe (Basis (Fin 4) ℂ (CoeSort.coe Lorentz.complexContr)) (Fin 4) - (fun x => CoeSort.coe Lorentz.complexContr) Basis.instFunLike := by rfl + = @DFunLike.coe (Basis (Fin 4) ℂ (Lorentz.complexContr)) (Fin 4) + (fun x => Lorentz.complexContr) Basis.instFunLike := by rfl have hI4 : @OfNat.ofNat complexLorentzTensor.k 1 One.toOfNat1 = @OfNat.ofNat ℂ 1 One.toOfNat1 := by rfl trans {δ' | μ ν}ᵀ.tensor @@ -86,12 +86,12 @@ lemma contrCoUnit_tensorBasis : contrCoUnit = @OfNat.ofNat (Fin 4) n Fin.instOfNat := by rfl have hI2 : @DFunLike.coe (Basis (Fin 4) ℂ ↑Lorentz.complexCo.V) (Fin 4) (fun x => ↑Lorentz.complexCo.V) Basis.instFunLike - = @DFunLike.coe (Basis (Fin 4) ℂ (CoeSort.coe Lorentz.complexCo)) (Fin 4) - (fun x => CoeSort.coe Lorentz.complexCo) Basis.instFunLike := by rfl + = @DFunLike.coe (Basis (Fin 4) ℂ (Lorentz.complexCo)) (Fin 4) + (fun x => Lorentz.complexCo) Basis.instFunLike := by rfl have hI3 : @DFunLike.coe (Basis (Fin 4) ℂ ↑Lorentz.complexContr.V) (Fin 4) (fun x => ↑Lorentz.complexContr.V) Basis.instFunLike - = @DFunLike.coe (Basis (Fin 4) ℂ (CoeSort.coe Lorentz.complexContr)) (Fin 4) - (fun x => CoeSort.coe Lorentz.complexContr) Basis.instFunLike := by rfl + = @DFunLike.coe (Basis (Fin 4) ℂ (Lorentz.complexContr)) (Fin 4) + (fun x => Lorentz.complexContr) Basis.instFunLike := by rfl have hI4 : @OfNat.ofNat complexLorentzTensor.k 1 One.toOfNat1 = @OfNat.ofNat ℂ 1 One.toOfNat1 := by rfl trans {δ | μ ν}ᵀ.tensor @@ -143,7 +143,6 @@ lemma altLeftLeftUnit_tensorBasis : altLeftLeftUnit = · simp only [complexLorentzTensor, Discrete.functor_obj_eq_as, Monoidal.tensorUnit_obj, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom, cons_val_zero, Fin.cases_zero] - rfl · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.mk_one, Fin.isValue, OverColor.mk_hom, cons_val_one, head_cons] rfl @@ -168,7 +167,6 @@ lemma leftAltLeftUnit_tensorBasis : leftAltLeftUnit = · simp only [complexLorentzTensor, Discrete.functor_obj_eq_as, Monoidal.tensorUnit_obj, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom, cons_val_zero, Fin.cases_zero] - rfl · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.mk_one, Fin.isValue, OverColor.mk_hom, cons_val_one, head_cons] rfl @@ -193,7 +191,6 @@ lemma altRightRightUnit_tensorBasis : altRightRightUnit = · simp only [complexLorentzTensor, Discrete.functor_obj_eq_as, Monoidal.tensorUnit_obj, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom, cons_val_zero, Fin.cases_zero] - rfl · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.mk_one, Fin.isValue, OverColor.mk_hom, cons_val_one, head_cons] rfl @@ -218,7 +215,6 @@ lemma rightAltRightUnit_tensorBasis : rightAltRightUnit = · simp only [complexLorentzTensor, Discrete.functor_obj_eq_as, Monoidal.tensorUnit_obj, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom, cons_val_zero, Fin.cases_zero] - rfl · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.mk_one, Fin.isValue, OverColor.mk_hom, cons_val_one, head_cons] rfl diff --git a/PhysLean/Relativity/Lorentz/ComplexVector/Metric.lean b/PhysLean/Relativity/Lorentz/ComplexVector/Metric.lean index aecbe47f..5267688f 100644 --- a/PhysLean/Relativity/Lorentz/ComplexVector/Metric.lean +++ b/PhysLean/Relativity/Lorentz/ComplexVector/Metric.lean @@ -55,7 +55,7 @@ def contrMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr wh refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • contrMetricVal = (TensorProduct.map (complexContr.ρ M) (complexContr.ρ M)) (x • contrMetricVal) @@ -107,7 +107,7 @@ def coMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo where refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • coMetricVal = (TensorProduct.map (complexCo.ρ M) (complexCo.ρ M)) (x • coMetricVal) diff --git a/PhysLean/Relativity/Lorentz/ComplexVector/Unit.lean b/PhysLean/Relativity/Lorentz/ComplexVector/Unit.lean index f7e8c101..c35d7125 100644 --- a/PhysLean/Relativity/Lorentz/ComplexVector/Unit.lean +++ b/PhysLean/Relativity/Lorentz/ComplexVector/Unit.lean @@ -54,7 +54,7 @@ def contrCoUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo where refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • contrCoUnitVal = (TensorProduct.map (complexContr.ρ M) (complexCo.ρ M)) (x • contrCoUnitVal) @@ -104,7 +104,7 @@ def coContrUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr where refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • coContrUnitVal = (TensorProduct.map (complexCo.ρ M) (complexContr.ρ M)) (x • coContrUnitVal) @@ -143,11 +143,11 @@ lemma contr_contrCoUnit (x : complexCo) : Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add, _root_.map_smul] - have h1' (x y : CoeSort.coe complexCo) (z : CoeSort.coe complexContr) : + have h1' (x y : complexCo.V) (z : complexContr.V) : (α_ complexCo.V complexContr.V complexCo.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl repeat rw [h1'] - have h1'' (y : CoeSort.coe complexCo) - (z : CoeSort.coe complexCo ⊗[ℂ] CoeSort.coe complexContr) : + have h1'' (y : complexCo.V) + (z : complexCo.V ⊗[ℂ] complexContr.V) : (coContrContraction.hom ▷ complexCo.V) (z ⊗ₜ[ℂ] y) = (coContrContraction.hom z) ⊗ₜ[ℂ] y := rfl repeat rw (config := { transparency := .instances }) [h1''] repeat rw [coContrContraction_basis'] @@ -177,12 +177,12 @@ lemma contr_coContrUnit (x : complexContr) : Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add, _root_.map_smul] - have h1' (x y : CoeSort.coe complexContr) (z : CoeSort.coe complexCo) : + have h1' (x y : complexContr.V) (z : complexCo.V) : (α_ complexContr.V complexCo.V complexContr.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl repeat rw [h1'] - have h1'' (y : CoeSort.coe complexContr) - (z : CoeSort.coe complexContr ⊗[ℂ] CoeSort.coe complexCo) : + have h1'' (y : complexContr.V) + (z : complexContr.V ⊗[ℂ] complexCo.V) : (contrCoContraction.hom ▷ complexContr.V) (z ⊗ₜ[ℂ] y) = (contrCoContraction.hom z) ⊗ₜ[ℂ] y := rfl repeat rw (config := { transparency := .instances }) [h1''] diff --git a/PhysLean/Relativity/Lorentz/Group/Basic.lean b/PhysLean/Relativity/Lorentz/Group/Basic.lean index 42750e58..26dde2f2 100644 --- a/PhysLean/Relativity/Lorentz/Group/Basic.lean +++ b/PhysLean/Relativity/Lorentz/Group/Basic.lean @@ -262,7 +262,7 @@ lemma toGL_embedding : IsEmbedding (@toGL d).toFun where /-- The embedding of the Lorentz group into `GL(n, ℝ)` gives `LorentzGroup d` an instance of a topological group. -/ -instance : TopologicalGroup (LorentzGroup d) := +instance : IsTopologicalGroup (LorentzGroup d) := IsInducing.topologicalGroup toGL toGL_embedding.toIsInducing /-! diff --git a/PhysLean/Relativity/Lorentz/Group/Proper.lean b/PhysLean/Relativity/Lorentz/Group/Proper.lean index d0b56125..8428cd18 100644 --- a/PhysLean/Relativity/Lorentz/Group/Proper.lean +++ b/PhysLean/Relativity/Lorentz/Group/Proper.lean @@ -41,7 +41,7 @@ instance : DiscreteTopology ℤ₂ := by exact forall_open_iff_discrete.mp fun _ => trivial /-- The instance of a topological group on `ℤ₂` defined via the discrete topology. -/ -instance : TopologicalGroup ℤ₂ := TopologicalGroup.mk +instance : IsTopologicalGroup ℤ₂ := IsTopologicalGroup.mk /-- A continuous function from `({-1, 1} : Set ℝ)` to `ℤ₂`. -/ @[simps!] diff --git a/PhysLean/Relativity/Lorentz/PauliMatrices/AsTensor.lean b/PhysLean/Relativity/Lorentz/PauliMatrices/AsTensor.lean index c8343cc7..a3fd0d99 100644 --- a/PhysLean/Relativity/Lorentz/PauliMatrices/AsTensor.lean +++ b/PhysLean/Relativity/Lorentz/PauliMatrices/AsTensor.lean @@ -114,7 +114,7 @@ def asConsTensor : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗ refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • asTensor = (TensorProduct.map (complexContr.ρ M) diff --git a/PhysLean/Relativity/Lorentz/RealVector/Contraction.lean b/PhysLean/Relativity/Lorentz/RealVector/Contraction.lean index 611eeeda..900f07c3 100644 --- a/PhysLean/Relativity/Lorentz/RealVector/Contraction.lean +++ b/PhysLean/Relativity/Lorentz/RealVector/Contraction.lean @@ -84,7 +84,7 @@ def contrCoContract : Contr d ⊗ Co d ⟶ 𝟙_ (Rep ℝ (LorentzGroup d)) wher simp only [one_mulVec, CategoryTheory.Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V, - Action.tensorUnit_ρ', CategoryTheory.Category.comp_id, lift.tmul] + Action.tensorUnit_ρ, CategoryTheory.Category.comp_id, lift.tmul] rfl /-- Notation for `contrCoContract` acting on a tmul. -/ @@ -107,7 +107,7 @@ def coContrContract : Co d ⊗ Contr d ⟶ 𝟙_ (Rep ℝ (LorentzGroup d)) wher simp only [vecMul_one, CategoryTheory.Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V, - Action.tensorUnit_ρ', CategoryTheory.Category.comp_id, lift.tmul] + Action.tensorUnit_ρ, CategoryTheory.Category.comp_id, lift.tmul] rfl /-- Notation for `coContrContract` acting on a tmul. -/ @@ -331,15 +331,16 @@ lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔ simp only [map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply] at hp hn rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] at hp hn let e : 𝟙_ (Rep ℝ ↑(LorentzGroup d)) ≃ₗ[ℝ] ℝ := - LinearEquiv.refl ℝ (CoeSort.coe (𝟙_ (Rep ℝ ↑(LorentzGroup d)))) + LinearEquiv.refl ℝ ((𝟙_ (Rep ℝ ↑(LorentzGroup d)))) apply e.injective have hp' := e.injective.eq_iff.mpr hp have hn' := e.injective.eq_iff.mpr hn - simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V, + simp [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, map_add, map_sub] at hp' hn' linear_combination (norm := ring_nf) (1 / 4) * hp' + (-1/ 4) * hn' rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] + simp only [Action.instMonoidalCategory_tensorUnit_V] ring /-! diff --git a/PhysLean/Relativity/Lorentz/SL2C/Basic.lean b/PhysLean/Relativity/Lorentz/SL2C/Basic.lean index 1e54aeb7..15474c0f 100644 --- a/PhysLean/Relativity/Lorentz/SL2C/Basic.lean +++ b/PhysLean/Relativity/Lorentz/SL2C/Basic.lean @@ -84,7 +84,7 @@ lemma toSelfAdjointMap_apply_σSAL_inl (M : SL(2, ℂ)) : + ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) • PauliMatrix.σSAL (Sum.inr 2) := by simp only [toSelfAdjointMap, PauliMatrix.σSAL, Fin.isValue, Basis.coe_mk, PauliMatrix.σSAL', - PauliMatrix.σ0, LinearMap.coe_mk, AddHom.coe_mk, norm_eq_abs, neg_add_rev, PauliMatrix.σ1, + PauliMatrix.σ0, LinearMap.coe_mk, AddHom.coe_mk, neg_add_rev, PauliMatrix.σ1, neg_of, neg_cons, neg_zero, neg_empty, neg_mul, PauliMatrix.σ2, neg_neg, PauliMatrix.σ3] ext1 simp only [Fin.isValue, AddSubgroup.coe_add, selfAdjoint.val_smul, smul_of, smul_cons, real_smul, @@ -102,10 +102,10 @@ lemma toSelfAdjointMap_apply_σSAL_inl (M : SL(2, ℂ)) : ext x y match x, y with | 0, 0 => - simp only [Fin.isValue, norm_eq_abs, cons_val', cons_val_zero, empty_val', cons_val_fin_one] + simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one] ring_nf | 0, 1 => - simp only [Fin.isValue, norm_eq_abs, cons_val', cons_val_one, head_cons, empty_val', + simp only [Fin.isValue, cons_val', cons_val_one, head_cons, empty_val', cons_val_fin_one, cons_val_zero] ring_nf rw [← re_add_im (M.1 0 0), ← re_add_im (M.1 0 1), ← re_add_im (M.1 1 0), ← re_add_im (M.1 1 1)] @@ -116,7 +116,7 @@ lemma toSelfAdjointMap_apply_σSAL_inl (M : SL(2, ℂ)) : simp only [Fin.isValue, I_sq, mul_neg, mul_one, neg_mul, neg_neg, one_mul, sub_neg_eq_add] ring | 1, 0 => - simp only [Fin.isValue, norm_eq_abs, cons_val', cons_val_zero, empty_val', cons_val_fin_one, + simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, head_fin_const] ring_nf rw [← re_add_im (M.1 0 0), ← re_add_im (M.1 0 1), ← re_add_im (M.1 1 0), ← re_add_im (M.1 1 1)] @@ -127,7 +127,7 @@ lemma toSelfAdjointMap_apply_σSAL_inl (M : SL(2, ℂ)) : simp only [Fin.isValue, I_sq, mul_neg, mul_one, neg_mul, neg_neg, one_mul, sub_neg_eq_add] ring | 1, 1 => - simp only [Fin.isValue, norm_eq_abs, cons_val', cons_val_one, head_cons, empty_val', + simp only [Fin.isValue, cons_val', cons_val_one, head_cons, empty_val', cons_val_fin_one, head_fin_const] ring_nf diff --git a/PhysLean/Relativity/Lorentz/Weyl/Metric.lean b/PhysLean/Relativity/Lorentz/Weyl/Metric.lean index 45f6fdae..7dadf6ae 100644 --- a/PhysLean/Relativity/Lorentz/Weyl/Metric.lean +++ b/PhysLean/Relativity/Lorentz/Weyl/Metric.lean @@ -94,7 +94,7 @@ def leftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded where refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • leftMetricVal = (TensorProduct.map (leftHanded.ρ M) (leftHanded.ρ M)) (x • leftMetricVal) @@ -141,7 +141,7 @@ def altLeftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ altLeftHande refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • altLeftMetricVal = (TensorProduct.map (altLeftHanded.ρ M) (altLeftHanded.ρ M)) (x • altLeftMetricVal) @@ -187,7 +187,7 @@ def rightMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded wher refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • rightMetricVal = (TensorProduct.map (rightHanded.ρ M) (rightHanded.ρ M)) (x • rightMetricVal) @@ -243,7 +243,7 @@ def altRightMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ altRightHa refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • altRightMetricVal = (TensorProduct.map (altRightHanded.ρ M) (altRightHanded.ρ M)) (x • altRightMetricVal) diff --git a/PhysLean/Relativity/Lorentz/Weyl/Unit.lean b/PhysLean/Relativity/Lorentz/Weyl/Unit.lean index de2f9dc5..b366e2df 100644 --- a/PhysLean/Relativity/Lorentz/Weyl/Unit.lean +++ b/PhysLean/Relativity/Lorentz/Weyl/Unit.lean @@ -49,7 +49,7 @@ def leftAltLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • leftAltLeftUnitVal = (TensorProduct.map (leftHanded.ρ M) (altLeftHanded.ρ M)) (x • leftAltLeftUnitVal) @@ -92,7 +92,7 @@ def altLeftLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • altLeftLeftUnitVal = (TensorProduct.map (altLeftHanded.ρ M) (leftHanded.ρ M)) (x • altLeftLeftUnitVal) @@ -139,7 +139,7 @@ def rightAltRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHa refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • rightAltRightUnitVal = (TensorProduct.map (rightHanded.ρ M) (altRightHanded.ρ M)) (x • rightAltRightUnitVal) @@ -190,7 +190,8 @@ def altRightRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHa refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp, + Action.tensorUnit_ρ + , CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • altRightRightUnitVal = (TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M)) (x • altRightRightUnitVal) diff --git a/PhysLean/Relativity/Tensors/OverColor/Discrete.lean b/PhysLean/Relativity/Tensors/OverColor/Discrete.lean index a7d09a36..f56bbb13 100644 --- a/PhysLean/Relativity/Tensors/OverColor/Discrete.lean +++ b/PhysLean/Relativity/Tensors/OverColor/Discrete.lean @@ -111,7 +111,7 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr exact (LinearEquiv.eq_symm_apply _).mp rfl lemma pairIsoSep_inv_tprod {c1 c2 : C} (fx : (i : (𝟭 Type).obj (OverColor.mk ![c1, c2]).left) → - CoeSort.coe (F.obj { as := (OverColor.mk ![c1, c2]).hom i })) : + (F.obj { as := (OverColor.mk ![c1, c2]).hom i }).V) : (pairIsoSep F).inv.hom (PiTensorProduct.tprod k fx) = fx (0 : Fin 2) ⊗ₜ fx (1 : Fin 2) := by simp only [Action.instMonoidalCategory_tensorObj_V, Nat.succ_eq_add_one, Nat.reduceAdd, pairIsoSep, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, diff --git a/PhysLean/Relativity/Tensors/OverColor/Lift.lean b/PhysLean/Relativity/Tensors/OverColor/Lift.lean index a8afb1ea..6e394cc0 100644 --- a/PhysLean/Relativity/Tensors/OverColor/Lift.lean +++ b/PhysLean/Relativity/Tensors/OverColor/Lift.lean @@ -173,9 +173,9 @@ def ε : 𝟙_ (Rep k G) ≅ objObj' F (𝟙_ (OverColor C)) := refine LinearMap.ext (fun x => ?_) simp only [objObj'_V_carrier, OverColor.instMonoidalCategoryStruct_tensorUnit_left, OverColor.instMonoidalCategoryStruct_tensorUnit_hom, - Action.instMonoidalCategory_tensorUnit_V, Action.tensorUnit_ρ', Functor.id_obj, + Action.instMonoidalCategory_tensorUnit_V, Action.tensorUnit_ρ, Functor.id_obj, Category.id_comp, LinearEquiv.coe_coe, ModuleCat.comp_apply] - rw [ModuleCat.hom_comp, ModuleCat.hom_comp] + rw [ModuleCat.hom_comp] simp only [objObj'_V_carrier, instMonoidalCategoryStruct_tensorUnit_left, instMonoidalCategoryStruct_tensorUnit_hom, LinearEquiv.toModuleIso_hom, ModuleCat.hom_ofHom, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply] @@ -232,7 +232,7 @@ def μ (X Y : OverColor C) : objObj' F X ⊗ objObj' F Y ≅ objObj' F (X ⊗ Y) refine PhysLean.PiTensorProduct.induction_tmul (fun p q => ?_) simp only [objObj'_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left, OverColor.instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp, - Action.instMonoidalCategory_tensorObj_V, Action.tensor_ρ', LinearMap.coe_comp, + Action.instMonoidalCategory_tensorObj_V, Action.tensor_ρ, LinearMap.coe_comp, Function.comp_apply] change (μModEquiv F X Y) ((objObj' F X).ρ M (PiTensorProduct.tprod k p) ⊗ₜ[k] @@ -617,7 +617,6 @@ lemma mapApp'_tprod (X : OverColor C) (p : (i : X.left) → F.obj (Discrete.mk ( PiTensorProduct.tprod k fun i => (η.app (Discrete.mk (X.hom i))).hom (p i) := by simp only [mapApp'] erw [PiTensorProduct.map_tprod] - rfl lemma mapApp'_naturality {X Y : OverColor C} (f : X ⟶ Y) : (obj' F).map f ≫ mapApp' η Y = mapApp' η X ≫ (obj' F').map f := by diff --git a/PhysLean/Relativity/Tensors/TensorSpecies/Contractions/Categorical.lean b/PhysLean/Relativity/Tensors/TensorSpecies/Contractions/Categorical.lean index 4cd8d796..94700d93 100644 --- a/PhysLean/Relativity/Tensors/TensorSpecies/Contractions/Categorical.lean +++ b/PhysLean/Relativity/Tensors/TensorSpecies/Contractions/Categorical.lean @@ -68,9 +68,9 @@ lemma contrOneTwoLeft_add_right {c1 c2 : S.C} (x : S.F.obj (OverColor.mk ![c1])) lemma contrOneTwoLeft_tprod_eq {c1 c2 : S.C} (fx : (i : (𝟭 Type).obj (OverColor.mk ![c1]).left) → - CoeSort.coe (S.FD.obj { as := (OverColor.mk ![c1]).hom i })) + (S.FD.obj { as := (OverColor.mk ![c1]).hom i })) (fy : (i : (𝟭 Type).obj (OverColor.mk ![S.τ c1, c2]).left) - → CoeSort.coe (S.FD.obj { as := (OverColor.mk ![S.τ c1, c2]).hom i })) : + → (S.FD.obj { as := (OverColor.mk ![S.τ c1, c2]).hom i })) : contrOneTwoLeft (PiTensorProduct.tprod S.k fx) (PiTensorProduct.tprod S.k fy) = ((S.tensorToVec c2).inv.hom (((S.contr.app (Discrete.mk c1)).hom (fx (0 : Fin 1) ⊗ₜ fy (0 : Fin 2)) • @@ -99,9 +99,9 @@ lemma contrOneTwoLeft_tprod_eq {c1 c2 : S.C} lemma contr_one_two_left_eq_contrOneTwoLeft_tprod {c1 c2 : S.C} (x : S.F.obj (OverColor.mk ![c1])) (y : S.F.obj (OverColor.mk ![S.τ c1, c2])) (fx : (i : (𝟭 Type).obj (OverColor.mk ![c1]).left) → - CoeSort.coe (S.FD.obj { as := (OverColor.mk ![c1]).hom i })) + (S.FD.obj { as := (OverColor.mk ![c1]).hom i })) (fy : (i : (𝟭 Type).obj (OverColor.mk ![S.τ c1, c2]).left) - → CoeSort.coe (S.FD.obj { as := (OverColor.mk ![S.τ c1, c2]).hom i })) + → (S.FD.obj { as := (OverColor.mk ![S.τ c1, c2]).hom i })) (hx : x = PiTensorProduct.tprod S.k fx) (hy : y = PiTensorProduct.tprod S.k fy) : {x | μ ⊗ y | μ ν}ᵀ.tensor = @@ -210,10 +210,10 @@ lemma contrOneTwoLeft_tensorTree {c1 c2 : S.C} (x : S.F.obj (OverColor.mk ![c1]) constructions and fields of the tensor species. -/ lemma contr_two_two_inner_tprod (c : S.C) (x : S.F.obj (OverColor.mk ![c, c])) (fx : (i : (𝟭 Type).obj (OverColor.mk ![c, c]).left) → - CoeSort.coe (S.FD.obj { as := (OverColor.mk ![c, c]).hom i })) + (S.FD.obj { as := (OverColor.mk ![c, c]).hom i })) (y : S.F.obj (OverColor.mk ![(S.τ c), (S.τ c)])) (fy : (i : (𝟭 Type).obj (OverColor.mk ![S.τ c, S.τ c]).left) → - CoeSort.coe (S.FD.obj { as := (OverColor.mk ![S.τ c, S.τ c]).hom i })) + (S.FD.obj { as := (OverColor.mk ![S.τ c, S.τ c]).hom i })) (hx : x = PiTensorProduct.tprod S.k fx) (hy : y = PiTensorProduct.tprod S.k fy) : {x | μ ν ⊗ y| ν ρ}ᵀ.tensor = (S.F.map (OverColor.mkIso (by diff --git a/PhysLean/Relativity/Tensors/Tree/Elab.lean b/PhysLean/Relativity/Tensors/Tree/Elab.lean index 6ea58a4e..d42f60f8 100644 --- a/PhysLean/Relativity/Tensors/Tree/Elab.lean +++ b/PhysLean/Relativity/Tensors/Tree/Elab.lean @@ -103,11 +103,11 @@ def indexToIdent (stx : Syntax) : TermElabM Ident := /-- Takes a pair ``a b : ℕ × TSyntax `indexExpr``. If `a.1 < b.1` and `a.2 = b.2` then outputs `some (a.1, b.1)`, otherwise `none`. -/ -def indexPosEq (a b : ℕ × TSyntax `indexExpr) : TermElabM (Option (ℕ × ℕ)) := do - let a' ← indexToIdent a.2 - let b' ← indexToIdent b.2 - if a.1 < b.1 ∧ Lean.TSyntax.getId a' = Lean.TSyntax.getId b' then - return some (a.1, b.1) +def indexPosEq (a b : TSyntax `indexExpr × ℕ) : TermElabM (Option (ℕ × ℕ)) := do + let a' ← indexToIdent a.1 + let b' ← indexToIdent b.1 + if a.2 < b.2 ∧ Lean.TSyntax.getId a' = Lean.TSyntax.getId b' then + return some (a.2, b.2) else return none @@ -185,7 +185,7 @@ def getNoIndicesExact (stx : Syntax) : TermElabM ℕ := do match n with | 1 => match type with - | Expr.app _ (Expr.app _ (Expr.app _ c)) => + | Expr.app _ (Expr.app _ (Expr.app _ (Expr.app _ c))) => let typeC ← inferType c match typeC with | Expr.forallE _ (Expr.app _ a) _ _ => @@ -297,10 +297,10 @@ def evalAdjustPos (l : List ℕ) : List ℕ := /-- The positions in getIndicesNode which get evaluated, and the value they take. -/ partial def getEvalPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do let ind ← getIndices stx - let indEnum := ind.enum - let evals := indEnum.filter (fun x => indexExprIsNum x.2) - let evals2 ← (evals.mapM (fun x => indexToNum x.2)) - let pos := evalAdjustPos (evals.map (fun x => x.1)) + let indEnum := ind.zipIdx + let evals := indEnum.filter (fun x => indexExprIsNum x.1) + let evals2 ← (evals.mapM (fun x => indexToNum x.1)) + let pos := evalAdjustPos (evals.map (fun x => x.2)) return List.zip pos evals2 /-- For each element of `l : List (ℕ × ℕ)` applies `TensorTree.eval` to the given term. -/ @@ -312,8 +312,8 @@ def evalSyntax (l : List (ℕ × ℕ)) (T : Term) : Term := partial def getContrPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do let ind ← getIndices stx let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x) - let indEnum := indFilt.enum - let bind := List.flatMap indEnum (fun a => indEnum.map (fun b => (a, b))) + let indEnum := indFilt.zipIdx + let bind := List.flatMap (fun a => indEnum.map (fun b => (a, b))) indEnum let filt ← bind.filterMapM (fun x => indexPosEq x.1 x.2) if ¬ ((filt.map Prod.fst).Nodup ∧ (filt.map Prod.snd).Nodup) then throwError "To many contractions" @@ -379,8 +379,8 @@ partial def getIndices (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := partial def getContrPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do let ind ← getIndices stx let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x) - let indEnum := indFilt.enum - let bind := List.flatMap indEnum (fun a => indEnum.map (fun b => (a, b))) + let indEnum := indFilt.zipIdx + let bind := List.flatMap (fun a => indEnum.map (fun b => (a, b))) indEnum let filt ← bind.filterMapM (fun x => indexPosEq x.1 x.2) if ¬ ((filt.map Prod.fst).Nodup ∧ (filt.map Prod.snd).Nodup) then throwError "To many contractions" @@ -408,10 +408,10 @@ end ProdNode def getPermutation (l1 l2 : List (TSyntax `indexExpr)) : TermElabM (List (ℕ)) := do let l1' ← l1.mapM (fun x => indexToIdent x) let l2' ← l2.mapM (fun x => indexToIdent x) - let l1enum := l1'.enum + let l1enum := l1'.zipIdx let l2'' := l2'.filterMap - (fun x => l1enum.find? (fun y => Lean.TSyntax.getId y.2 = Lean.TSyntax.getId x)) - return l2''.map fun x => x.1 + (fun x => l1enum.find? (fun y => Lean.TSyntax.getId y.1 = Lean.TSyntax.getId x)) + return l2''.map fun x => x.2 open PhysLean.Fin diff --git a/PhysLean/Relativity/Tensors/Tree/NodeIdentities/Basic.lean b/PhysLean/Relativity/Tensors/Tree/NodeIdentities/Basic.lean index 2135de9c..bcd85e22 100644 --- a/PhysLean/Relativity/Tensors/Tree/NodeIdentities/Basic.lean +++ b/PhysLean/Relativity/Tensors/Tree/NodeIdentities/Basic.lean @@ -366,7 +366,6 @@ lemma action_constTwoNode {c1 c2 : S.C} (Discrete.pairIsoSep S.FD).hom.hom) _ = _ erw [← v.comm g] simp - rfl /-- An `action` node on a `constThreeNode` leaves the tensor invariant. -/ lemma action_constThreeNode {c1 c2 c3 : S.C} @@ -382,6 +381,5 @@ lemma action_constThreeNode {c1 c2 c3 : S.C} S.FD.obj { as := c3 }).ρ g)) ≫ (Discrete.tripleIsoSep S.FD).hom.hom) _ = _ erw [← v.comm g] simp - rfl end TensorTree diff --git a/PhysLean/Relativity/Tensors/Tree/NodeIdentities/ContrContr.lean b/PhysLean/Relativity/Tensors/Tree/NodeIdentities/ContrContr.lean index ae60d11d..14bd7808 100644 --- a/PhysLean/Relativity/Tensors/Tree/NodeIdentities/ContrContr.lean +++ b/PhysLean/Relativity/Tensors/Tree/NodeIdentities/ContrContr.lean @@ -179,7 +179,7 @@ lemma contrSwapHom_contrMapSnd_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c). rfl lemma contrSwapHom_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).left) → - CoeSort.coe (S.FD.obj { as := (OverColor.mk c).hom i })) : + (S.FD.obj { as := (OverColor.mk c).hom i })) : ((PiTensorProduct.tprod S.k) fun k => x (q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove k))))) = ((lift.obj S.FD).map q.contrSwapHom).hom From 75d864df77bd58ab2a2a8865b3dc53d3958c9108 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 4 Mar 2025 09:08:21 +0000 Subject: [PATCH 3/5] refactor: Lint --- PhysLean/CondensedMatter/Basic.lean | 2 -- PhysLean/Optics/Basic.lean | 1 - .../StandardModel/HiggsBoson/Basic.lean | 2 +- .../HiggsBoson/PointwiseInnerProd.lean | 2 +- .../QuantumMechanics/FiniteTarget/Basic.lean | 2 +- .../HarmonicOscillator/Basic.lean | 4 ++-- .../HarmonicOscillator/Completeness.lean | 2 +- .../HarmonicOscillator/Eigenfunction.lean | 6 ++--- .../OneDimension/HarmonicOscillator/TISE.lean | 11 ++++----- .../OneDimension/HilbertSpace/Basic.lean | 2 +- .../Lorentz/ComplexVector/Unit.lean | 6 ++--- .../Lorentz/RealVector/Contraction.lean | 4 +--- .../Relativity/Lorentz/SL2C/SelfAdjoint.lean | 3 +-- PhysLean/Relativity/Lorentz/Weyl/Unit.lean | 3 +-- PhysLean/Relativity/Tensors/Tree/Elab.lean | 2 +- scripts/hepLean_style_lint.lean | 24 +++++++++---------- 16 files changed, 34 insertions(+), 42 deletions(-) diff --git a/PhysLean/CondensedMatter/Basic.lean b/PhysLean/CondensedMatter/Basic.lean index a80d4345..03b8b831 100644 --- a/PhysLean/CondensedMatter/Basic.lean +++ b/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 - -/ diff --git a/PhysLean/Optics/Basic.lean b/PhysLean/Optics/Basic.lean index 18535366..8eadccb0 100644 --- a/PhysLean/Optics/Basic.lean +++ b/PhysLean/Optics/Basic.lean @@ -18,5 +18,4 @@ Some directories which are NOT currently place holders are: - Quantum Mechanics - Relativity - -/ diff --git a/PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean b/PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean index 411a9b63..b9f75c76 100644 --- a/PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean +++ b/PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean @@ -93,7 +93,7 @@ instance : ContMDiffVectorBundle ⊤ HiggsVec HiggsBundle SpaceTime.asSmoothMani /-- The type `HiggsField` is defined such that elements are smooth sections of the trivial vector bundle `HiggsBundle`. Such elements are Higgs fields. Since `HiggsField` is trivial as a vector bundle, a Higgs field is equivalent to a smooth map - from `SpaceTime` to `HiggsVec`. -/ + from `SpaceTime` to `HiggsVec`. -/ abbrev HiggsField : Type := ContMDiffSection SpaceTime.asSmoothManifold HiggsVec ⊤ HiggsBundle /-- Given a vector in `HiggsVec` the constant Higgs field with value equal to that diff --git a/PhysLean/Particles/StandardModel/HiggsBoson/PointwiseInnerProd.lean b/PhysLean/Particles/StandardModel/HiggsBoson/PointwiseInnerProd.lean index 6d797457..e4197dc3 100644 --- a/PhysLean/Particles/StandardModel/HiggsBoson/PointwiseInnerProd.lean +++ b/PhysLean/Particles/StandardModel/HiggsBoson/PointwiseInnerProd.lean @@ -113,7 +113,7 @@ lemma smooth_innerProd (φ1 φ2 : HiggsField) : ContMDiff 𝓘(ℝ, SpaceTime) the function `SpaceTime → ℝ` obtained by taking the square norm of the pointwise Higgs vector. In other words, `normSq φ x = ‖φ x‖ ^ 2`. - The notation `‖φ‖_H^2` is used for the `normSq φ` -/ + The notation `‖φ‖_H^2` is used for the `normSq φ`. -/ @[simp] def normSq (φ : HiggsField) : SpaceTime → ℝ := fun x => ‖φ x‖ ^ 2 diff --git a/PhysLean/QuantumMechanics/FiniteTarget/Basic.lean b/PhysLean/QuantumMechanics/FiniteTarget/Basic.lean index 27d3399b..55ddd908 100644 --- a/PhysLean/QuantumMechanics/FiniteTarget/Basic.lean +++ b/PhysLean/QuantumMechanics/FiniteTarget/Basic.lean @@ -35,7 +35,7 @@ abbrev V (_ : FiniteTarget n hℏ) := Fin n → ℂ /-- Given a finite target QM system `A`, the time evolution matrix for a `t : ℝ`, `A.timeEvolutionMatrix t` is defined as `e ^ (- I t /ℏ * A.H)`. -/ noncomputable def timeEvolutionMatrix (A : FiniteTarget n hℏ) (t : ℝ) : Matrix (Fin n) (Fin n) ℂ := - NormedSpace.exp ℂ (- (Complex.I * t / ℏ) • A.H) + NormedSpace.exp ℂ (- (Complex.I * t / ℏ) • A.H) /-- Given a finite target QM system `A`, `timeEvolution` is the linear map from `A.V` to `A.V` obtained by multiplication with `timeEvolutionMatrix`. -/ diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean index 3d800c23..1bf1eb6f 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean @@ -134,7 +134,7 @@ lemma one_over_ξ : 1/Q.ξ = √(Q.m * Q.ω / Q.ℏ) := by have := Q.hℏ field_simp [ξ] -lemma ξ_inverse : Q.ξ⁻¹ = √(Q.m * Q.ω / Q.ℏ):= by +lemma ξ_inverse : Q.ξ⁻¹ = √(Q.m * Q.ω / Q.ℏ) := by rw [inv_eq_one_div] exact one_over_ξ Q @@ -182,7 +182,7 @@ lemma schrodingerOperator_eq (ψ : ℝ → ℂ) : /-- The schrodinger operator written in terms of `ξ`. -/ lemma schrodingerOperator_eq_ξ (ψ : ℝ → ℂ) : Q.schrodingerOperator ψ = - fun x => (Q.ℏ ^2 / (2 * Q.m)) * (- (deriv (deriv ψ) x) + (1/Q.ξ^2 )^2 * x^2 * ψ x) := by + fun x => (Q.ℏ ^2 / (2 * Q.m)) * (- (deriv (deriv ψ) x) + (1/Q.ξ^2)^2 * x^2 * ψ x) := by funext x simp [schrodingerOperator_eq, ξ_sq, ξ_inverse, ξ_ne_zero, ξ_pos, ξ_abs, ← Complex.ofReal_pow] have hm' := Complex.ofReal_ne_zero.mpr Q.m_ne_zero diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean index b28ed4f0..3daf1bb1 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean @@ -175,7 +175,7 @@ lemma orthogonal_physHermite_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) or_false, Real.sqrt_nonneg] at h1 have h0 : n ! ≠ 0 := by exact factorial_ne_zero n - have h0' : ¬ (√Q.ξ = 0 ∨ √Real.pi = 0):= by + have h0' : ¬ (√Q.ξ = 0 ∨ √Real.pi = 0) := by simpa using And.intro (Real.sqrt_ne_zero'.mpr Q.ξ_pos) (Real.sqrt_ne_zero'.mpr Real.pi_pos) simp only [h0, h0', or_self, false_or] at h1 rw [← h1] diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean index 09ef79e6..8e6a0e67 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean @@ -43,7 +43,7 @@ lemma eigenfunction_eq (n : ℕ) : ring lemma eigenfunction_zero : Q.eigenfunction 0 = fun (x : ℝ) => - (1/ √(√Real.pi * Q.ξ)) * Complex.exp (- x^2 / (2 * Q.ξ^2)):= by + (1/ √(√Real.pi * Q.ξ)) * Complex.exp (- x^2 / (2 * Q.ξ^2)) := by funext x simp [eigenfunction] @@ -190,8 +190,8 @@ lemma eigenfunction_mul (n p : ℕ) : one_div, mul_inv_rev, neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_pow, Complex.ofReal_ofNat, mul_one] ring - _ = (1/√(2 ^ n * n !) * 1/√(2 ^ p * p !)) * (1/ (√Real.pi * Q.ξ)) * - (physHermite n (x / Q.ξ) * physHermite p (x / Q.ξ)) * (Real.exp (- x^2 / Q.ξ^2)) := by + _ = (1/√(2 ^ n * n !) * 1/√(2 ^ p * p !)) * (1/ (√Real.pi * Q.ξ)) * + (physHermite n (x / Q.ξ) * physHermite p (x / Q.ξ)) * (Real.exp (- x^2 / Q.ξ^2)) := by congr 1 · congr 1 · congr 1 diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean index d2feb003..716c4571 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean @@ -70,7 +70,7 @@ lemma deriv_eigenfunction_zero : deriv (Q.eigenfunction 0) = ring lemma deriv_eigenfunction_zero' : deriv (Q.eigenfunction 0) = - (- √2 / (2 * Q.ξ) : ℂ) • Q.eigenfunction 1 := by + (- √2 / (2 * Q.ξ) : ℂ) • Q.eigenfunction 1 := by rw [deriv_eigenfunction_zero] funext x simp only [Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_one, Complex.ofReal_pow, @@ -89,7 +89,7 @@ lemma deriv_physHermite_characteristic_length (n : ℕ) : match n with | 0 => rw [physHermite_zero] - simp [deriv_const_mul_field', Complex.ofReal_div, Complex.ofReal_mul, Algebra.smul_mul_assoc, + simp [deriv_const_mul_field', Complex.ofReal_div, Complex.ofReal_mul, Algebra.smul_mul_assoc, Complex.ofReal_zero, zero_mul, zero_add, zero_div, cast_zero, Complex.ofReal_zero, zero_smul] | n + 1 => funext x @@ -158,7 +158,6 @@ lemma deriv_deriv_eigenfunction_zero (x : ℝ) : deriv (deriv (Q.eigenfunction 0 simp only [Complex.ofReal_one, Complex.ofReal_pow, one_mul, one_pow, inv_pow] ring - lemma deriv_deriv_eigenfunction_succ (n : ℕ) (x : ℝ) : deriv (fun x => deriv (Q.eigenfunction (n + 1)) x) x = Complex.ofReal (1/√(2 ^ (n + 1) * (n + 1) !) * (1/Q.ξ)) * @@ -183,7 +182,7 @@ lemma deriv_deriv_eigenfunction_succ (n : ℕ) (x : ℝ) : simp only [differentiableAt_const, deriv_mul, deriv_const', zero_mul, mul_zero, add_zero, deriv_add, zero_add] rw [deriv_mul (by fun_prop) (by fun_prop)] - simp [deriv_mul_const_field', Complex.deriv_ofReal, mul_one] + simp [deriv_mul_const_field', Complex.deriv_ofReal, mul_one] nth_rewrite 2 [deriv_physHermite_characteristic_length] ring_nf simp only [one_div, Complex.ofReal_inv, cast_add, cast_one, add_tsub_cancel_right] @@ -195,7 +194,7 @@ lemma deriv_deriv_eigenfunction (n : ℕ) (x : ℝ) : match n with | 0 => simpa using Q.deriv_deriv_eigenfunction_zero x | n + 1 => - trans Complex.ofReal (1/Real.sqrt (2 ^ (n + 1) * (n + 1) !) ) * + trans Complex.ofReal (1/Real.sqrt (2 ^ (n + 1) * (n + 1) !)) * (((- 1 / Q.ξ ^ 2) * (2 * (n + 1) + (1 + (- 1/ Q.ξ ^ 2) * x ^ 2)) * (physHermite (n + 1) (x/Q.ξ))) * Q.eigenfunction 0 x) @@ -223,7 +222,7 @@ lemma deriv_deriv_eigenfunction (n : ℕ) (x : ℝ) : trans (- 1/ Q.ξ^2) * (2 * (n + 1) * (2 * ((1 / Q.ξ) * x) * (physHermite n (x/Q.ξ)) - 2 * n * (physHermite (n - 1) (x/Q.ξ))) - + (1 + (- 1 / Q.ξ^2) * x ^ 2) * (physHermite (n + 1) ( x/Q.ξ))) + + (1 + (- 1 / Q.ξ^2) * x ^ 2) * (physHermite (n + 1) (x/Q.ξ))) · ring_nf trans (- 1 / Q.ξ^2) * (2 * (n + 1) * (physHermite (n + 1) (x/Q.ξ)) + (1 + (- 1/ Q.ξ^2) * x ^ 2) * (physHermite (n + 1) (x/Q.ξ))) diff --git a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean index cf4716a3..7bd586b9 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean @@ -55,7 +55,7 @@ lemma memHS_iff {f : ℝ → ℂ} : MemHS f ↔ exact Continuous.comp_aestronglyMeasurable continuous_norm h1 simp only [h0, true_and] simp only [HasFiniteIntegral, enorm_pow] - simp only [enorm, nnnorm, Real.norm_eq_abs, abs_norm] + simp only [enorm, nnnorm, Real.norm_eq_abs, abs_norm] lemma aeEqFun_mk_mem_iff (f : ℝ → ℂ) (hf : AEStronglyMeasurable f volume) : AEEqFun.mk f hf ∈ HilbertSpace ↔ MemHS f := by diff --git a/PhysLean/Relativity/Lorentz/ComplexVector/Unit.lean b/PhysLean/Relativity/Lorentz/ComplexVector/Unit.lean index c35d7125..849c2e28 100644 --- a/PhysLean/Relativity/Lorentz/ComplexVector/Unit.lean +++ b/PhysLean/Relativity/Lorentz/ComplexVector/Unit.lean @@ -143,11 +143,11 @@ lemma contr_contrCoUnit (x : complexCo) : Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add, _root_.map_smul] - have h1' (x y : complexCo.V) (z : complexContr.V) : + have h1' (x y : complexCo.V) (z : complexContr.V) : (α_ complexCo.V complexContr.V complexCo.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl repeat rw [h1'] have h1'' (y : complexCo.V) - (z : complexCo.V ⊗[ℂ] complexContr.V) : + (z : complexCo.V ⊗[ℂ] complexContr.V) : (coContrContraction.hom ▷ complexCo.V) (z ⊗ₜ[ℂ] y) = (coContrContraction.hom z) ⊗ₜ[ℂ] y := rfl repeat rw (config := { transparency := .instances }) [h1''] repeat rw [coContrContraction_basis'] @@ -182,7 +182,7 @@ lemma contr_coContrUnit (x : complexContr) : (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl repeat rw [h1'] have h1'' (y : complexContr.V) - (z : complexContr.V ⊗[ℂ] complexCo.V) : + (z : complexContr.V ⊗[ℂ] complexCo.V) : (contrCoContraction.hom ▷ complexContr.V) (z ⊗ₜ[ℂ] y) = (contrCoContraction.hom z) ⊗ₜ[ℂ] y := rfl repeat rw (config := { transparency := .instances }) [h1''] diff --git a/PhysLean/Relativity/Lorentz/RealVector/Contraction.lean b/PhysLean/Relativity/Lorentz/RealVector/Contraction.lean index 900f07c3..3f9b6c63 100644 --- a/PhysLean/Relativity/Lorentz/RealVector/Contraction.lean +++ b/PhysLean/Relativity/Lorentz/RealVector/Contraction.lean @@ -335,9 +335,7 @@ lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔ apply e.injective have hp' := e.injective.eq_iff.mpr hp have hn' := e.injective.eq_iff.mpr hn - simp [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V, - Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, - Action.FunctorCategoryEquivalence.functor_obj_obj, map_add, map_sub] at hp' hn' + simp only [Action.instMonoidalCategory_tensorUnit_V, map_add, map_sub] at hp' hn' linear_combination (norm := ring_nf) (1 / 4) * hp' + (-1/ 4) * hn' rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] simp only [Action.instMonoidalCategory_tensorUnit_V] diff --git a/PhysLean/Relativity/Lorentz/SL2C/SelfAdjoint.lean b/PhysLean/Relativity/Lorentz/SL2C/SelfAdjoint.lean index c7b20a0d..47cee44b 100644 --- a/PhysLean/Relativity/Lorentz/SL2C/SelfAdjoint.lean +++ b/PhysLean/Relativity/Lorentz/SL2C/SelfAdjoint.lean @@ -72,8 +72,7 @@ $$\begin{align} \begin{vmatrix} \operatorname{Re}(x\bar{y}) & -\operatorname{Im}(x\bar{y}) \\ \operatorname{Im}(x\bar{y}) & \operatorname{Re}(x\bar{y}) -\end{vmatrix} \det\left( - \begin{bmatrix} \lvert x\rvert^2 & □ \\ 0 & \lvert y\rvert^2 \end{bmatrix} - +\end{vmatrix} \det\left(\begin{bmatrix} \lvert x\rvert^2 & □ \\ 0 & \lvert y\rvert^2 \end{bmatrix} - \begin{bmatrix} □ & □ \\ 0 & 0 \end{bmatrix} \begin{bmatrix} □ & □ \\ □ & □ \end{bmatrix} \begin{bmatrix} 0 & □ \\ 0 & □ \end{bmatrix} diff --git a/PhysLean/Relativity/Lorentz/Weyl/Unit.lean b/PhysLean/Relativity/Lorentz/Weyl/Unit.lean index b366e2df..06692383 100644 --- a/PhysLean/Relativity/Lorentz/Weyl/Unit.lean +++ b/PhysLean/Relativity/Lorentz/Weyl/Unit.lean @@ -190,8 +190,7 @@ def altRightRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHa refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ - , CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • altRightRightUnitVal = (TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M)) (x • altRightRightUnitVal) diff --git a/PhysLean/Relativity/Tensors/Tree/Elab.lean b/PhysLean/Relativity/Tensors/Tree/Elab.lean index d42f60f8..689773f0 100644 --- a/PhysLean/Relativity/Tensors/Tree/Elab.lean +++ b/PhysLean/Relativity/Tensors/Tree/Elab.lean @@ -380,7 +380,7 @@ partial def getContrPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do let ind ← getIndices stx let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x) let indEnum := indFilt.zipIdx - let bind := List.flatMap (fun a => indEnum.map (fun b => (a, b))) indEnum + let bind := List.flatMap (fun a => indEnum.map (fun b => (a, b))) indEnum let filt ← bind.filterMapM (fun x => indexPosEq x.1 x.2) if ¬ ((filt.map Prod.fst).Nodup ∧ (filt.map Prod.snd).Nodup) then throwError "To many contractions" diff --git a/scripts/hepLean_style_lint.lean b/scripts/hepLean_style_lint.lean index a02fd5a7..3de6a349 100644 --- a/scripts/hepLean_style_lint.lean +++ b/scripts/hepLean_style_lint.lean @@ -31,9 +31,9 @@ def PhysLeanTextLinter : Type := Array String → Array (String × ℕ × ℕ) /-- Checks if there are two consecutive empty lines. -/ def doubleEmptyLineLinter : PhysLeanTextLinter := fun lines ↦ Id.run do - let enumLines := (lines.toList.enumFrom 1) + let enumLines := (lines.toList.zipIdx 1) let pairLines := List.zip enumLines (List.tail! enumLines) - let errors := pairLines.filterMap (fun ((lno1, l1), _, l2) ↦ + let errors := pairLines.filterMap (fun ((l1, lno1), l2, _) ↦ if l1.length == 0 && l2.length == 0 then some (s!" Double empty line. ", lno1, 1) else none) @@ -41,8 +41,8 @@ def doubleEmptyLineLinter : PhysLeanTextLinter := fun lines ↦ Id.run do /-- Checks if there is a double space in the line, which is not at the start. -/ def doubleSpaceLinter : PhysLeanTextLinter := fun lines ↦ Id.run do - let enumLines := (lines.toList.enumFrom 1) - let errors := enumLines.filterMap (fun (lno, l) ↦ + let enumLines := (lines.toList.zipIdx 1) + let errors := enumLines.filterMap (fun (l, lno) ↦ if String.containsSubstr l.trimLeft " " then let k := (Substring.findAllSubstr l " ").toList.getLast? let col := match k with @@ -53,8 +53,8 @@ def doubleSpaceLinter : PhysLeanTextLinter := fun lines ↦ Id.run do errors.toArray def longLineLinter : PhysLeanTextLinter := fun lines ↦ Id.run do - let enumLines := (lines.toList.enumFrom 1) - let errors := enumLines.filterMap (fun (lno, l) ↦ + let enumLines := (lines.toList.zipIdx 1) + let errors := enumLines.filterMap (fun (l, lno) ↦ if l.length > 100 ∧ ¬ String.containsSubstr l "http" then some (s!" Line is too long.", lno, 100) else none) @@ -62,8 +62,8 @@ def longLineLinter : PhysLeanTextLinter := fun lines ↦ Id.run do /-- Substring linter. -/ def substringLinter (s : String) : PhysLeanTextLinter := fun lines ↦ Id.run do - let enumLines := (lines.toList.enumFrom 1) - let errors := enumLines.filterMap (fun (lno, l) ↦ + let enumLines := (lines.toList.zipIdx 1) + let errors := enumLines.filterMap (fun (l, lno) ↦ if String.containsSubstr l s then let k := (Substring.findAllSubstr l s).toList.getLast? let col := match k with @@ -74,8 +74,8 @@ def substringLinter (s : String) : PhysLeanTextLinter := fun lines ↦ Id.run do errors.toArray def endLineLinter (s : String) : PhysLeanTextLinter := fun lines ↦ Id.run do - let enumLines := (lines.toList.enumFrom 1) - let errors := enumLines.filterMap (fun (lno, l) ↦ + let enumLines := (lines.toList.zipIdx 1) + let errors := enumLines.filterMap (fun (l, lno) ↦ if l.endsWith s then some (s!" Line ends with `{s}`.", lno, l.length) else none) @@ -83,8 +83,8 @@ def endLineLinter (s : String) : PhysLeanTextLinter := fun lines ↦ Id.run do /-- Number of space at new line must be even. -/ def numInitialSpacesEven : PhysLeanTextLinter := fun lines ↦ Id.run do - let enumLines := (lines.toList.enumFrom 1) - let errors := enumLines.filterMap (fun (lno, l) ↦ + let enumLines := (lines.toList.zipIdx 1) + let errors := enumLines.filterMap (fun (l, lno) ↦ let numSpaces := (l.takeWhile (· == ' ')).length if numSpaces % 2 != 0 then some (s!"Number of initial spaces is not even.", lno, 1) From c7342f31262e167ef8ffac9619018c8d13021a00 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 4 Mar 2025 09:36:48 +0000 Subject: [PATCH 4/5] feat: Lint --- .../Lorentz/ComplexTensor/Units/Basis.lean | 12 ++---------- PhysLean/Relativity/Tensors/OverColor/Lift.lean | 1 - 2 files changed, 2 insertions(+), 11 deletions(-) diff --git a/PhysLean/Relativity/Lorentz/ComplexTensor/Units/Basis.lean b/PhysLean/Relativity/Lorentz/ComplexTensor/Units/Basis.lean index d1c18146..17c5a23e 100644 --- a/PhysLean/Relativity/Lorentz/ComplexTensor/Units/Basis.lean +++ b/PhysLean/Relativity/Lorentz/ComplexTensor/Units/Basis.lean @@ -40,10 +40,6 @@ lemma coContrUnit_tensorBasis : coContrUnit = (Fin 4) (fun x => ↑Lorentz.complexCo.V) Basis.instFunLike = @DFunLike.coe (Basis (Fin 4) ℂ (Lorentz.complexCo)) (Fin 4) (fun x => Lorentz.complexCo) Basis.instFunLike := by rfl - have hI3 : @DFunLike.coe (Basis (Fin 4) ℂ ↑Lorentz.complexContr.V) - (Fin 4) (fun x => ↑Lorentz.complexContr.V) Basis.instFunLike - = @DFunLike.coe (Basis (Fin 4) ℂ (Lorentz.complexContr)) (Fin 4) - (fun x => Lorentz.complexContr) Basis.instFunLike := by rfl have hI4 : @OfNat.ofNat complexLorentzTensor.k 1 One.toOfNat1 = @OfNat.ofNat ℂ 1 One.toOfNat1 := by rfl trans {δ' | μ ν}ᵀ.tensor @@ -70,7 +66,7 @@ lemma coContrUnit_tensorBasis : coContrUnit = · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom, cons_val_zero, Fin.cases_zero] simp only [complexLorentzTensor, Discrete.functor_obj_eq_as, Monoidal.tensorUnit_obj, - Fin.mk_one, Fin.isValue, cons_val_one, head_cons, hI1, hI3, + Fin.mk_one, Fin.isValue, cons_val_one, head_cons, hI1, Lorentz.complexContrBasisFin4_apply_zero, Lorentz.complexContrBasisFin4_apply_two, Lorentz.complexContrBasisFin4_apply_one, Lorentz.complexContrBasisFin4_apply_three] @@ -88,10 +84,6 @@ lemma contrCoUnit_tensorBasis : contrCoUnit = (Fin 4) (fun x => ↑Lorentz.complexCo.V) Basis.instFunLike = @DFunLike.coe (Basis (Fin 4) ℂ (Lorentz.complexCo)) (Fin 4) (fun x => Lorentz.complexCo) Basis.instFunLike := by rfl - have hI3 : @DFunLike.coe (Basis (Fin 4) ℂ ↑Lorentz.complexContr.V) - (Fin 4) (fun x => ↑Lorentz.complexContr.V) Basis.instFunLike - = @DFunLike.coe (Basis (Fin 4) ℂ (Lorentz.complexContr)) (Fin 4) - (fun x => Lorentz.complexContr) Basis.instFunLike := by rfl have hI4 : @OfNat.ofNat complexLorentzTensor.k 1 One.toOfNat1 = @OfNat.ofNat ℂ 1 One.toOfNat1 := by rfl trans {δ | μ ν}ᵀ.tensor @@ -114,7 +106,7 @@ lemma contrCoUnit_tensorBasis : contrCoUnit = fin_cases i · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom, cons_val_zero, Fin.cases_zero] - simp [complexLorentzTensor, hI1, hI3] + simp [complexLorentzTensor, hI1] · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom, cons_val_zero, Fin.cases_zero] simp only [complexLorentzTensor, Discrete.functor_obj_eq_as, Monoidal.tensorUnit_obj, diff --git a/PhysLean/Relativity/Tensors/OverColor/Lift.lean b/PhysLean/Relativity/Tensors/OverColor/Lift.lean index 6e394cc0..145eb78d 100644 --- a/PhysLean/Relativity/Tensors/OverColor/Lift.lean +++ b/PhysLean/Relativity/Tensors/OverColor/Lift.lean @@ -89,7 +89,6 @@ lemma objObj'_ρ_tprod (f : OverColor C) (M : G) (x : (i : f.left) → F.obj (Di rw [PiTensorProduct.map_tprod] rfl -@[simp] lemma objObj'_ρ_empty (g : G) : (objObj' F (𝟙_ (OverColor C))).ρ g = LinearMap.id := by rw [objObj'_ρ] ext x From 326761a4661e2643ef4ec333c18f900e6484af8e Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 4 Mar 2025 11:26:46 +0000 Subject: [PATCH 5/5] refactor: Lint --- .../Lorentz/ComplexTensor/Units/Basis.lean | 32 ++++--------------- 1 file changed, 6 insertions(+), 26 deletions(-) diff --git a/PhysLean/Relativity/Lorentz/ComplexTensor/Units/Basis.lean b/PhysLean/Relativity/Lorentz/ComplexTensor/Units/Basis.lean index 17c5a23e..9e285672 100644 --- a/PhysLean/Relativity/Lorentz/ComplexTensor/Units/Basis.lean +++ b/PhysLean/Relativity/Lorentz/ComplexTensor/Units/Basis.lean @@ -33,21 +33,11 @@ lemma coContrUnit_tensorBasis : coContrUnit = + complexLorentzTensor.tensorBasis ![Color.down, Color.up] (fun _ => 1) + complexLorentzTensor.tensorBasis ![Color.down, Color.up] (fun _ => 2) + complexLorentzTensor.tensorBasis ![Color.down, Color.up] (fun _ => 3) := by - have hI1 (n : ℕ) : @OfNat.ofNat (Fin (complexLorentzTensor.repDim - (![Color.down, Color.up] ((fun i => i) ⟨0, Nat.zero_lt_two⟩)))) n Fin.instOfNat = - @OfNat.ofNat (Fin 4) n Fin.instOfNat := by rfl - have hI2 : @DFunLike.coe (Basis (Fin 4) ℂ ↑Lorentz.complexCo.V) - (Fin 4) (fun x => ↑Lorentz.complexCo.V) Basis.instFunLike - = @DFunLike.coe (Basis (Fin 4) ℂ (Lorentz.complexCo)) (Fin 4) - (fun x => Lorentz.complexCo) Basis.instFunLike := by rfl - have hI4 : @OfNat.ofNat complexLorentzTensor.k 1 One.toOfNat1 = - @OfNat.ofNat ℂ 1 One.toOfNat1 := by rfl trans {δ' | μ ν}ᵀ.tensor · simp rw [tensorNode_coContrUnit] simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor, - Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - hI4] + Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V] rw (transparency := .instances) [Lorentz.coContrUnit_apply_one] rw [Lorentz.coContrUnitVal_expand_tmul] simp only [Fin.isValue, map_add] @@ -62,11 +52,11 @@ lemma coContrUnit_tensorBasis : coContrUnit = fin_cases i · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom, cons_val_zero, Fin.cases_zero] - simp [complexLorentzTensor, hI1, hI2] + simp [complexLorentzTensor] · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom, cons_val_zero, Fin.cases_zero] simp only [complexLorentzTensor, Discrete.functor_obj_eq_as, Monoidal.tensorUnit_obj, - Fin.mk_one, Fin.isValue, cons_val_one, head_cons, hI1, + Fin.mk_one, Fin.isValue, cons_val_one, head_cons, Lorentz.complexContrBasisFin4_apply_zero, Lorentz.complexContrBasisFin4_apply_two, Lorentz.complexContrBasisFin4_apply_one, Lorentz.complexContrBasisFin4_apply_three] @@ -77,21 +67,11 @@ lemma contrCoUnit_tensorBasis : contrCoUnit = + complexLorentzTensor.tensorBasis ![Color.up, Color.down] (fun _ => 1) + complexLorentzTensor.tensorBasis ![Color.up, Color.down] (fun _ => 2) + complexLorentzTensor.tensorBasis ![Color.up, Color.down] (fun _ => 3) := by - have hI1 (n : ℕ) : @OfNat.ofNat (Fin (complexLorentzTensor.repDim - (![Color.up, Color.down] ((fun i => i) ⟨0, Nat.zero_lt_two⟩)))) n Fin.instOfNat = - @OfNat.ofNat (Fin 4) n Fin.instOfNat := by rfl - have hI2 : @DFunLike.coe (Basis (Fin 4) ℂ ↑Lorentz.complexCo.V) - (Fin 4) (fun x => ↑Lorentz.complexCo.V) Basis.instFunLike - = @DFunLike.coe (Basis (Fin 4) ℂ (Lorentz.complexCo)) (Fin 4) - (fun x => Lorentz.complexCo) Basis.instFunLike := by rfl - have hI4 : @OfNat.ofNat complexLorentzTensor.k 1 One.toOfNat1 = - @OfNat.ofNat ℂ 1 One.toOfNat1 := by rfl trans {δ | μ ν}ᵀ.tensor · simp rw [tensorNode_contrCoUnit] simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor, - Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - hI4] + Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V] rw (transparency := .instances) [Lorentz.contrCoUnit_apply_one] rw [Lorentz.contrCoUnitVal_expand_tmul] simp only [Fin.isValue, map_add] @@ -106,11 +86,11 @@ lemma contrCoUnit_tensorBasis : contrCoUnit = fin_cases i · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom, cons_val_zero, Fin.cases_zero] - simp [complexLorentzTensor, hI1] + simp [complexLorentzTensor] · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom, cons_val_zero, Fin.cases_zero] simp only [complexLorentzTensor, Discrete.functor_obj_eq_as, Monoidal.tensorUnit_obj, - Fin.mk_one, Fin.isValue, cons_val_one, head_cons, hI1, hI2, + Fin.mk_one, Fin.isValue, cons_val_one, head_cons, Lorentz.complexCoBasisFin4_apply_one, Lorentz.complexCoBasisFin4_apply_zero, Lorentz.complexCoBasisFin4_apply_two, Lorentz.complexCoBasisFin4_apply_three] rfl