feat(tensors): prove the Levi-Civita contraction identities - #1565
feat(tensors): prove the Levi-Civita contraction identities#1565Robby955 wants to merge 5 commits into
Conversation
|
Thank you for this pull-request (PR). If this is your first PR, welcome to the community! Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.
Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages. If you have any problems or questions, please reach out to the community on the Zulip. |
|
Will try and give a proper review tomorrow, but I think this could do with lemmas moved around bit. For example there are some IsReindexing lemmas here which should likely be in the corresponding file not here |
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Some more things to move.
There are also lots of small definitions/lemmas that are:
- Either not needed,
- Can be reframed in terms of useful physics API.
| rw [Finset.sum_congr rfl (fun v _ => epsEtaSummand_eq v), Finset.sum_neg_distrib, h] | ||
|
|
||
| set_option backward.isDefEq.respectTransparency false in | ||
| lemma unitTensor_down_repr {d : ℕ} |
There was a problem hiding this comment.
This should be moved to the unitTensor file
| exact Fintype.sum_equiv (Equiv.arrowCongr (Equiv.refl (Fin 4)) | ||
| (finSumFinEquiv : (Fin 1 ⊕ Fin 3) ≃ Fin 4)) _ _ (fun _ => rfl) | ||
|
|
||
| lemma prod_eta_diag_of_injective {v : Fin 4 → Fin 1 ⊕ Fin 3} (hv : Function.Injective v) : |
There was a problem hiding this comment.
Should be moved to the minkowskiMatrix file
| simp only [Fintype.sum_prod_type] | ||
| rfl | ||
|
|
||
| lemma sum_reindex_finSumFinEquiv {M : Type} [AddCommMonoid M] (F : (Fin 4 → Fin 4) → M) : |
There was a problem hiding this comment.
This is not likely needed as a sperate lemma, similar with a lot of otherr small definitions here.
| rw [IsReindexing.inv_equiv_symm_eq, ← Fin.append_succAbove_const_eq_cycleIcc i, | ||
| Fin.append_right] | ||
|
|
||
| lemma metricTensor_repr_apply {d : ℕ} (cc : Color) |
There was a problem hiding this comment.
MOve e.g. to the metricTensor file
| simp only [basisIdxCongr_eq_refl, Equiv.refl_apply] | ||
| exact congrArg b (IsReindexing.inv_id_eq _ _) | ||
|
|
||
| lemma crossToSlot_basis_repr {d nA : ℕ} {c : Fin (nA+1) → Color} {cM : Fin 2 → Color} |
|
awaiting-author |
github-actions
Bot
added
the
awaiting-author
|
(May also help to split this PR up into smaller bits each touching a single file) |
|
Thanks for the review. I have reorganized the proof around the owning APIs in
The exact one-sum and Kronecker/Minkowski formulas are specific to the real Lorentz bases. Putting those statements directly in the generic tensor files would either create an import cycle or require basis/contraction compatibility not present in The two headline theorem statements are unchanged. The targeted build, full -awaiting-author |
github-actions
Bot
removed
the
awaiting-author
| private lemma section_chain {cA cB : Fin 4 → Color} | ||
| (h1 : (0 : Fin (0+1+1)) ≠ 1) (h2 : (1 : Fin (2+1+1)) ≠ 3) | ||
| (h3 : (2 : Fin (4+1+1)) ≠ 5) (h4 : (3 : Fin (6+1+1)) ≠ 7) | ||
| (x x1 x2 x3 : Fin 1 ⊕ Fin 3) : | ||
| ((ofFinEquiv (S := realLorentzTensor 3) (c := Fin.append cA cB) h4 | ||
| ((ofFinEquiv h3 | ||
| ((ofFinEquiv h2 | ||
| ((ofFinEquiv h1 (fun j => j.elim0) (x, x)).1) (x1, x1)).1) (x2, x2)).1) | ||
| (x3, x3)).1 : Fin (6+1+1) → Fin 1 ⊕ Fin 3) | ||
| = ![x, x1, x2, x3, x, x1, x2, x3] := by | ||
| funext m | ||
| fin_cases m <;> rfl | ||
|
|
||
| private lemma prod_fst_vec {cA cB : Fin 4 → Color} (y0 y1 y2 y3 y4 y5 y6 y7 : Fin 1 ⊕ Fin 3) : | ||
| (((ComponentIdx.prod (S := realLorentzTensor 3) (c := cA) (c1 := cB)) | ||
| (![y0,y1,y2,y3,y4,y5,y6,y7] : Fin (4+4) → Fin 1 ⊕ Fin 3)).1 : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) = ![y0,y1,y2,y3] := by | ||
| funext m; fin_cases m <;> rfl | ||
|
|
||
| private lemma prod_snd_vec {cA cB : Fin 4 → Color} (y0 y1 y2 y3 y4 y5 y6 y7 : Fin 1 ⊕ Fin 3) : | ||
| (((ComponentIdx.prod (S := realLorentzTensor 3) (c := cA) (c1 := cB)) | ||
| (![y0,y1,y2,y3,y4,y5,y6,y7] : Fin (4+4) → Fin 1 ⊕ Fin 3)).2 : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) = ![y4,y5,y6,y7] := by | ||
| funext m; fin_cases m <;> rfl | ||
|
|
||
| section Nest | ||
| variable (x x1 x2 x3 y0 y1 y2 y3 : Fin 1 ⊕ Fin 3) | ||
|
|
||
| private lemma nest3 : (Fin.insertNth (3 : Fin (3+1)) y3 | ||
| (fun m => ![x, x1, x2, x3] (Fin.succAbove 3 m)) : Fin 4 → Fin 1 ⊕ Fin 3) | ||
| = ![x, x1, x2, y3] := by | ||
| funext m; fin_cases m <;> rfl | ||
|
|
||
| private lemma nest2 : (Fin.insertNth (2 : Fin (3+1)) y2 | ||
| (fun m => (![x, x1, x2, y3] : Fin 4 → Fin 1 ⊕ Fin 3) (Fin.succAbove 2 m)) : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) = ![x, x1, y2, y3] := by | ||
| funext m; fin_cases m <;> rfl | ||
|
|
||
| private lemma nest1 : (Fin.insertNth (1 : Fin (3+1)) y1 | ||
| (fun m => (![x, x1, y2, y3] : Fin 4 → Fin 1 ⊕ Fin 3) (Fin.succAbove 1 m)) : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) = ![x, y1, y2, y3] := by | ||
| funext m; fin_cases m <;> rfl | ||
|
|
||
| private lemma nest0 : (Fin.insertNth (0 : Fin (3+1)) y0 | ||
| (fun m => (![x, y1, y2, y3] : Fin 4 → Fin 1 ⊕ Fin 3) (Fin.succAbove 0 m)) : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) = ![y0, y1, y2, y3] := by | ||
| funext m; fin_cases m <;> rfl | ||
|
|
||
| end Nest | ||
|
|
||
| private lemma vec4_0 {a b c e : Fin 1 ⊕ Fin 3} : | ||
| (![a,b,c,e] : Fin 4 → Fin 1 ⊕ Fin 3) 0 = a := rfl | ||
| private lemma vec4_1 {a b c e : Fin 1 ⊕ Fin 3} : | ||
| (![a,b,c,e] : Fin 4 → Fin 1 ⊕ Fin 3) 1 = b := rfl | ||
| private lemma vec4_2 {a b c e : Fin 1 ⊕ Fin 3} : | ||
| (![a,b,c,e] : Fin 4 → Fin 1 ⊕ Fin 3) 2 = c := rfl | ||
| private lemma vec4_3 {a b c e : Fin 1 ⊕ Fin 3} : | ||
| (![a,b,c,e] : Fin 4 → Fin 1 ⊕ Fin 3) 3 = e := rfl | ||
|
|
||
| private lemma sum_mul_eta {d : ℕ} (f : (Fin 1 ⊕ Fin d) → ℝ) (y : Fin 1 ⊕ Fin d) : | ||
| ∑ z : Fin 1 ⊕ Fin d, f z * minkowskiMatrix z y = f y * minkowskiMatrix y y := by | ||
| change (f ᵥ* minkowskiMatrix) y = _ | ||
| rw [minkowskiMatrix.vecMul_apply] | ||
|
|
||
| /-- Bundling four independent basis indices into one component index. -/ | ||
| private def vec4Equiv : | ||
| ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) | ||
| ≃ (Fin 4 → Fin 1 ⊕ Fin 3) where | ||
| toFun p := ![p.1, p.2.1, p.2.2.1, p.2.2.2] | ||
| invFun v := (v 0, v 1, v 2, v 3) | ||
| left_inv p := rfl | ||
| right_inv v := by funext m; fin_cases m <;> rfl | ||
|
|
||
| /-- Bundling three independent basis indices into one component index. -/ | ||
| private def vec3Equiv : | ||
| ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≃ (Fin 3 → Fin 1 ⊕ Fin 3) where | ||
| toFun p := ![p.1, p.2.1, p.2.2] | ||
| invFun v := (v 0, v 1, v 2) | ||
| left_inv p := rfl | ||
| right_inv v := by funext m; fin_cases m <;> rfl | ||
|
|
||
| private lemma sum4_eq {M : Type} [AddCommMonoid M] (F : (Fin 4 → Fin 1 ⊕ Fin 3) → M) : | ||
| ∑ x : Fin 1 ⊕ Fin 3, ∑ x1 : Fin 1 ⊕ Fin 3, ∑ x2 : Fin 1 ⊕ Fin 3, ∑ x3 : Fin 1 ⊕ Fin 3, | ||
| F ![x, x1, x2, x3] | ||
| = ∑ v : Fin 4 → Fin 1 ⊕ Fin 3, F v := by | ||
| rw [← Equiv.sum_comp vec4Equiv F] | ||
| simp only [Fintype.sum_prod_type] | ||
| rfl | ||
|
|
||
| open KroneckerDelta in | ||
| /-- Abbreviation for the summand of the fully contracted epsilon-epsilon sum. -/ | ||
| private noncomputable def epsEtaSummand (v : Fin 4 → Fin 1 ⊕ Fin 3) : ℝ := | ||
| ((generalizedKroneckerDelta (fun i => finSumFinEquiv (v i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ) * | ||
| (((generalizedKroneckerDelta (fun i => finSumFinEquiv (v i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ) | ||
| * minkowskiMatrix (v 0) (v 0) * minkowskiMatrix (v 1) (v 1) | ||
| * minkowskiMatrix (v 2) (v 2) * minkowskiMatrix (v 3) (v 3)) | ||
|
|
||
| open KroneckerDelta in | ||
| private lemma epsEtaSummand_eq (v : Fin 4 → Fin 1 ⊕ Fin 3) : epsEtaSummand v = | ||
| - (((generalizedKroneckerDelta (fun i => finSumFinEquiv (v i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ) | ||
| * ((generalizedKroneckerDelta (fun i => finSumFinEquiv (v i)) | ||
| (id : Fin 4 → Fin 4) : ℤ) : ℝ)) := by | ||
| rw [epsEtaSummand] | ||
| by_cases hA : generalizedKroneckerDelta (fun i => finSumFinEquiv (v i)) | ||
| (id : Fin 4 → Fin 4) = 0 | ||
| · rw [hA]; norm_num | ||
| · have hinj : Function.Injective (fun i => finSumFinEquiv (v i)) := by | ||
| by_contra hni | ||
| exact hA (leviCivitaSymbol_eq_zero_of_not_injective hni) | ||
| have hv : Function.Injective v := Function.Injective.of_comp hinj | ||
| have hp := minkowskiMatrix.prod_diagonal_comp_of_injective hv | ||
| rw [Fin.prod_univ_four] at hp | ||
| linear_combination | ||
| (((generalizedKroneckerDelta (fun i => finSumFinEquiv (v i)) | ||
| (id : Fin 4 → Fin 4) : ℤ) : ℝ) * | ||
| ((generalizedKroneckerDelta (fun i => finSumFinEquiv (v i)) | ||
| (id : Fin 4 → Fin 4) : ℤ) : ℝ)) * hp | ||
|
|
||
| open KroneckerDelta in | ||
| private lemma sum_epsEtaSummand : ∑ v : Fin 4 → Fin 1 ⊕ Fin 3, epsEtaSummand v = -24 := by | ||
| have hsum : ∑ v : Fin 4 → Fin 1 ⊕ Fin 3, | ||
| (generalizedKroneckerDelta (fun i => finSumFinEquiv (v i)) (id : Fin 4 → Fin 4) | ||
| * generalizedKroneckerDelta (fun i => finSumFinEquiv (v i)) | ||
| (id : Fin 4 → Fin 4) : ℤ) = 24 := by | ||
| calc | ||
| _ = ∑ g : Fin 4 → Fin 4, | ||
| generalizedKroneckerDelta g (id : Fin 4 → Fin 4) * | ||
| generalizedKroneckerDelta g (id : Fin 4 → Fin 4) := | ||
| Fintype.sum_equiv (Equiv.arrowCongr (Equiv.refl (Fin 4)) | ||
| (finSumFinEquiv : (Fin 1 ⊕ Fin 3) ≃ Fin 4)) _ _ (fun _ => rfl) | ||
| _ = 24 := sum_generalizedKroneckerDelta_mul_self | ||
| have h : (∑ v : Fin 4 → Fin 1 ⊕ Fin 3, | ||
| (((generalizedKroneckerDelta (fun i => finSumFinEquiv (v i)) | ||
| (id : Fin 4 → Fin 4) : ℤ) : ℝ) | ||
| * ((generalizedKroneckerDelta (fun i => finSumFinEquiv (v i)) | ||
| (id : Fin 4 → Fin 4) : ℤ) : ℝ))) = 24 := by | ||
| exact_mod_cast congrArg (fun z : ℤ => (z : ℝ)) hsum | ||
| rw [Finset.sum_congr rfl (fun v _ => epsEtaSummand_eq v), Finset.sum_neg_distrib, h] | ||
|
|
||
| open ComponentIdx.DropPairSection in | ||
| private lemma section_chain3 {cA cB : Fin 4 → Color} | ||
| (h1 : (0 : Fin (2+1+1)) ≠ 2) (h2 : (1 : Fin (4+1+1)) ≠ 4) (h3 : (2 : Fin (6+1+1)) ≠ 6) | ||
| (b : Fin 2 → Fin 1 ⊕ Fin 3) (x x1 x2 : Fin 1 ⊕ Fin 3) : | ||
| ((ofFinEquiv (S := realLorentzTensor 3) (c := Fin.append cA cB) h3 | ||
| ((ofFinEquiv h2 ((ofFinEquiv h1 b (x, x)).1) (x1, x1)).1) (x2, x2)).1 : | ||
| Fin (6+1+1) → Fin 1 ⊕ Fin 3) | ||
| = ![x, x1, x2, b 0, x, x1, x2, b 1] := by | ||
| funext m | ||
| fin_cases m <;> rfl | ||
|
|
||
| private lemma sum3_eq' {M : Type} [AddCommMonoid M] | ||
| (F : (Fin 1 ⊕ Fin 3) → (Fin 1 ⊕ Fin 3) → (Fin 1 ⊕ Fin 3) → M) : | ||
| ∑ x : Fin 1 ⊕ Fin 3, ∑ x1 : Fin 1 ⊕ Fin 3, ∑ x2 : Fin 1 ⊕ Fin 3, F x x1 x2 | ||
| = ∑ w : Fin 3 → Fin 1 ⊕ Fin 3, F (w 0) (w 1) (w 2) := by | ||
| rw [← Equiv.sum_comp vec3Equiv (fun w => F (w 0) (w 1) (w 2))] | ||
| simp only [Fintype.sum_prod_type] | ||
| rfl | ||
|
|
||
| open KroneckerDelta in | ||
| private lemma eps_eta_three (a b c y0 y1 : Fin 1 ⊕ Fin 3) : | ||
| ((generalizedKroneckerDelta (fun i => finSumFinEquiv ((![a,b,c,y0] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ) | ||
| * (((generalizedKroneckerDelta (fun i => finSumFinEquiv ((![a,b,c,y1] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ) | ||
| * minkowskiMatrix a a * minkowskiMatrix b b * minkowskiMatrix c c | ||
| * minkowskiMatrix y1 y1) | ||
| = - (((generalizedKroneckerDelta (fun i => finSumFinEquiv ((![a,b,c,y0] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ) | ||
| * ((generalizedKroneckerDelta (fun i => finSumFinEquiv ((![a,b,c,y1] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ)) := by | ||
| by_cases hA : generalizedKroneckerDelta (fun i => finSumFinEquiv ((![a,b,c,y1] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) = 0 | ||
| · rw [hA]; norm_num | ||
| · have hinj : Function.Injective | ||
| (fun i => finSumFinEquiv ((![a,b,c,y1] : Fin 4 → Fin 1 ⊕ Fin 3) i)) := by | ||
| by_contra hni | ||
| exact hA (leviCivitaSymbol_eq_zero_of_not_injective hni) | ||
| have hv : Function.Injective (![a,b,c,y1] : Fin 4 → Fin 1 ⊕ Fin 3) := | ||
| Function.Injective.of_comp hinj | ||
| have hp := minkowskiMatrix.prod_diagonal_comp_of_injective hv | ||
| rw [Fin.prod_univ_four] at hp | ||
| simp only [vec4_0, vec4_1, vec4_2, vec4_3] at hp | ||
| linear_combination | ||
| (((generalizedKroneckerDelta (fun i => finSumFinEquiv ((![a,b,c,y0] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ) * | ||
| ((generalizedKroneckerDelta (fun i => finSumFinEquiv ((![a,b,c,y1] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ)) * hp | ||
|
|
||
| open KroneckerDelta in | ||
| private lemma sum_eps_three (y0 y1 : Fin 1 ⊕ Fin 3) : | ||
| ∑ x : Fin 1 ⊕ Fin 3, ∑ x1 : Fin 1 ⊕ Fin 3, ∑ x2 : Fin 1 ⊕ Fin 3, | ||
| ((generalizedKroneckerDelta (fun i => finSumFinEquiv ((![x,x1,x2,y0] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ) | ||
| * (((generalizedKroneckerDelta (fun i => finSumFinEquiv ((![x,x1,x2,y1] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ) | ||
| * minkowskiMatrix x x * minkowskiMatrix x1 x1 * minkowskiMatrix x2 x2 | ||
| * minkowskiMatrix y1 y1) | ||
| = -6 * (if y0 = y1 then 1 else 0) := by | ||
| rw [Finset.sum_congr rfl fun x _ => Finset.sum_congr rfl fun x1 _ => | ||
| Finset.sum_congr rfl fun x2 _ => eps_eta_three x x1 x2 y0 y1] | ||
| simp only [Finset.sum_neg_distrib] | ||
| have hZ : ∑ x : Fin 1 ⊕ Fin 3, ∑ x1 : Fin 1 ⊕ Fin 3, ∑ x2 : Fin 1 ⊕ Fin 3, | ||
| (generalizedKroneckerDelta (fun i => finSumFinEquiv ((![x,x1,x2,y0] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) | ||
| * generalizedKroneckerDelta (fun i => finSumFinEquiv ((![x,x1,x2,y1] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4)) | ||
| = 6 * ((kroneckerDelta (finSumFinEquiv y0) (finSumFinEquiv y1) : ℕ) : ℤ) := by | ||
| rw [sum3_eq' (fun x x1 x2 => generalizedKroneckerDelta (fun i => | ||
| finSumFinEquiv ((![x, x1, x2, y0] : Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) | ||
| * generalizedKroneckerDelta (fun i => | ||
| finSumFinEquiv ((![x, x1, x2, y1] : Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4))] | ||
| have hs (y : Fin 1 ⊕ Fin 3) (w : Fin 3 → Fin 1 ⊕ Fin 3) : | ||
| (fun i => finSumFinEquiv | ||
| ((![w 0, w 1, w 2, y] : Fin 4 → Fin 1 ⊕ Fin 3) i)) = | ||
| Fin.snoc (fun i => finSumFinEquiv (w i)) (finSumFinEquiv y) := by | ||
| funext i | ||
| fin_cases i <;> rfl | ||
| rw [Finset.sum_congr rfl fun w _ => by rw [hs y0 w, hs y1 w]] | ||
| calc | ||
| _ = ∑ h : Fin 3 → Fin 4, | ||
| generalizedKroneckerDelta (Fin.snoc h (finSumFinEquiv y0)) id * | ||
| generalizedKroneckerDelta (Fin.snoc h (finSumFinEquiv y1)) id := | ||
| Fintype.sum_equiv (Equiv.arrowCongr (Equiv.refl (Fin 3)) | ||
| (finSumFinEquiv : (Fin 1 ⊕ Fin 3) ≃ Fin 4)) _ _ (fun _ => rfl) | ||
| _ = _ := sum_generalizedKroneckerDelta_mul_snoc _ _ | ||
| have hR : ∑ x : Fin 1 ⊕ Fin 3, ∑ x1 : Fin 1 ⊕ Fin 3, ∑ x2 : Fin 1 ⊕ Fin 3, | ||
| (((generalizedKroneckerDelta (fun i => finSumFinEquiv ((![x,x1,x2,y0] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ) | ||
| * ((generalizedKroneckerDelta (fun i => finSumFinEquiv ((![x,x1,x2,y1] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ)) | ||
| = 6 * (if y0 = y1 then 1 else 0) := by | ||
| have := congrArg (fun z : ℤ => (z : ℝ)) hZ | ||
| push_cast at this | ||
| rw [this] | ||
| by_cases hy : y0 = y1 | ||
| · rw [hy]; simp [KroneckerDelta.eq_one_of_same] | ||
| · rw [if_neg hy, KroneckerDelta.eq_zero_of_ne (fun hc => hy (finSumFinEquiv.injective hc))] | ||
| norm_num | ||
| rw [hR] | ||
| ring | ||
|
|
||
| open KroneckerDelta in | ||
| private lemma sum_eps_three' (y0 y1 : Fin 1 ⊕ Fin 3) : | ||
| ∑ x : Fin 1 ⊕ Fin 3, ∑ x1 : Fin 1 ⊕ Fin 3, ∑ x2 : Fin 1 ⊕ Fin 3, | ||
| ((generalizedKroneckerDelta (fun i => finSumFinEquiv ((![x,x1,x2,y0] : | ||
| Fin 4 → Fin 1 ⊕ Fin 3) i)) (id : Fin 4 → Fin 4) : ℤ) : ℝ) | ||
| * (((Tensor.basis ![Color.up, Color.up, Color.up, Color.up]).repr ε4) | ||
| (![x,x1,x2,y1] : Fin 4 → Fin 1 ⊕ Fin 3) | ||
| * minkowskiMatrix x x * minkowskiMatrix x1 x1 * minkowskiMatrix x2 x2 | ||
| * minkowskiMatrix y1 y1) | ||
| = -6 * (if y0 = y1 then 1 else 0) := by | ||
| rw [← sum_eps_three y0 y1] | ||
| refine Finset.sum_congr rfl fun x _ => Finset.sum_congr rfl fun x1 _ => | ||
| Finset.sum_congr rfl fun x2 _ => ?_ | ||
| rw [leviCivita_basis_repr_apply] |
There was a problem hiding this comment.
With all of these lemmas: I think the following needs to be done:
- Rephrase them as API around objects that already exist.
- Move them to the corresponding file
- Or if they a small one-line proofs remove them entirely.
The point is that they do not tell a good story, about what they are and why they are there. i understand they are needed for the calculation, but I think it is always possible to do such a reframing.
Maybe one idea is to reframe this whole file as a series of different forms of ε4 | μ ν ρ σ ⊗ ε4 | τ(μ) τ(ν) τ(ρ) τ(τ) each getting simplier?
There was a problem hiding this comment.
Think this lemma should go next to CrossToSlot definition, or we move CrossToSlot here.
|
awaiting-author |
github-actions
Bot
added
the
awaiting-author
|
The other alternative to these PRs is that we could add them to PhyslibAlpha, so we have them, and then could leave the tidying for the future |
Thanks! I’m working through the new review comments now. I’ll first try to rework the proofs around the existing tensor APIs and make the intermediate results mathematically useful. No problem on PhyslibAlpha if you prefer as well. |
ab91a43 to
b671683
Compare
|
I made another pass and pushed the revision at b671683.
The old private helper forest and separate real CrossToSlot module are gone, for a net reduction of 106 lines from the previous head. I also rebased onto current master, including #1567, and reran the builds and linters. |
github-actions
Bot
removed
the
awaiting-author
| ∑ h : Fin 3 → Fin 4, | ||
| generalizedKroneckerDelta (Fin.snoc h σ) id * |
There was a problem hiding this comment.
Could be collapsed to one line. I think you should check for all of these throughout both your pull requests
|
|
||
| /-- Away from the two restored positions, `ofFinEquiv` agrees with the original | ||
| component index. -/ | ||
| lemma ofFinEquiv_apply_succSuccAbove {n : ℕ} {c : Fin (n + 1 + 1) → C} |
There was a problem hiding this comment.
This is a single rewriting of a lemma that already exists so I just wouldn't define it and use the definition wherever you use this lemma
| norm_num | ||
|
|
||
| open ComponentIdx.DropPairSection in | ||
| private lemma contractFour_route {cA cB : Fin 4 → Color} |
There was a problem hiding this comment.
Might be nice to put this as a nonprofit lemma near ofFinEquiv
| apply Prod.ext <;> funext m <;> fin_cases m <;> rfl | ||
|
|
||
| open ComponentIdx.DropPairSection in | ||
| private lemma contractThree_route {cA cB : Fin 4 → Color} |
There was a problem hiding this comment.
Put near ComponentIdx.prod
| private def vec4Equiv {X : Type} : (X × X × X × X) ≃ (Fin 4 → X) where | ||
| toFun p := ![p.1, p.2.1, p.2.2.1, p.2.2.2] | ||
| invFun v := (v 0, v 1, v 2, v 3) | ||
| left_inv p := rfl | ||
| right_inv v := by funext m; fin_cases m <;> rfl | ||
|
|
||
| /-- Bundling three independent basis indices into one component index. -/ | ||
| private def vec3Equiv {X : Type} : (X × X × X) ≃ (Fin 3 → X) where | ||
| toFun p := ![p.1, p.2.1, p.2.2] | ||
| invFun v := (v 0, v 1, v 2) | ||
| left_inv p := rfl | ||
| right_inv v := by funext m; fin_cases m <;> rfl | ||
|
|
||
| private lemma sum4_eq {M X : Type} [Fintype X] [AddCommMonoid M] (F : (Fin 4 → X) → M) : | ||
| ∑ x0 : X, ∑ x1 : X, ∑ x2 : X, ∑ x3 : X, F ![x0, x1, x2, x3] | ||
| = ∑ v : Fin 4 → X, F v := by | ||
| rw [← Equiv.sum_comp vec4Equiv F] | ||
| simp only [Fintype.sum_prod_type] | ||
| rfl | ||
|
|
||
| private lemma sum3_eq {M X : Type} [Fintype X] [AddCommMonoid M] (F : (Fin 3 → X) → M) : | ||
| ∑ x0 : X, ∑ x1 : X, ∑ x2 : X, F ![x0, x1, x2] = ∑ h, F h := by | ||
| rw [← Equiv.sum_comp vec3Equiv F] | ||
| simp only [Fintype.sum_prod_type] | ||
| rfl |
There was a problem hiding this comment.
I still really think these lemmas are not needed. Most of them are just three lines. Even just including them within the actual theorems of content, I think, will produce a cleaner file.
|
I think after these changes, things are starting to look a lot better and we may be able to just go PhysLib. I still think there are a couple of lemmas that you can remove, especially the private ones, but I think we're almost there. Maybe just a couple more iterations with you, if that's okay. |
jstoobysmith
added
the
awaiting-author
Move reusable contraction, metric, unit, Minkowski, and Kronecker component lemmas into their owning modules. Keep the finite-index proof scaffolding private and the headline identities in LeviCivita/Contractions.
b671683 to
a940832
Compare
|
Sounds good with me, I pushed the following:
|
|
-awaiting-author |
2 participants
Proves the two remaining epsilon-epsilon identities for the Lorentzian Levi-Civita tensor,
leviCivita_contract_selfandleviCivita_contract_three, left as stated goals in #1348. Bothstatements are unchanged.
The route is through components. Both sides are compared under
(Tensor.basis _).reprand thecontractions collapse to finite sums over
Fin 1 ⊕ Fin 3, where the product of two symbols is ageneralizedKroneckerDeltaand the contraction machinery from #1335 gives the 24 and the 6. Thesign comes out of the metric: when the symbol is nonzero the index map is injective, hence a
bijection on a four-element type, so the four diagonal metric factors multiply to the determinant,
which is minus one in this signature.
Two component lemmas that did not exist before carry the argument and may be useful beyond it:
toDualMapAtIndex_basis_repr, the basis representation of index lowering, andunitTensor_down_repr, the basis representation of the unit tensor of color down. The rest of thenew material is rank-four bookkeeping for this file.
The proofs elaborate within the default heartbeat budget, so no
maxHeartbeatsoption is needed.The
nolint checkTypeonleviCivita_contract_selfstays: that linter re-typechecks the statement,which this change does not alter, and its comment now names the current toolchain. The Tensors API
map entry for these identities is flipped to done with a real location.
One question on placement. The two component lemmas would sit naturally next to their definitions,
toDualMapAtIndex_basis_reprin Dual.lean in particular, rather than in this file. I kepteverything local so the diff stays reviewable, and can move them wherever you prefer, here or in a
follow-up.