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

Merge pull request #41 from HEPLean/Update-versions

Browse source 
chore: Update to Lean 4.9-rc1
This commit is contained in:
Joseph Tooby-Smith 2024-06-07 09:56:39 -04:00 • committed by GitHub
commit ba506280c1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 27 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
View file

@ -114,12 +114,12 @@ lemma boundary_split (k : Fin n) : k.succ.val + (n.succ - k.succ.val) = n.succ
lemma boundary_accGrav' (k : Fin n) : accGrav n.succ S =
∑ i : Fin (k.succ.val + (n.succ - k.succ.val)), S (Fin.cast (boundary_split k) i) := by
simp [accGrav]
erw [Finset.sum_equiv (Fin.castIso (boundary_split k)).toEquiv]
erw [Finset.sum_equiv (Fin.castOrderIso (boundary_split k)).toEquiv]
intro i
simp only [Fin.val_succ, mem_univ, RelIso.coe_fn_toEquiv]
intro i
simp
rfl
lemma boundary_accGrav'' (k : Fin n) (hk : boundary S k) :
accGrav n.succ S = (2 * ↑↑k + 1 - ↑n) * S (0 : Fin n.succ) := by

12
HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
View file

@ -71,9 +71,9 @@ lemma ext_δ (S T : Fin (2 * n.succ) → ℚ) (h1 : ∀ i, S (δ₁ i) = T (δ
lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) :
∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by
rw [Finset.sum_equiv (Fin.castIso (split_equal n.succ)).symm.toEquiv]
rw [Finset.sum_equiv (Fin.castOrderIso (split_equal n.succ)).symm.toEquiv]
intro i
simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
intro i
simp
rw [h1]
@ -83,9 +83,9 @@ lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) :
lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) :
∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by
rw [Finset.sum_equiv (Fin.castIso (split_equal n.succ)).symm.toEquiv]
rw [Finset.sum_equiv (Fin.castOrderIso (split_equal n.succ)).symm.toEquiv]
intro i
simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
intro i
simp
rw [h1]
@ -95,9 +95,9 @@ lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) :
lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) :
∑ i, S i = S δ!₃ + S δ!₄ + ∑ i : Fin n, ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by
have h1 : ∑ i, S i = ∑ i : Fin (1 + ((n + n) + 1)), S (Fin.cast (n_cond₂ n) i) := by
rw [Finset.sum_equiv (Fin.castIso (n_cond₂ n)).symm.toEquiv]
rw [Finset.sum_equiv (Fin.castOrderIso (n_cond₂ n)).symm.toEquiv]
intro i
simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
intro i
simp
rw [h1]

10
HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
View file

@ -75,7 +75,7 @@ def δa₄ (j : Fin n.succ) : Fin (2 * n.succ + 1) :=
Fin.cast (split_adda n) (Fin.natAdd ((1+n)+1) j)
lemma δa₁_δ₁ : @δa₁ n = δ₁ 0 := by
rfl
exact Fin.rev_inj.mp rfl
lemma δa₁_δ!₃ : @δa₁ n = δ!₃ := by
rfl
@ -115,9 +115,9 @@ lemma δ₂_δ!₂ (j : Fin n) : δ₂ j = δ!₂ j := by
lemma sum_δ (S : Fin (2 * n + 1) → ℚ) :
∑ i, S i = S δ₃ + ∑ i : Fin n, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
have h1 : ∑ i, S i = ∑ i : Fin (n + 1 + n), S (Fin.cast (split_odd n) i) := by
rw [Finset.sum_equiv (Fin.castIso (split_odd n)).symm.toEquiv]
rw [Finset.sum_equiv (Fin.castOrderIso (split_odd n)).symm.toEquiv]
intro i
simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
intro i
simp
rw [h1]
@ -131,9 +131,9 @@ lemma sum_δ (S : Fin (2 * n + 1) → ℚ) :
lemma sum_δ! (S : Fin (2 * n + 1) → ℚ) :
∑ i, S i = S δ!₃ + ∑ i : Fin n, ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by
have h1 : ∑ i, S i = ∑ i : Fin ((1+n)+n), S (Fin.cast (split_odd! n) i) := by
rw [Finset.sum_equiv (Fin.castIso (split_odd! n)).symm.toEquiv]
rw [Finset.sum_equiv (Fin.castOrderIso (split_odd! n)).symm.toEquiv]
intro i
simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
simp only [mem_univ, Fin.castOrderIso, RelIso.coe_fn_toEquiv]
intro i
simp
rw [h1]

4
HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
View file

@ -235,7 +235,7 @@ lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) :
(- arg [V]ud )
(- arg [V]us)
(τ - arg [V]ud - arg [V]us - arg [V]cb - arg [V]tb)
have hUV : ⟦U⟧ = ⟦V⟧ := by
have hUV : Quotient.mk CKMMatrixSetoid U = ⟦V⟧ := by
simp only [Quotient.eq]
symm
exact phaseShiftApply.equiv _ _ _ _ _ _ _
@ -268,7 +268,7 @@ lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud
let U : CKMMatrix := phaseShiftApply V 0 0 (- Real.pi + arg [V]cd + arg [V]cs + arg [V]ub)
(Real.pi - arg [V]cd ) (- arg [V]cs) (- arg [V]ub )
use U
have hUV : ⟦U⟧ = ⟦V⟧ := by
have hUV : Quotient.mk CKMMatrixSetoid U= ⟦V⟧ := by
simp only [Quotient.eq]
symm
exact phaseShiftApply.equiv _ _ _ _ _ _ _

22
lake-manifest.json
View file

@ -1,31 +1,31 @@
{"version": 7,
{"version": "1.0.0",
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"rev": "14f258593e8c261d8834f13c6edc7b970c253ee8",
"rev": "af2dda22771c59db026c48ac0aabc73b72b7a4de",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inputRev": "nightly-testing",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
"rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
"rev": "44f57616b0d9b8f9e5606f2c58d01df54840eba7",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inputRev": "nightly-testing",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"rev": "f617e0673845925e612b62141ff54c4b7980dc63",
"rev": "f744aab6fc4e06553464e6ae66730a3b14b8e615",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inputRev": "nightly-testing",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
@ -49,7 +49,7 @@
{"url": "https://github.com/leanprover-community/import-graph.git",
"type": "git",
"subDir": null,
"rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb",
"rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@ -58,7 +58,7 @@
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"rev": "b1087dd1d2d0075153f5ecffd8848d43cf02c042",
"rev": "1df6b982d827c6f6e335f594f5db66e3624abaf2",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": null,
@ -76,7 +76,7 @@
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
"type": "git",
"subDir": null,
"rev": "8b53cc65534bc2c6888c3d4c53a3439648213f74",
"rev": "effd8b8771cfd7ece69db99448168078e113c61f",
"name": "UnicodeBasic",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@ -94,7 +94,7 @@
{"url": "https://github.com/leanprover/doc-gen4",
"type": "git",
"subDir": null,
"rev": "b91fea210b7b6b451f19c6344d1f82765b9607af",
"rev": "1cae40a2dd0dca57030385ff53d72c3aa7b27f2b",
"name": "«doc-gen4»",
"manifestFile": "lake-manifest.json",
"inputRev": "main",

2
lean-toolchain
View file

@ -1 +1 @@
leanprover/lean4:v4.8.0-rc1
leanprover/lean4:v4.9.0-rc1