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

chore: Update to Lean 4.9-rc1

Browse source
This commit is contained in:
jstoobysmith 2024-06-07 08:41:49 -04:00
parent 60f1ebc3eb
commit b0db05a208
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]