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

refactor: Style Lint

Browse source
This commit is contained in:
jstoobysmith 2024-12-19 12:59:14 +00:00
parent aad3afd3a7
commit 63c4cabdf4
9 changed files with 512 additions and 453 deletions
Download patch file Download diff file Expand all files Collapse all files

19
HepLean/Mathematics/Fin.lean
View file

@ -244,7 +244,7 @@ lemma finExtractOne_apply_neq {n : ℕ} (i j : Fin n.succ.succ) (hij : i ≠ j)
finExtractOne i j = Sum.inr (predAboveI i j) := by
symm
apply (Equiv.symm_apply_eq _).mp ?_
simp
simp only [Nat.succ_eq_add_one, finExtractOne_symm_inr_apply]
exact succsAbove_predAboveI hij
/-- Given an equivalence `Fin n.succ.succ ≃ Fin n.succ.succ`, and an `i : Fin n.succ.succ`,
@ -252,7 +252,8 @@ lemma finExtractOne_apply_neq {n : ℕ} (i j : Fin n.succ.succ) (hij : i ≠ j)
def finExtractOnPermHom {m : ℕ} (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin m.succ.succ) :
Fin n.succ → Fin m.succ := fun x => predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x)))
lemma finExtractOnPermHom_inv {m : ℕ} (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin m.succ.succ) :
lemma finExtractOnPermHom_inv {m : ℕ} (i : Fin n.succ.succ)
(σ : Fin n.succ.succ ≃ Fin m.succ.succ) :
(finExtractOnPermHom (σ i) σ.symm) ∘ (finExtractOnPermHom i σ) = id := by
funext x
simp only [Nat.succ_eq_add_one, Function.comp_apply, finExtractOnPermHom, Equiv.symm_apply_apply,
@ -287,13 +288,15 @@ def finExtractOnePerm {m : ℕ} (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃
right_inv x := by
simpa using congrFun (finExtractOnPermHom_inv (σ i) σ.symm) x
lemma finExtractOnePerm_equiv {n m : ℕ} (e : Fin n.succ.succ ≃ Fin m.succ.succ) (i : Fin n.succ.succ) :
e ∘ i.succAbove = (e i).succAbove ∘ finExtractOnePerm i e := by
simp [finExtractOnePerm]
lemma finExtractOnePerm_equiv {n m : ℕ} (e : Fin n.succ.succ ≃ Fin m.succ.succ)
(i : Fin n.succ.succ) :
e ∘ i.succAbove = (e i).succAbove ∘ finExtractOnePerm i e := by
simp only [Nat.succ_eq_add_one, finExtractOnePerm, Equiv.coe_fn_mk]
funext x
simp [finExtractOnPermHom]
simp only [Function.comp_apply, finExtractOnPermHom, Nat.succ_eq_add_one,
finExtractOne_symm_inr_apply]
rw [succsAbove_predAboveI]
simp
simp only [Nat.succ_eq_add_one, ne_eq, EmbeddingLike.apply_eq_iff_eq]
exact Fin.ne_succAbove i x
@[simp]
@ -437,7 +440,7 @@ lemma equivCons_succ {n m : ℕ} (e : Fin n ≃ Fin m) (i : ℕ) (hi : i + 1 < n
simp only [Nat.succ_eq_add_one, equivCons, Equiv.toFun_as_coe, Equiv.invFun_as_coe,
Equiv.coe_fn_symm_mk]
have hi : ⟨i + 1, hi⟩ = Fin.succ ⟨i, Nat.succ_lt_succ_iff.mp hi⟩ := by rfl
simp
simp only [Equiv.coe_fn_mk]
rw [hi]
rw [Fin.cons_succ]
rfl

344
HepLean/Mathematics/List.lean
View file

@ -14,78 +14,82 @@ open Fin
open HepLean
variable {n : Nat}
lemma takeWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
lemma takeWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
(l : List I) → (i : ℕ) → (hi : ∀ (i j : Fin l.length), i < j → P (l.get j) → P (l.get i)) →
List.takeWhile P (List.eraseIdx l i) = (List.takeWhile P l).eraseIdx i
| [], _, h => by
simp
rfl
| a :: [], 0, h => by
simp [List.takeWhile]
simp only [List.takeWhile, List.eraseIdx_zero, List.nil_eq]
split
next x heq => simp_all only [decide_eq_true_eq, List.tail_cons]
next x heq => simp_all only [decide_eq_false_iff_not, List.tail_nil]
| a :: [], Nat.succ n , h => by
simp
rw [List.eraseIdx_of_length_le ]
· rfl
· rfl
| a :: [], Nat.succ n, h => by
simp only [Nat.succ_eq_add_one, List.eraseIdx_cons_succ, List.eraseIdx_nil]
rw [List.eraseIdx_of_length_le]
have h1 : (List.takeWhile P [a]).length ≤ [a].length :=
List.Sublist.length_le (List.takeWhile_sublist _)
simp at h1
simp only [List.length_singleton] at h1
omega
| a :: b :: l, 0, h => by
simp [List.takeWhile]
simp only [List.takeWhile, List.eraseIdx_zero]
by_cases hPb : P b
· have hPa : P a := by
simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp [Fin.lt_def]) (by simpa using hPb)
simp [hPb, hPa]
· simp [hPb]
· simp only [hPb, decide_False, List.nil_eq]
simp_all only [List.length_cons, List.get_eq_getElem]
split
next x heq => simp_all only [decide_eq_true_eq, List.tail_cons]
next x heq => simp_all only [decide_eq_false_iff_not, List.tail_nil]
· rfl
· rfl
| a :: b :: l, Nat.succ n, h => by
simp
simp only [Nat.succ_eq_add_one, List.eraseIdx_cons_succ]
by_cases hPa : P a
· dsimp [List.takeWhile]
simp [hPa]
simp only [hPa, decide_True, List.eraseIdx_cons_succ, List.cons.injEq, true_and]
rw [takeWile_eraseIdx]
rfl
intro i j hij hP
simpa using h (Fin.succ i) (Fin.succ j) (by simpa using hij) (by simpa using hP)
simpa using h (Fin.succ i) (Fin.succ j) (by simpa using hij) (by simpa using hP)
· simp [hPa]
lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
(l : List I) → (i : ℕ) → (hi : ∀ (i j : Fin l.length), i < j → P (l.get j) → P (l.get i)) →
List.dropWhile P (List.eraseIdx l i) =
if (List.takeWhile P l).length ≤ i then
if (List.takeWhile P l).length ≤ i then
(List.dropWhile P l).eraseIdx (i - (List.takeWhile P l).length)
else (List.dropWhile P l)
| [], _, h => by
simp
| a :: [], 0, h => by
simp [List.dropWhile]
simp_all only [List.length_singleton, List.get_eq_getElem, Fin.val_eq_zero, List.getElem_cons_zero, implies_true,
decide_True, decide_False, List.tail_cons, ite_self]
| a :: [], Nat.succ n , h => by
simp [List.dropWhile, List.takeWhile]
rw [List.eraseIdx_of_length_le ]
simp_all only [List.length_singleton, List.get_eq_getElem, Fin.val_eq_zero, List.getElem_cons_zero, implies_true,
ite_self]
simp_all only [List.length_singleton, List.get_eq_getElem, Fin.val_eq_zero, List.getElem_cons_zero, implies_true]
simp only [List.dropWhile, nonpos_iff_eq_zero, List.length_eq_zero, List.takeWhile_eq_nil_iff,
List.length_singleton, zero_lt_one, Fin.zero_eta, Fin.isValue, List.get_eq_getElem,
Fin.val_eq_zero, List.getElem_cons_zero, decide_eq_true_eq, forall_const, zero_le,
Nat.sub_eq_zero_of_le, List.eraseIdx_zero, ite_not, List.nil_eq]
simp_all only [List.length_singleton, List.get_eq_getElem, Fin.val_eq_zero,
List.getElem_cons_zero, implies_true, decide_True, decide_False, List.tail_cons, ite_self]
| a :: [], Nat.succ n, h => by
simp only [List.dropWhile, List.eraseIdx_nil, List.takeWhile, Nat.succ_eq_add_one]
rw [List.eraseIdx_of_length_le]
simp_all only [List.length_singleton, List.get_eq_getElem, Fin.val_eq_zero,
List.getElem_cons_zero, implies_true, ite_self]
simp_all only [List.length_singleton, List.get_eq_getElem, Fin.val_eq_zero,
List.getElem_cons_zero, implies_true]
split
next x heq =>
simp_all only [decide_eq_true_eq, List.length_nil, List.length_singleton, add_tsub_cancel_right, zero_le]
simp_all only [decide_eq_true_eq, List.length_nil, List.length_singleton,
add_tsub_cancel_right, zero_le]
next x heq =>
simp_all only [decide_eq_false_iff_not, List.length_singleton, List.length_nil, tsub_zero,
le_add_iff_nonneg_left, zero_le]
| a :: b :: l, 0, h => by
simp [List.takeWhile, List.dropWhile]
simp only [List.dropWhile, List.takeWhile, nonpos_iff_eq_zero, List.length_eq_zero, zero_le,
Nat.sub_eq_zero_of_le, List.eraseIdx_zero]
by_cases hPb : P b
· have hPa : P a := by
simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp [Fin.lt_def]) (by simpa using hPb)
simp [hPb, hPa]
· simp [hPb]
· simp only [hPb, decide_False, nonpos_iff_eq_zero, List.length_eq_zero]
simp_all only [List.length_cons, List.get_eq_getElem]
simp_all only [decide_False, nonpos_iff_eq_zero, List.length_eq_zero]
split
@ -93,29 +97,32 @@ lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
simp_all only [nonpos_iff_eq_zero, List.length_eq_zero]
split
next x heq => simp_all only [List.cons_ne_self]
next x heq => simp_all only [decide_eq_false_iff_not, List.tail_cons]
· rfl
next h_1 =>
simp_all only [nonpos_iff_eq_zero, List.length_eq_zero]
split
next x heq => simp_all only [List.cons_ne_self, not_false_eq_true, decide_eq_true_eq]
next x heq => rfl
next x heq => simp_all only [not_true_eq_false]
| a :: b :: l, Nat.succ n, h => by
simp
simp only [Nat.succ_eq_add_one, List.eraseIdx_cons_succ]
by_cases hPb : P b
· have hPa : P a := by
simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp [Fin.lt_def]) (by simpa using hPb)
simp [List.takeWhile, List.dropWhile, hPb, hPa]
simp only [List.dropWhile, hPa, decide_True, List.takeWhile, hPb, List.length_cons,
add_le_add_iff_right, Nat.reduceSubDiff]
rw [dropWile_eraseIdx]
simp_all only [List.length_cons, List.get_eq_getElem, decide_True, List.takeWhile_cons_of_pos,
List.dropWhile_cons_of_pos]
intro i j hij hP
simpa using h (Fin.succ i) (Fin.succ j) (by simpa using hij) (by simpa using hP)
· simp [List.takeWhile, List.dropWhile, hPb]
intro i j hij hP
simpa using h (Fin.succ i) (Fin.succ j) (by simpa using hij) (by simpa using hP)
· simp only [List.dropWhile, List.takeWhile, hPb, decide_False]
by_cases hPa : P a
· rw [dropWile_eraseIdx]
simp [hPa, List.dropWhile, hPb]
simp only [hPa, decide_True, hPb, decide_False, Bool.false_eq_true, not_false_eq_true,
List.takeWhile_cons_of_neg, List.length_nil, zero_le, ↓reduceIte, List.dropWhile,
tsub_zero, List.length_singleton, le_add_iff_nonneg_left, add_tsub_cancel_right]
intro i j hij hP
simpa using h (Fin.succ i) (Fin.succ j) (by simpa using hij) (by simpa using hP)
simpa using h (Fin.succ i) (Fin.succ j) (by simpa using hij) (by simpa using hP)
· simp [hPa]
def orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
@ -137,49 +144,49 @@ lemma orderedInsertPos_lt_length {I : Type} (le1 : I → I → Prop) [DecidableR
lemma orderedInsert_get_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
(List.orderedInsert le1 r0 r)[(orderedInsertPos le1 r r0).val] = r0 := by
simp [orderedInsertPos, List.orderedInsert_eq_take_drop]
simp only [List.orderedInsert_eq_take_drop, decide_not, orderedInsertPos]
rw [List.getElem_append]
simp
@[simp]
lemma orderedInsert_eraseIdx_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
(List.orderedInsert le1 r0 r).eraseIdx ↑(orderedInsertPos le1 r r0) = r := by
(List.orderedInsert le1 r0 r).eraseIdx ↑(orderedInsertPos le1 r r0) = r := by
simp only [List.orderedInsert_eq_take_drop]
rw [List.eraseIdx_append_of_length_le]
· simp [orderedInsertPos]
· simp [orderedInsertPos]
· rfl
lemma orderedInsertPos_cons {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
lemma orderedInsertPos_cons {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 r1 : I) :
(orderedInsertPos le1 (r1 ::r) r0).val =
if le1 r0 r1 then ⟨0, by simp⟩ else (Fin.succ (orderedInsertPos le1 r r0)) := by
simp [orderedInsertPos, List.takeWhile]
simp only [List.orderedInsert.eq_2, orderedInsertPos, List.takeWhile, decide_not, Fin.zero_eta,
Fin.succ_mk]
by_cases h : le1 r0 r1
· simp [h]
· simp [h]
lemma orderedInsertPos_sigma {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(le1 : I → I → Prop) [DecidableRel le1] (l : List (Σ i, f i))
(k : I) (a : f k) :
(k : I) (a : f k) :
(orderedInsertPos (fun (i j : Σ i, f i) => le1 i.1 j.1) l ⟨k, a⟩).1 =
(orderedInsertPos le1 (List.map (fun (i : Σ i, f i) => i.1) l) k).1 := by
simp [orderedInsertPos]
simp only [orderedInsertPos, decide_not]
induction l with
| nil =>
simp
| cons a l ih =>
simp [List.takeWhile]
simp only [List.takeWhile]
obtain ⟨fst, snd⟩ := a
simp_all only
split
next x heq =>
simp_all only [Bool.not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, List.length_cons, decide_False,
Bool.not_false]
simp_all only [Bool.not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not,
List.length_cons, decide_False, Bool.not_false]
next x heq =>
simp_all only [Bool.not_eq_eq_eq_not, Bool.not_false, decide_eq_true_eq, List.length_nil, decide_True,
Bool.not_true]
simp_all only [Bool.not_eq_eq_eq_not, Bool.not_false, decide_eq_true_eq, List.length_nil,
decide_True, Bool.not_true]
@[simp]
lemma orderedInsert_get_lt {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
@ -190,10 +197,10 @@ lemma orderedInsert_get_lt {I : Type} (le1 : I → I → Prop) [DecidableRel le1
have h1 : (List.takeWhile (fun b => decide ¬le1 r0 b) r).length ≤ r.length :=
List.Sublist.length_le (List.takeWhile_sublist fun b => decide ¬le1 r0 b)
omega⟩ := by
simp [orderedInsertPos] at hi
simp [List.orderedInsert_eq_take_drop]
simp only [orderedInsertPos, decide_not] at hi
simp only [List.orderedInsert_eq_take_drop, decide_not, List.get_eq_getElem]
rw [List.getElem_append]
simp [hi]
simp only [hi, ↓reduceDIte]
rw [List.IsPrefix.getElem]
exact List.takeWhile_prefix fun b => !decide (le1 r0 b)
@ -203,19 +210,18 @@ lemma orderedInsertPos_take_orderedInsert {I : Type} (le1 : I → I → Prop) [D
List.takeWhile (fun b => decide ¬le1 r0 b) r := by
simp [orderedInsertPos, List.orderedInsert_eq_take_drop]
lemma orderedInsertPos_take_eq_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
List.take (orderedInsertPos le1 r r0) r =
List.take (orderedInsertPos le1 r r0) (List.orderedInsert le1 r0 r) := by
refine List.ext_get ?_ ?_
· simp
exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le1 r r0 )
refine List.ext_get ?_ ?_
· simp only [List.length_take, Fin.is_le', inf_of_le_left, inf_eq_left]
exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le1 r r0)
· intro n h1 h2
simp
simp only [List.get_eq_getElem, List.getElem_take]
erw [orderedInsert_get_lt le1 r r0 n]
rfl
simp at h1
simp only [List.length_take, lt_inf_iff] at h1
exact h1.1
lemma orderedInsertPos_drop_eq_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
@ -223,7 +229,8 @@ lemma orderedInsertPos_drop_eq_orderedInsert {I : Type} (le1 : I → I → Prop)
List.drop (orderedInsertPos le1 r r0) r =
List.drop (orderedInsertPos le1 r r0).succ (List.orderedInsert le1 r0 r) := by
conv_rhs => simp [orderedInsertPos, List.orderedInsert_eq_take_drop]
have hr : r = List.takeWhile (fun b => !decide (le1 r0 b)) r ++ List.dropWhile (fun b => !decide (le1 r0 b)) r := by
have hr : r = List.takeWhile (fun b => !decide (le1 r0 b)) r ++
List.dropWhile (fun b => !decide (le1 r0 b)) r := by
exact Eq.symm (List.takeWhile_append_dropWhile (fun b => !decide (le1 r0 b)) r)
conv_lhs =>
rhs
@ -243,26 +250,27 @@ lemma orderedInsertPos_drop {I : Type} (le1 : I → I → Prop) [DecidableRel le
rw [orderedInsertPos_drop_eq_orderedInsert]
simp [orderedInsertPos, List.orderedInsert_eq_take_drop]
lemma orderedInsertPos_succ_take_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
lemma orderedInsertPos_succ_take_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
(List.take (orderedInsertPos le1 r r0).succ (List.orderedInsert le1 r0 r)) =
List.takeWhile (fun b => decide ¬le1 r0 b) r ++ [r0] := by
List.takeWhile (fun b => decide ¬le1 r0 b) r ++ [r0] := by
simp [orderedInsertPos, List.orderedInsert_eq_take_drop, List.take_append_eq_append_take]
lemma lt_orderedInsertPos_rel {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r0 : I) (r : List I) (n : Fin r.length)
(r0 : I) (r : List I) (n : Fin r.length)
(hn : n.val < (orderedInsertPos le1 r r0).val) : ¬ le1 r0 (r.get n) := by
have htake : r.get n ∈ List.take (orderedInsertPos le1 r r0) r := by
rw [@List.mem_take_iff_getElem]
use n
simp
simp only [List.get_eq_getElem, lt_inf_iff, Fin.is_lt, and_true, exists_prop]
exact hn
rw [orderedInsertPos_take] at htake
have htake' := List.mem_takeWhile_imp htake
simpa using htake'
lemma gt_orderedInsertPos_rel {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
[IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) (hs : List.Sorted le1 r) (n : Fin r.length)
[IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) (hs : List.Sorted le1 r)
(n : Fin r.length)
(hn : ¬ n.val < (orderedInsertPos le1 r r0).val) : le1 r0 (r.get n) := by
have hrsSorted : List.Sorted le1 (List.orderedInsert le1 r0 r) :=
List.Sorted.orderedInsert r0 r hs
@ -278,7 +286,6 @@ lemma gt_orderedInsertPos_rel {I : Type} (le1 : I → I → Prop) [DecidableRel
congr
omega
lemma orderedInsert_eraseIdx_lt_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) (i : ℕ)
(hi : i < orderedInsertPos le1 r r0)
@ -291,10 +298,10 @@ lemma orderedInsert_eraseIdx_lt_orderedInsertPos {I : Type} (le1 : I → I → P
· rw [takeWile_eraseIdx]
exact hr
· rw [dropWile_eraseIdx]
simp [orderedInsertPos] at hi
simp only [orderedInsertPos, decide_not] at hi
have hi' : ¬ (List.takeWhile (fun b => !decide (le1 r0 b)) r).length ≤ ↑i := by
omega
simp [hi']
simp only [decide_not, hi', ↓reduceIte]
exact fun i j a a_1 => hr i j a a_1
· exact hi
@ -302,15 +309,16 @@ lemma orderedInsert_eraseIdx_orderedInsertPos_le {I : Type} (le1 : I → I → P
(r : List I) (r0 : I) (i : ℕ)
(hi : orderedInsertPos le1 r r0 ≤ i)
(hr : ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)) :
(List.orderedInsert le1 r0 r).eraseIdx (Nat.succ i) = List.orderedInsert le1 r0 (r.eraseIdx i) := by
(List.orderedInsert le1 r0 r).eraseIdx (Nat.succ i) =
List.orderedInsert le1 r0 (r.eraseIdx i) := by
conv_lhs => simp only [List.orderedInsert_eq_take_drop]
rw [List.eraseIdx_append_of_length_le]
· simp only [List.orderedInsert_eq_take_drop]
congr 1
· rw [takeWile_eraseIdx]
rw [List.eraseIdx_of_length_le]
simp [orderedInsertPos] at hi
simp
simp only [orderedInsertPos, decide_not] at hi
simp only [decide_not]
omega
exact hr
· simp only [Nat.succ_eq_add_one]
@ -328,12 +336,13 @@ lemma orderedInsert_eraseIdx_orderedInsertPos_le {I : Type} (le1 : I → I → P
· simp only [orderedInsertPos] at hi
omega
def orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
def orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
Fin (r0 :: r).length ≃ Fin (List.orderedInsert le1 r0 r).length := by
let e2 : Fin (List.orderedInsert le1 r0 r).length ≃ Fin (r0 :: r).length :=
(Fin.castOrderIso (List.orderedInsert_length le1 r r0)).toEquiv
let e3 : Fin (r0 :: r).length ≃ Fin 1 ⊕ Fin (r).length := finExtractOne 0
let e4 : Fin (r0 :: r).length ≃ Fin 1 ⊕ Fin (r).length := finExtractOne ⟨orderedInsertPos le1 r r0, orderedInsertPos_lt_length le1 r r0⟩
let e4 : Fin (r0 :: r).length ≃ Fin 1 ⊕ Fin (r).length :=
finExtractOne ⟨orderedInsertPos le1 r r0, orderedInsertPos_lt_length le1 r r0⟩
exact e3.trans (e4.symm.trans e2.symm)
@[simp]
@ -344,35 +353,44 @@ lemma orderedInsertEquiv_zero {I : Type} (le1 : I → I → Prop) [DecidableRel
@[simp]
lemma orderedInsertEquiv_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
(r0 : I) (n : ℕ) (hn : Nat.succ n < (r0 :: r).length) :
orderedInsertEquiv le1 r r0 ⟨Nat.succ n, hn⟩ = Fin.cast (List.orderedInsert_length le1 r r0).symm
((Fin.succAbove ⟨(orderedInsertPos le1 r r0), orderedInsertPos_lt_length le1 r r0⟩) ⟨n, Nat.succ_lt_succ_iff.mp hn⟩) := by
simp [orderedInsertEquiv]
orderedInsertEquiv le1 r r0 ⟨Nat.succ n, hn⟩ =
Fin.cast (List.orderedInsert_length le1 r r0).symm
((Fin.succAbove ⟨(orderedInsertPos le1 r r0), orderedInsertPos_lt_length le1 r r0⟩)
⟨n, Nat.succ_lt_succ_iff.mp hn⟩) := by
simp only [List.length_cons, orderedInsertEquiv, Nat.succ_eq_add_one, OrderIso.toEquiv_symm,
Fin.symm_castOrderIso, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply]
match r with
| [] =>
simp
| r1 :: r =>
erw [finExtractOne_apply_neq]
simp [orderedInsertPos]
simp only [List.orderedInsert.eq_2, List.length_cons, orderedInsertPos, decide_not,
Nat.succ_eq_add_one, finExtractOne_symm_inr_apply]
rfl
exact ne_of_beq_false rfl
@[simp]
lemma orderedInsertEquiv_fin_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
(r0 : I) (n : Fin r.length) :
(r0 : I) (n : Fin r.length) :
orderedInsertEquiv le1 r r0 n.succ = Fin.cast (List.orderedInsert_length le1 r r0).symm
((Fin.succAbove ⟨(orderedInsertPos le1 r r0), orderedInsertPos_lt_length le1 r r0⟩) ⟨n, n.isLt⟩) := by
simp [orderedInsertEquiv]
((Fin.succAbove ⟨(orderedInsertPos le1 r r0), orderedInsertPos_lt_length le1 r r0⟩)
⟨n, n.isLt⟩) := by
simp only [List.length_cons, orderedInsertEquiv, Nat.succ_eq_add_one, OrderIso.toEquiv_symm,
Fin.symm_castOrderIso, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Fin.eta]
match r with
| [] =>
simp
| r1 :: r =>
erw [finExtractOne_apply_neq]
simp [orderedInsertPos]
simp only [List.orderedInsert.eq_2, List.length_cons, orderedInsertPos, decide_not,
Nat.succ_eq_add_one, finExtractOne_symm_inr_apply]
rfl
exact ne_of_beq_false rfl
lemma orderedInsertEquiv_congr {α : Type} {r : α → α → Prop} [DecidableRel r] (a : α) (l l' : List α)
(h : l = l') : orderedInsertEquiv r l a = (Fin.castOrderIso (by simp [h])).toEquiv.trans
lemma orderedInsertEquiv_congr {α : Type} {r : α → α → Prop} [DecidableRel r] (a : α)
(l l' : List α) (h : l = l') :
orderedInsertEquiv r l a = (Fin.castOrderIso (by simp [h])).toEquiv.trans
((orderedInsertEquiv r l' a).trans (Fin.castOrderIso (by simp [h])).toEquiv) := by
subst h
rfl
@ -383,35 +401,38 @@ lemma get_eq_orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRe
funext x
match x with
| ⟨0, h⟩ =>
simp
simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
List.getElem_cons_zero, Function.comp_apply]
erw [orderedInsertEquiv_zero]
simp
| ⟨Nat.succ n, h⟩ =>
simp
simp only [List.length_cons, Nat.succ_eq_add_one, List.get_eq_getElem, List.getElem_cons_succ,
Function.comp_apply]
erw [orderedInsertEquiv_succ]
simp [Fin.succAbove]
simp only [Fin.succAbove, Fin.castSucc_mk, Fin.mk_lt_mk, Fin.succ_mk, Fin.coe_cast]
by_cases hn : n < ↑(orderedInsertPos le1 r r0)
· simp [hn]
· simp [hn]
simp [List.orderedInsert_eq_take_drop]
· simp only [hn, ↓reduceIte]
simp only [List.orderedInsert_eq_take_drop, decide_not]
rw [List.getElem_append]
have hn' : ¬ n + 1 < (List.takeWhile (fun b => !decide (le1 r0 b)) r).length := by
simp [orderedInsertPos] at hn
simp only [orderedInsertPos, decide_not, not_lt] at hn
omega
simp [hn']
simp only [hn', ↓reduceDIte]
have hnn : n + 1 - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length =
(n - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length) + 1 := by
simp [orderedInsertPos] at hn
simp only [orderedInsertPos, decide_not, not_lt] at hn
omega
simp [hnn]
simp only [hnn, List.getElem_cons_succ]
conv_rhs =>
rw [List.IsSuffix.getElem (List.dropWhile_suffix fun b => !decide (le1 r0 b))]
congr
have hr : r.length = (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + (List.dropWhile (fun b => !decide (le1 r0 b)) r).length := by
have hr : r.length = (List.takeWhile (fun b => !decide (le1 r0 b)) r).length +
(List.dropWhile (fun b => !decide (le1 r0 b)) r).length := by
rw [← List.length_append]
congr
exact Eq.symm (List.takeWhile_append_dropWhile (fun b => !decide (le1 r0 b)) r)
simp [hr]
simp only [hr, add_tsub_cancel_right]
omega
lemma orderedInsertEquiv_get {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
@ -421,14 +442,14 @@ lemma orderedInsertEquiv_get {I : Type} (le1 : I → I → Prop) [DecidableRel l
funext x
simp
lemma orderedInsert_eraseIdx_orderedInsertEquiv_zero
{I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
(List.orderedInsert le1 r0 r).eraseIdx (orderedInsertEquiv le1 r r0 ⟨0, by simp⟩) = r := by
simp [orderedInsertEquiv]
lemma orderedInsert_eraseIdx_orderedInsertEquiv_succ
{I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (n : ℕ) (hn : Nat.succ n < (r0 :: r).length)
{I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (n : ℕ)
(hn : Nat.succ n < (r0 :: r).length)
(hr : ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)) :
(List.orderedInsert le1 r0 r).eraseIdx (orderedInsertEquiv le1 r r0 ⟨Nat.succ n, hn⟩) =
(List.orderedInsert le1 r0 (r.eraseIdx n)) := by
@ -453,33 +474,34 @@ lemma orderedInsert_eraseIdx_orderedInsertEquiv_fin_succ
(List.orderedInsert le1 r0 (r.eraseIdx n)) := by
have hn : n.succ = ⟨n.val + 1, by omega⟩ := by
rw [Fin.ext_iff]
simp
rfl
rw [hn]
exact orderedInsert_eraseIdx_orderedInsertEquiv_succ le1 r r0 n.val _ hr
lemma orderedInsertEquiv_sigma {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(le1 : I → I → Prop) [DecidableRel le1] (l : List (Σ i, f i))
(i : I) (a : f i) :
(orderedInsertEquiv (fun i j => le1 i.fst j.fst) l ⟨i, a⟩) =
(i : I) (a : f i) :
(orderedInsertEquiv (fun i j => le1 i.fst j.fst) l ⟨i, a⟩) =
(Fin.castOrderIso (by simp)).toEquiv.trans
((orderedInsertEquiv le1 (List.map (fun i => i.1) l) i).trans
(Fin.castOrderIso (by simp [List.orderedInsert_length])).toEquiv) := by
ext x
match x with
| ⟨0, h0⟩ =>
simp
simp only [List.length_cons, Fin.zero_eta, Equiv.trans_apply, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, Fin.cast_zero, Fin.coe_cast]
erw [orderedInsertEquiv_zero, orderedInsertEquiv_zero]
simp [orderedInsertPos_sigma]
| ⟨Nat.succ n, h0⟩ =>
simp
simp only [List.length_cons, Nat.succ_eq_add_one, Equiv.trans_apply, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, Fin.cast_mk, Fin.coe_cast]
erw [orderedInsertEquiv_succ, orderedInsertEquiv_succ]
simp [orderedInsertPos_sigma]
simp only [orderedInsertPos_sigma, Fin.coe_cast]
rw [Fin.succAbove, Fin.succAbove]
simp
simp only [Fin.castSucc_mk, Fin.mk_lt_mk, Fin.succ_mk]
split
next h => simp_all only
next h => simp_all only [not_lt]
· rfl
· rfl
/-- This result is taken from:
https://github.com/leanprover/lean4/blob/master/src/Init/Data/List/Nat/InsertIdx.lean
@ -489,12 +511,14 @@ lemma orderedInsertEquiv_sigma {I : Type} {f : I → Type} [∀ i, Fintype (f i)
Floris van Doorn, Mario Carneiro.
Once HepLean is updated to a more recent version of Lean this result will be removed.
-/
theorem length_insertIdx' : ∀ n as, (List.insertIdx n a as).length = if n ≤ as.length then as.length + 1 else as.length
-/
theorem length_insertIdx' : ∀ n as, (List.insertIdx n a as).length =
if n ≤ as.length then as.length + 1 else as.length
| 0, _ => by simp
| n + 1, [] => by simp
| n + 1, [] => by rfl
| n + 1, a :: as => by
simp only [List.insertIdx_succ_cons, List.length_cons, length_insertIdx', Nat.add_le_add_iff_right]
simp only [List.insertIdx_succ_cons, List.length_cons, length_insertIdx',
Nat.add_le_add_iff_right]
split <;> rfl
/-- This result is taken from:
@ -505,15 +529,17 @@ theorem length_insertIdx' : ∀ n as, (List.insertIdx n a as).length = if n ≤
Floris van Doorn, Mario Carneiro.
Once HepLean is updated to that version of Lean this result will be removed.
-/
-/
theorem _root_.List.getElem_insertIdx_of_ge {l : List α} {x : α} {n k : Nat} (hn : n + 1 ≤ k)
(hk : k < (List.insertIdx n x l).length) :
(List.insertIdx n x l)[k] = l[k - 1]'(by simp [length_insertIdx'] at hk; split at hk <;> omega) := by
(List.insertIdx n x l)[k] =
l[k - 1]'(by simp only [length_insertIdx'] at hk; split at hk <;> omega) := by
induction l generalizing n k with
| nil =>
cases n with
| zero =>
simp [List.insertIdx_zero, List.length_singleton] at hk
simp only [List.insertIdx_zero, List.length_cons, List.length_nil, zero_add,
Nat.lt_one_iff] at hk
omega
| succ n => simp at hk
| cons _ _ ih =>
@ -533,15 +559,14 @@ theorem _root_.List.getElem_insertIdx_of_ge {l : List α} {x : α} {n k : Nat} (
| zero => omega
| succ k => simp
lemma orderedInsert_eq_insertIdx_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
List.orderedInsert le1 r0 r = List.insertIdx (orderedInsertPos le1 r r0).1 r0 r := by
List.orderedInsert le1 r0 r = List.insertIdx (orderedInsertPos le1 r r0).1 r0 r := by
apply List.ext_get
· simp [List.orderedInsert_length]
· simp only [List.orderedInsert_length]
rw [List.length_insertIdx]
have h1 := orderedInsertPos_lt_length le1 r r0
simp at h1
simp only [List.length_cons] at h1
omega
intro n h1 h2
obtain ⟨n', hn'⟩ := (orderedInsertEquiv le1 r r0).surjective ⟨n, h1⟩
@ -549,39 +574,43 @@ lemma orderedInsert_eq_insertIdx_orderedInsertPos {I : Type} (le1 : I → I →
have hn'' : n = ((orderedInsertEquiv le1 r r0) n').val := by rw [hn']
subst hn''
rw [← orderedInsertEquiv_get]
simp
simp only [List.length_cons, Function.comp_apply, Equiv.symm_apply_apply, List.get_eq_getElem]
match n' with
| ⟨0, h0⟩ =>
simp
simp [orderedInsertEquiv]
simp only [List.getElem_cons_zero, orderedInsertEquiv, List.length_cons, Nat.succ_eq_add_one,
OrderIso.toEquiv_symm, Fin.symm_castOrderIso, Fin.zero_eta, Equiv.trans_apply,
finExtractOne_apply_eq, Fin.isValue, finExtractOne_symm_inl_apply, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, Fin.cast_mk, Fin.eta]
rw [List.getElem_insertIdx_self]
exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le1 r r0)
| ⟨Nat.succ n', h0⟩ =>
simp
simp only [Nat.succ_eq_add_one, List.getElem_cons_succ, List.length_cons]
have hr := orderedInsertEquiv_succ le1 r r0 n' h0
trans (List.insertIdx (↑(orderedInsertPos le1 r r0)) r0 r).get ⟨↑((orderedInsertEquiv le1 r r0) ⟨n' +1, h0⟩), h2⟩
trans (List.insertIdx (↑(orderedInsertPos le1 r r0)) r0 r).get
⟨↑((orderedInsertEquiv le1 r r0) ⟨n' +1, h0⟩), h2⟩
swap
rfl
· rfl
rw [Fin.ext_iff] at hr
have hx : (⟨↑((orderedInsertEquiv le1 r r0) ⟨n' +1, h0⟩), h2⟩ :Fin (List.insertIdx (↑(orderedInsertPos le1 r r0)) r0 r).length) =
⟨(
(⟨↑(orderedInsertPos le1 r r0), orderedInsertPos_lt_length le1 r r0⟩ : Fin ((r).length + 1))).succAbove ⟨n', Nat.succ_lt_succ_iff.mp h0⟩, by
have hx : (⟨↑((orderedInsertEquiv le1 r r0) ⟨n' +1, h0⟩), h2⟩ :
Fin (List.insertIdx (↑(orderedInsertPos le1 r r0)) r0 r).length) =
⟨((⟨↑(orderedInsertPos le1 r r0),
orderedInsertPos_lt_length le1 r r0⟩ : Fin ((r).length + 1))).succAbove
⟨n', Nat.succ_lt_succ_iff.mp h0⟩, by
erw [← hr]
exact h2
⟩ := by
exact h2⟩ := by
rw [Fin.ext_iff]
simp
simp only [List.length_cons]
simpa using hr
rw [hx]
simp [Fin.succAbove]
simp only [Fin.succAbove, Fin.castSucc_mk, Fin.mk_lt_mk, Fin.succ_mk, List.get_eq_getElem]
by_cases hn' : n' < ↑(orderedInsertPos le1 r r0)
· simp [hn']
· simp only [hn', ↓reduceIte]
erw [List.getElem_insertIdx_of_lt]
exact hn'
· simp [hn']
· simp only [hn', ↓reduceIte]
rw [List.getElem_insertIdx_of_ge]
simp
omega
· rfl
· omega
/-- The equivalence between `Fin l.length ≃ Fin (List.insertionSort r l).length` induced by the
sorting algorithm. -/
@ -593,8 +622,7 @@ def insertionSortEquiv {α : Type} (r : α → α → Prop) [DecidableRel r] : (
lemma insertionSortEquiv_get {α : Type} {r : α → α → Prop} [DecidableRel r] : (l : List α) →
l.get ∘ (insertionSortEquiv r l).symm = (List.insertionSort r l).get
| [] => by
simp [insertionSortEquiv]
| [] => by rfl
| a :: l => by
rw [insertionSortEquiv]
change ((a :: l).get ∘ ((Fin.equivCons (insertionSortEquiv r l))).symm) ∘
@ -617,8 +645,8 @@ lemma insertionSortEquiv_congr {α : Type} {r : α → α → Prop} [DecidableRe
((insertionSortEquiv r l').trans (Fin.castOrderIso (by simp [h])).toEquiv) := by
subst h
rfl
lemma insertionSort_get_comp_insertionSortEquiv {α : Type} {r : α → α → Prop} [DecidableRel r] (l : List α) :
(List.insertionSort r l).get ∘ (insertionSortEquiv r l) = l.get := by
lemma insertionSort_get_comp_insertionSortEquiv {α : Type} {r : α → α → Prop} [DecidableRel r]
(l : List α) : (List.insertionSort r l).get ∘ (insertionSortEquiv r l) = l.get := by
rw [← insertionSortEquiv_get]
funext x
simp
@ -628,8 +656,6 @@ lemma insertionSort_eq_ofFn {α : Type} {r : α → α → Prop} [DecidableRel r
rw [insertionSortEquiv_get (r := r)]
exact Eq.symm (List.ofFn_get (List.insertionSort r l))
def optionErase {I : Type} (l : List I) (i : Option (Fin l.length)) : List I :=
match i with
| none => l
@ -642,7 +668,7 @@ def optionEraseZ {I : Type} (l : List I) (a : I) (i : Option (Fin l.length)) : L
lemma eraseIdx_length {I : Type} (l : List I) (i : Fin l.length) :
(List.eraseIdx l i).length + 1 = l.length := by
simp [List.length_eraseIdx]
simp only [List.length_eraseIdx, Fin.is_lt, ↓reduceIte]
have hi := i.prop
omega
@ -650,21 +676,21 @@ lemma eraseIdx_cons_length {I : Type} (a : I) (l : List I) (i : Fin (a :: l).len
(List.eraseIdx (a :: l) i).length= l.length := by
simp [List.length_eraseIdx]
lemma eraseIdx_get {I : Type} (l : List I) (i : Fin l.length) :
(List.eraseIdx l i).get = l.get ∘ (Fin.cast (eraseIdx_length l i)) ∘ (Fin.cast (eraseIdx_length l i).symm i).succAbove := by
(List.eraseIdx l i).get = l.get ∘ (Fin.cast (eraseIdx_length l i)) ∘
(Fin.cast (eraseIdx_length l i).symm i).succAbove := by
ext x
simp only [Function.comp_apply, List.get_eq_getElem, List.eraseIdx, List.getElem_eraseIdx]
simp [Fin.succAbove]
simp only [Fin.succAbove, Fin.coe_cast]
by_cases hi: x.castSucc < Fin.cast (by exact Eq.symm (eraseIdx_length l i)) i
· simp [ hi]
· simp only [hi, ↓reduceIte, Fin.coe_castSucc, dite_eq_left_iff, not_lt]
intro h
rw [Fin.lt_def] at hi
simp_all
simp_all only [Fin.coe_castSucc, Fin.coe_cast]
omega
· simp [ hi]
· simp only [hi, ↓reduceIte, Fin.val_succ]
rw [Fin.lt_def] at hi
simp at hi
simp only [Fin.coe_castSucc, Fin.coe_cast, not_lt] at hi
have hn : ¬ x.val < i.val := by omega
simp [hn]
@ -673,18 +699,17 @@ lemma eraseIdx_insertionSort {I : Type} (le1 : I → I → Prop) [DecidableRel l
(n : ℕ) → (r : List I) → (hn : n < r.length) →
(List.insertionSort le1 r).eraseIdx ↑((HepLean.List.insertionSortEquiv le1 r) ⟨n, hn⟩)
= List.insertionSort le1 (r.eraseIdx n)
| 0, [], _ => by
simp
| 0, [], _ => by rfl
| 0, (r0 :: r), hn => by
simp only [List.insertionSort, List.insertionSort.eq_2, List.length_cons, insertionSortEquiv,
Nat.succ_eq_add_one, Fin.zero_eta, Equiv.trans_apply, equivCons_zero, List.eraseIdx_zero,
List.tail_cons]
erw [orderedInsertEquiv_zero]
simp
| Nat.succ n, [], hn => by
simp [insertionSortEquiv]
| Nat.succ n, [], hn => by rfl
| Nat.succ n, (r0 :: r), hn => by
simp [insertionSortEquiv]
simp only [List.insertionSort, List.length_cons, insertionSortEquiv, Nat.succ_eq_add_one,
Equiv.trans_apply, equivCons_succ]
have hOr := orderedInsert_eraseIdx_orderedInsertEquiv_fin_succ le1
(List.insertionSort le1 r) r0 ((insertionSortEquiv le1 r) ⟨n, by simpa using hn⟩)
erw [hOr]
@ -703,12 +728,9 @@ lemma eraseIdx_insertionSort {I : Type} (le1 : I → I → Prop) [DecidableRel l
exact ht ((List.insertionSort le1 r).get i) ((List.insertionSort le1 r).get j) r0 hx hn
lemma eraseIdx_insertionSort_fin {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
[IsTotal I le1] [IsTrans I le1] (r : List I) (n : Fin r.length) :
[IsTotal I le1] [IsTrans I le1] (r : List I) (n : Fin r.length) :
(List.insertionSort le1 r).eraseIdx ↑((HepLean.List.insertionSortEquiv le1 r) n)
= List.insertionSort le1 (r.eraseIdx n) :=
eraseIdx_insertionSort le1 n.val r (Fin.prop n)
end HepLean.List

74
HepLean/PerturbationTheory/Wick/Koszul/Contraction.lean
View file

@ -29,7 +29,6 @@ variable {I : Type} {l : List I} (c : Contractions l)
def normalize : List I := c.1
lemma contractions_nil (a : Contractions ([] : List I)) : a = ⟨[], ContractionsAux.nil⟩ := by
cases a
rename_i aux c
@ -37,24 +36,22 @@ lemma contractions_nil (a : Contractions ([] : List I)) : a = ⟨[], Contraction
rfl
lemma contractions_single {i : I} (a : Contractions [i]) : a =
⟨[i], ContractionsAux.cons none ContractionsAux.nil⟩ := by
⟨[i], ContractionsAux.cons none ContractionsAux.nil⟩ := by
cases a
rename_i aux c
cases c
rename_i aux' c'
cases c'
cases aux'
simp [optionEraseZ]
simp only [List.length_nil, optionEraseZ]
rename_i x
exact Fin.elim0 x
def nilEquiv : Contractions ([] : List I) ≃ Unit where
toFun _ := ()
invFun _ := ⟨[], ContractionsAux.nil⟩
left_inv a := by
exact Eq.symm (contractions_nil a)
right_inv _ := by
rfl
left_inv a := Eq.symm (contractions_nil a)
right_inv _ := rfl
def consEquiv {a : I} {l : List I} :
Contractions (a :: l) ≃ (c : Contractions l) × Option (Fin (c.normalize).length) where
@ -77,33 +74,32 @@ instance decidable : (l : List I) → DecidableEq (Contractions l)
match a, b with
| ⟨_, a⟩, ⟨_, b⟩ =>
match a, b with
| ContractionsAux.nil , ContractionsAux.nil => isTrue rfl
| _ :: l =>
| ContractionsAux.nil, ContractionsAux.nil => isTrue rfl
| _ :: l =>
haveI : DecidableEq (Contractions l) := decidable l
haveI : DecidableEq ((c : Contractions l) × Option (Fin (c.normalize).length)) :=
Sigma.instDecidableEqSigma
Equiv.decidableEq consEquiv
instance fintype : (l : List I) → Fintype (Contractions l)
instance fintype : (l : List I) → Fintype (Contractions l)
| [] => {
elems := {⟨[], ContractionsAux.nil⟩}
complete := by
intro a
rw [Finset.mem_singleton]
exact contractions_nil a}
| a :: l =>
| a :: l =>
haveI : Fintype (Contractions l) := fintype l
haveI : Fintype ((c : Contractions l) × Option (Fin (c.normalize).length)) :=
Sigma.instFintype
Fintype.ofEquiv _ consEquiv.symm
structure Splitting {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1] where
𝓑n : I → (Σ i, f i)
𝓑p : I → (Σ i, f i)
𝓧n : I → ℂ
𝓧p : I → ℂ
𝓑n : I → (Σ i, f i)
𝓑p : I → (Σ i, f i)
𝓧n : I → ℂ
𝓧p : I → ℂ
h𝓑 : ∀ i, ofListM f [i] 1 = ofList [𝓑n i] (𝓧n i) + ofList [𝓑p i] (𝓧p i)
h𝓑n : ∀ i j, le1 (𝓑n i) j
h𝓑p : ∀ i j, le1 j (𝓑p i)
@ -112,11 +108,11 @@ def toCenterTerm {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
(q : I → Fin 2)
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
{A : Type} [Semiring A] [Algebra ℂ A]
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
: {r : List I} → (c : Contractions r) → (S : Splitting f le1) → A
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F] :
{r : List I} → (c : Contractions r) → (S : Splitting f le1) → A
| [], ⟨[], .nil⟩, _ => 1
| _ :: _, ⟨_, .cons (aux := aux') none c⟩, S => toCenterTerm f q le1 F ⟨aux', c⟩ S
| a :: _, ⟨_, .cons (aux := aux') (some n) c⟩, S => toCenterTerm f q le1 F ⟨aux', c⟩ S *
| a :: _, ⟨_, .cons (aux := aux') (some n) c⟩, S => toCenterTerm f q le1 F ⟨aux', c⟩ S *
superCommuteCoef q [aux'.get n] (List.take (↑n) aux') •
F (((superCommute fun i => q i.fst) (ofList [S.𝓑p a] (S.𝓧p a))) (ofListM f [aux'.get n] 1))
@ -124,11 +120,12 @@ lemma toCenterTerm_none {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
(q : I → Fin 2) {r : List I}
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
{A : Type} [Semiring A] [Algebra ℂ A]
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
(S : Splitting f le1) (a : I) (c : Contractions r) :
toCenterTerm (r := a :: r) f q le1 F (Contractions.consEquiv.symm ⟨c, none⟩) S = toCenterTerm f q le1 F c S := by
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
(S : Splitting f le1) (a : I) (c : Contractions r) :
toCenterTerm (r := a :: r) f q le1 F (Contractions.consEquiv.symm ⟨c, none⟩) S =
toCenterTerm f q le1 F c S := by
rw [consEquiv]
simp [optionErase]
simp only [Equiv.coe_fn_symm_mk]
dsimp [toCenterTerm]
rfl
@ -136,8 +133,8 @@ lemma toCenterTerm_center {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
(q : I → Fin 2)
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
{A : Type} [Semiring A] [Algebra ℂ A]
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
: {r : List I} → (c : Contractions r) → (S : Splitting f le1) →
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F] :
{r : List I} → (c : Contractions r) → (S : Splitting f le1) →
(c.toCenterTerm f q le1 F S) ∈ Subalgebra.center ℂ A
| [], ⟨[], .nil⟩, _ => by
dsimp [toCenterTerm]
@ -145,7 +142,7 @@ lemma toCenterTerm_center {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
| _ :: _, ⟨_, .cons (aux := aux') none c⟩, S => by
dsimp [toCenterTerm]
exact toCenterTerm_center f q le1 F ⟨aux', c⟩ S
| a :: _, ⟨_, .cons (aux := aux') (some n) c⟩, S => by
| a :: _, ⟨_, .cons (aux := aux') (some n) c⟩, S => by
dsimp [toCenterTerm]
refine Subalgebra.mul_mem (Subalgebra.center ℂ A) ?hx ?hy
exact toCenterTerm_center f q le1 F ⟨aux', c⟩ S
@ -154,9 +151,10 @@ lemma toCenterTerm_center {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
rw [map_sum, map_sum]
refine Subalgebra.sum_mem (Subalgebra.center ℂ A) ?hy.hx.h
intro x _
simp [CreatAnnilateSect.toList]
simp only [CreatAnnilateSect.toList]
rw [ofList_singleton]
exact OperatorMap.superCommute_ofList_singleton_ι_center (q := fun i => q i.1) (le1 := le1) F (S.𝓑p a) ⟨aux'[↑n], x.head⟩
exact OperatorMap.superCommute_ofList_singleton_ι_center (q := fun i => q i.1)
(le1 := le1) F (S.𝓑p a) ⟨aux'[↑n], x.head⟩
end Contractions
@ -167,9 +165,11 @@ lemma static_wick_nil {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
(S : Contractions.Splitting f le1) :
F (ofListM f [] 1) = ∑ c : Contractions [],
c.toCenterTerm f q le1 F S * F (koszulOrder le1 (fun i => q i.fst) (ofListM f c.normalize 1)) := by
c.toCenterTerm f q le1 F S *
F (koszulOrder le1 (fun i => q i.fst) (ofListM f c.normalize 1)) := by
rw [← Contractions.nilEquiv.symm.sum_comp]
simp [Contractions.nilEquiv]
simp only [Finset.univ_unique, PUnit.default_eq_unit, Contractions.nilEquiv, Equiv.coe_fn_symm_mk,
Finset.sum_const, Finset.card_singleton, one_smul]
dsimp [Contractions.normalize, Contractions.toCenterTerm]
simp [ofListM_empty]
@ -181,9 +181,11 @@ lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
(S : Contractions.Splitting f le1)
(ih : F (ofListM f r 1) =
∑ c : Contractions r, c.toCenterTerm f q le1 F S * F (koszulOrder le1 (fun i => q i.fst) (ofListM f c.normalize 1))) :
F (ofListM f (a :: r) 1) = ∑ c : Contractions ( a :: r),
c.toCenterTerm f q le1 F S * F (koszulOrder le1 (fun i => q i.fst) (ofListM f c.normalize 1)) := by
∑ c : Contractions r, c.toCenterTerm f q le1 F S * F (koszulOrder le1 (fun i => q i.fst)
(ofListM f c.normalize 1))) :
F (ofListM f (a :: r) 1) = ∑ c : Contractions (a :: r),
c.toCenterTerm f q le1 F S *
F (koszulOrder le1 (fun i => q i.fst) (ofListM f c.normalize 1)) := by
rw [ofListM_cons_eq_ofListM, map_mul, ih, Finset.mul_sum,
← Contractions.consEquiv.symm.sum_comp]
erw [Finset.sum_sigma]
@ -219,7 +221,8 @@ lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
rhs
rhs
intro n
rw [← Algebra.smul_mul_assoc, smul_comm, ← map_smul, ← LinearMap.map_smul₂, ← ofList_eq_smul_one]
rw [← Algebra.smul_mul_assoc, smul_comm, ← map_smul, ← LinearMap.map_smul₂,
← ofList_eq_smul_one]
rw [← add_assoc, ← map_add, ← map_add, ← add_mul, ← hb, ← ofListM_cons_eq_ofListM, mul_add]
rw [Fintype.sum_option]
congr 1
@ -233,7 +236,8 @@ lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
theorem static_wick_theorem {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2)
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1] [IsTrans ((i : I) × f i) le1] [IsTotal ((i : I) × f i) le1]
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1] [IsTrans ((i : I) × f i) le1]
[IsTotal ((i : I) × f i) le1]
{A : Type} [Semiring A] [Algebra ℂ A] (r : List I)
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
(S : Contractions.Splitting f le1) :

164
HepLean/PerturbationTheory/Wick/Koszul/Grade.lean
View file

@ -19,7 +19,7 @@ def grade {I : Type} (q : I → Fin 2) : (l : List I) → Fin 2
| a :: l => if q a = grade q l then 0 else 1
@[simp]
lemma grade_freeMonoid {I : Type} (q : I → Fin 2) (i : I) : grade q (FreeMonoid.of i) = q i := by
lemma grade_freeMonoid {I : Type} (q : I → Fin 2) (i : I) : grade q (FreeMonoid.of i) = q i := by
simp only [grade, Fin.isValue]
have ha (a : Fin 2) : (if a = 0 then 0 else 1) = a := by
fin_cases a <;> rfl
@ -42,12 +42,12 @@ lemma grade_append {I : Type} (q : I → Fin 2) (l r : List I) :
simp only [grade, List.append_eq, Fin.isValue]
erw [ih]
have hab (a b c : Fin 2) : (if a = if b = c then 0 else 1 then (0 : Fin 2) else 1) =
if (if a = b then 0 else 1) = c then 0 else 1 := by
if (if a = b then 0 else 1) = c then 0 else 1 := by
fin_cases a <;> fin_cases b <;> fin_cases c <;> rfl
exact hab (q a) (grade q l) (grade q r)
lemma grade_orderedInsert {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (l : List I) ( i : I ) :
grade q (List.orderedInsert le1 i l) = grade q (i :: l) := by
lemma grade_orderedInsert {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(l : List I) (i : I) : grade q (List.orderedInsert le1 i l) = grade q (i :: l) := by
induction l with
| nil => simp
| cons j l ih =>
@ -58,13 +58,14 @@ lemma grade_orderedInsert {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
rw [grade]
rw [ih]
simp only [grade, Fin.isValue]
have h1 (a b c : Fin 2) : (if a = if b = c then 0 else 1 then (0 : Fin 2) else 1) = if b = if a = c then 0 else 1 then 0 else 1 := by
have h1 (a b c : Fin 2) : (if a = if b = c then 0 else 1 then (0 : Fin 2) else 1) =
if b = if a = c then 0 else 1 then 0 else 1 := by
fin_cases a <;> fin_cases b <;> fin_cases c <;> rfl
exact h1 _ _ _
@[simp]
lemma grade_insertionSort {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (l : List I) :
grade q (List.insertionSort le1 l) = grade q l := by
lemma grade_insertionSort {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(l : List I) : grade q (List.insertionSort le1 l) = grade q l := by
induction l with
| nil => simp
| cons j l ih =>
@ -74,7 +75,7 @@ lemma grade_insertionSort {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
rw [ih]
lemma grade_count {I : Type} (q : I → Fin 2) (l : List I) :
grade q l = if Nat.mod (List.countP (fun i => decide (q i = 1)) l) 2 = 0 then 0 else 1 := by
grade q l = if Nat.mod (List.countP (fun i => decide (q i = 1)) l) 2 = 0 then 0 else 1 := by
induction l with
| nil => simp
| cons r0 r ih =>
@ -100,7 +101,7 @@ lemma grade_count {I : Type} (q : I → Fin 2) (l : List I) :
next h2 => simp_all only [Fin.isValue]
next h2 =>
simp_all only [Fin.isValue, zero_ne_one]
have ha (a : ℕ) (ha : ¬ a % 2 = 0) : (a + 1) % 2 = 0 := by
have ha (a : ℕ) (ha : ¬ a % 2 = 0) : (a + 1) % 2 = 0 := by
omega
exact h2 (ha (List.countP (fun i => decide (q i = 1)) r) h1)
· have h0 : q r0 = 0 := by omega
@ -114,9 +115,9 @@ lemma grade_perm {I : Type} (q : I → Fin 2) {l l' : List I} (h : l.Perm l') :
rw [grade_count, grade_count, h.countP_eq]
def superCommuteCoef {I : Type} (q : I → Fin 2) (la lb : List I) : ℂ :=
if grade q la = 1 ∧ grade q lb = 1 then - 1 else 1
if grade q la = 1 ∧ grade q lb = 1 then - 1 else 1
lemma superCommuteCoef_comm {I : Type} (q : I → Fin 2) (la lb : List I) :
lemma superCommuteCoef_comm {I : Type} (q : I → Fin 2) (la lb : List I) :
superCommuteCoef q la lb = superCommuteCoef q lb la := by
simp only [superCommuteCoef, Fin.isValue]
congr 1
@ -125,13 +126,13 @@ lemma superCommuteCoef_comm {I : Type} (q : I → Fin 2) (la lb : List I) :
lemma superCommuteCoef_perm_snd {I : Type} (q : I → Fin 2) (la lb lb' : List I)
(h : lb.Perm lb') :
superCommuteCoef q la lb = superCommuteCoef q la lb' := by
rw [superCommuteCoef, superCommuteCoef, grade_perm q h ]
rw [superCommuteCoef, superCommuteCoef, grade_perm q h]
lemma superCommuteCoef_mul_self {I : Type} (q : I → Fin 2) (l lb : List I) :
superCommuteCoef q l lb * superCommuteCoef q l lb = 1 := by
superCommuteCoef q l lb * superCommuteCoef q l lb = 1 := by
simp only [superCommuteCoef, Fin.isValue, mul_ite, mul_neg, mul_one]
have ha (a b : Fin 2) : (if a = 1 ∧ b = 1 then -if a = 1 ∧ b = 1 then -1 else 1
else if a = 1 ∧ b = 1 then -1 else 1) = (1 : ℂ) := by
have ha (a b : Fin 2) : (if a = 1 ∧ b = 1 then -if a = 1 ∧ b = 1 then -1 else 1
else if a = 1 ∧ b = 1 then -1 else 1) = (1 : ℂ) := by
fin_cases a <;> fin_cases b
any_goals rfl
simp
@ -141,7 +142,7 @@ lemma superCommuteCoef_empty {I : Type} (q : I → Fin 2) (la : List I) :
superCommuteCoef q la [] = 1 := by
simp only [superCommuteCoef, Fin.isValue, grade_empty, zero_ne_one, and_false, ↓reduceIte]
lemma superCommuteCoef_append {I : Type} (q : I → Fin 2) (la lb lc : List I) :
lemma superCommuteCoef_append {I : Type} (q : I → Fin 2) (la lb lc : List I) :
superCommuteCoef q la (lb ++ lc) = superCommuteCoef q la lb * superCommuteCoef q la lc := by
simp only [superCommuteCoef, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one, imp_false,
mul_ite, mul_neg, mul_one]
@ -163,7 +164,7 @@ lemma superCommuteCoef_append {I : Type} (q : I → Fin 2) (la lb lc : List I)
omega
simp [ha]
lemma superCommuteCoef_cons {I : Type} (q : I → Fin 2) (i : I) (la lb : List I) :
lemma superCommuteCoef_cons {I : Type} (q : I → Fin 2) (i : I) (la lb : List I) :
superCommuteCoef q la (i :: lb) = superCommuteCoef q la [i] * superCommuteCoef q la lb := by
trans superCommuteCoef q la ([i] ++ lb)
simp only [List.singleton_append]
@ -173,13 +174,13 @@ def superCommuteCoefM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) : ℂ :=
(if grade (fun i => q i.fst) l = 1 ∧ grade q r = 1 then -1 else 1)
lemma superCommuteCoefM_empty {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)):
lemma superCommuteCoefM_empty {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) :
superCommuteCoefM q l [] = 1 := by
simp [superCommuteCoefM]
def superCommuteCoefLE {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
[DecidableRel le1] (i : I) (n : Fin r.length) : ℂ :=
def superCommuteCoefLE {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
[DecidableRel le1] (i : I) (n : Fin r.length) : ℂ :=
koszulSign le1 q r *
superCommuteCoef q [i] (List.take (↑((HepLean.List.insertionSortEquiv le1 r) n))
(List.insertionSort le1 r)) *
@ -195,10 +196,10 @@ lemma superCommuteCoefLE_eq_q {I : Type} (q : I → Fin 2) (le1 :I → I → Pro
koszulSign le1 q (r.eraseIdx ↑n) := by
simp [superCommuteCoefLE, superCommuteCoef, grade, hq]
lemma koszulSignInsert_eq_filter {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (r0 : I)
: (r : List I) →
koszulSignInsert le1 q r0 r = koszulSignInsert le1 q r0 (List.filter (fun i => decide (¬ le1 r0 i)) r)
lemma koszulSignInsert_eq_filter {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(r0 : I) : (r : List I) →
koszulSignInsert le1 q r0 r =
koszulSignInsert le1 q r0 (List.filter (fun i => decide (¬ le1 r0 i)) r)
| [] => by
simp [koszulSignInsert]
| r1 :: r => by
@ -217,10 +218,9 @@ lemma koszulSignInsert_eq_filter {I : Type} (q : I → Fin 2) (le1 : I → I →
simp only [decide_not]
simp
lemma koszulSignInsert_eq_grade {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (r0 : I)
(r : List I) :
koszulSignInsert le1 q r0 r = if grade q [r0] = 1 ∧
grade q (List.filter (fun i => decide (¬ le1 r0 i)) r) = 1 then -1 else 1 := by
lemma koszulSignInsert_eq_grade {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(r0 : I) (r : List I) : koszulSignInsert le1 q r0 r = if grade q [r0] = 1 ∧
grade q (List.filter (fun i => decide (¬ le1 r0 i)) r) = 1 then -1 else 1 := by
induction r with
| nil =>
simp [koszulSignInsert]
@ -235,11 +235,11 @@ lemma koszulSignInsert_eq_grade {I : Type} (q : I → Fin 2) (le1 : I → I →
have ha (a b c : Fin 2) : (if a = 1 ∧ b = 1 then -if ¬a = 0 ∧
c = 1 then -1 else (1 : ℂ)
else if ¬a = 0 ∧ c = 1 then -1 else 1) =
if ¬a = 0 ∧ ¬b = c then -1 else 1:= by
if ¬a = 0 ∧ ¬b = c then -1 else 1 := by
fin_cases a <;> fin_cases b <;> fin_cases c
any_goals rfl
simp
rw [← ha (q r0) (q r1) (grade q (List.filter (fun a => !decide (le1 r0 a)) r) )]
rw [← ha (q r0) (q r1) (grade q (List.filter (fun a => !decide (le1 r0 a)) r))]
congr
· rw [koszulSignInsert_eq_filter] at ih
simpa [grade] using ih
@ -252,7 +252,7 @@ lemma koszulSignInsert_eq_grade {I : Type} (q : I → Fin 2) (le1 : I → I →
simpa [grade] using ih
simpa using hr1
lemma koszulSignInsert_eq_perm {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) (r r' : List I)
lemma koszulSignInsert_eq_perm {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) (r r' : List I)
(a : I) [DecidableRel le1] (h : r.Perm r') :
koszulSignInsert le1 q a r = koszulSignInsert le1 q a r' := by
rw [koszulSignInsert_eq_grade]
@ -260,7 +260,7 @@ lemma koszulSignInsert_eq_perm {I : Type} (q : I → Fin 2) (le1 : I → I →
congr 1
simp only [Fin.isValue, decide_not, eq_iff_iff, and_congr_right_iff]
intro h'
have hg : grade q (List.filter (fun i => !decide (le1 a i)) r) =
have hg : grade q (List.filter (fun i => !decide (le1 a i)) r) =
grade q (List.filter (fun i => !decide (le1 a i)) r') := by
rw [grade_count, grade_count]
rw [List.countP_filter, List.countP_filter]
@ -273,25 +273,23 @@ lemma koszulSignInsert_eq_sort {I : Type} (q : I → Fin 2) (le1 : I → I → P
apply koszulSignInsert_eq_perm
exact List.Perm.symm (List.perm_insertionSort le1 r)
lemma koszulSignInsert_eq_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
[IsTotal I le1] [IsTrans I le1] (r0 : I)
(r : List I) :
koszulSignInsert le1 q r0 r = koszulSignInsert le1 q r0 (r0 :: r):= by
[IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) :
koszulSignInsert le1 q r0 r = koszulSignInsert le1 q r0 (r0 :: r) := by
simp only [koszulSignInsert, Fin.isValue, and_self]
have h1 : le1 r0 r0 := by
simpa using IsTotal.total (r := le1) r0 r0
simp [h1]
def insertSign {I : Type} (q : I → Fin 2) (n : ℕ)
(r0 : I) (r : List I) : ℂ :=
(r0 : I) (r : List I) : ℂ :=
superCommuteCoef q [r0] (List.take n r)
lemma take_insert_same {I : Type} (i : I) :
(n : ℕ) → (r : List I) →
(n : ℕ) → (r : List I) →
List.take n (List.insertIdx n i r) = List.take n r
| 0, _ => by simp
| _+1, [] => by simp
| 0, _ => by simp
| _+1, [] => by simp
| n+1, a::as => by
simp only [List.insertIdx_succ_cons, List.take_succ_cons, List.cons.injEq, true_and]
exact take_insert_same i n as
@ -303,10 +301,10 @@ lemma insertSign_insert {I : Type} (q : I → Fin 2) (n : ℕ)
rw [take_insert_same]
lemma take_eraseIdx_same {I : Type} :
(n : ℕ) → (r : List I) →
(n : ℕ) → (r : List I) →
List.take n (List.eraseIdx r n) = List.take n r
| 0, _ => by simp
| _+1, [] => by simp
| 0, _ => by simp
| _+1, [] => by simp
| n+1, a::as => by
simp only [List.eraseIdx_cons_succ, List.take_succ_cons, List.cons.injEq, true_and]
exact take_eraseIdx_same n as
@ -328,16 +326,15 @@ lemma insertSign_succ_cons {I : Type} (q : I → Fin 2) (n : ℕ)
rw [superCommuteCoef_cons]
lemma take_insert_gt {I : Type} (i : I) :
(n m : ℕ) → (h : n < m) → (r : List I) →
List.take n (List.insertIdx m i r) = List.take n r
| 0, 0, _, _ => by simp
| 0, m + 1, _, _ => by simp
| n+1, m + 1, _, [] => by simp
(n m : ℕ) → (h : n < m) → (r : List I) →
List.take n (List.insertIdx m i r) = List.take n r
| 0, 0, _, _ => by simp
| 0, m + 1, _, _ => by simp
| n+1, m + 1, _, [] => by simp
| n+1, m + 1, h, a::as => by
simp only [List.insertIdx_succ_cons, List.take_succ_cons, List.cons.injEq, true_and]
refine take_insert_gt i n m (Nat.succ_lt_succ_iff.mp h) as
lemma insertSign_insert_gt {I : Type} (q : I → Fin 2) (n m : ℕ)
(r0 r1 : I) (r : List I) (hn : n < m) :
insertSign q n r0 (List.insertIdx m r1 r) = insertSign q n r0 r := by
@ -346,13 +343,13 @@ lemma insertSign_insert_gt {I : Type} (q : I → Fin 2) (n m : ℕ)
exact take_insert_gt r1 n m hn r
lemma take_insert_let {I : Type} (i : I) :
(n m : ℕ) → (h : m ≤ n) → (r : List I) → (hm : m ≤ r.length) →
(n m : ℕ) → (h : m ≤ n) → (r : List I) → (hm : m ≤ r.length) →
(List.take (n + 1) (List.insertIdx m i r)).Perm (i :: List.take n r)
| 0, 0, h, _, _ => by simp
| m + 1, 0, h, r, _ => by simp
| n + 1, m + 1, h, [], hm => by
| 0, 0, h, _, _ => by simp
| m + 1, 0, h, r, _ => by simp
| n + 1, m + 1, h, [], hm => by
simp at hm
| n + 1, m + 1, h, a::as, hm => by
| n + 1, m + 1, h, a::as, hm => by
simp only [List.insertIdx_succ_cons, List.take_succ_cons]
have hp : (i :: a :: List.take n as).Perm (a :: i :: List.take n as) := by
exact List.Perm.swap a i (List.take n as)
@ -361,7 +358,7 @@ lemma take_insert_let {I : Type} (i : I) :
exact take_insert_let i n m (Nat.le_of_succ_le_succ h) as (Nat.le_of_succ_le_succ hm)
lemma insertSign_insert_lt_eq_insertSort {I : Type} (q : I → Fin 2) (n m : ℕ)
(r0 r1 : I) (r : List I) (hn : m ≤ n) (hm : m ≤ r.length):
(r0 r1 : I) (r : List I) (hn : m ≤ n) (hm : m ≤ r.length) :
insertSign q (n + 1) r0 (List.insertIdx m r1 r) = insertSign q (n + 1) r0 (r1 :: r) := by
rw [insertSign, insertSign]
apply superCommuteCoef_perm_snd
@ -369,23 +366,21 @@ lemma insertSign_insert_lt_eq_insertSort {I : Type} (q : I → Fin 2) (n m : ℕ
refine take_insert_let r1 n m hn r hm
lemma insertSign_insert_lt {I : Type} (q : I → Fin 2) (n m : ℕ)
(r0 r1 : I) (r : List I) (hn : m ≤ n) (hm : m ≤ r.length):
insertSign q (n + 1) r0 (List.insertIdx m r1 r) = superCommuteCoef q [r0] [r1] * insertSign q n r0 r := by
(r0 r1 : I) (r : List I) (hn : m ≤ n) (hm : m ≤ r.length) :
insertSign q (n + 1) r0 (List.insertIdx m r1 r) = superCommuteCoef q [r0] [r1] *
insertSign q n r0 r := by
rw [insertSign_insert_lt_eq_insertSort, insertSign_succ_cons]
exact hn
exact hm
def koszulSignCons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (r0 r1 : I) :
ℂ :=
if le1 r0 r1 then 1 else
if q r0 = 1 ∧ q r1 = 1 then -1 else 1
lemma koszulSignCons_eq_superComuteCoef {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(r0 r1 : I) : koszulSignCons q le1 r0 r1 =
if le1 r0 r1 then 1 else superCommuteCoef q [r0] [r1] := by
lemma koszulSignCons_eq_superComuteCoef {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
[DecidableRel le1] (r0 r1 : I) : koszulSignCons q le1 r0 r1 =
if le1 r0 r1 then 1 else superCommuteCoef q [r0] [r1] := by
simp only [koszulSignCons, Fin.isValue, superCommuteCoef, grade, ite_eq_right_iff, zero_ne_one,
imp_false]
congr 1
@ -402,11 +397,12 @@ lemma koszulSignCons_eq_superComuteCoef {I : Type} (q : I → Fin 2) (le1 : I
lemma koszulSignInsert_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
[IsTotal I le1] [IsTrans I le1] (r0 r1 : I) (r : List I) :
koszulSignInsert le1 q r0 (r1 :: r) = koszulSignCons q le1 r0 r1 * koszulSignInsert le1 q r0 r := by
koszulSignInsert le1 q r0 (r1 :: r) = koszulSignCons q le1 r0 r1 *
koszulSignInsert le1 q r0 r := by
simp [koszulSignInsert, koszulSignCons]
lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
[IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) :
lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
[DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) :
koszulSignInsert le1 q r0 r = insertSign q (orderedInsertPos le1 (List.insertionSort le1 r) r0)
r0 (List.insertionSort le1 r) := by
rw [koszulSignInsert_eq_cons, koszulSignInsert_eq_sort, koszulSignInsert_eq_filter,
@ -416,8 +412,9 @@ lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I
rw [List.insertionSort]
nth_rewrite 1 [List.orderedInsert_eq_take_drop]
rw [List.filter_append]
have h1 : List.filter (fun a => decide ¬le1 r0 a) (List.takeWhile (fun b => decide ¬le1 r0 b) (List.insertionSort le1 r))
= (List.takeWhile (fun b => decide ¬le1 r0 b) (List.insertionSort le1 r)) := by
have h1 : List.filter (fun a => decide ¬le1 r0 a)
(List.takeWhile (fun b => decide ¬le1 r0 b) (List.insertionSort le1 r))
= (List.takeWhile (fun b => decide ¬le1 r0 b) (List.insertionSort le1 r)) := by
induction r with
| nil => simp
| cons r1 r ih =>
@ -435,7 +432,7 @@ lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I
Bool.not_true, decide_eq_false_iff_not, Decidable.not_not]
intro a ha
refine List.Sorted.rel_of_mem_take_of_mem_drop
(k := (orderedInsertPos le1 (List.insertionSort le1 r) r0).1 + 1 )
(k := (orderedInsertPos le1 (List.insertionSort le1 r) r0).1 + 1)
(List.sorted_insertionSort le1 (r0 :: r)) ?_ ?_
· simp only [List.insertionSort, List.orderedInsert_eq_take_drop, decide_not]
rw [List.take_append_eq_append_take]
@ -449,12 +446,12 @@ lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I
· simp [orderedInsertPos]
lemma koszulSignInsert_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(i j : I) [IsTotal I le1] [IsTrans I le1] (r : List I) (n : ℕ) (hn : n ≤ r.length) :
koszulSignInsert le1 q j (List.insertIdx n i r) = koszulSignInsert le1 q j (i :: r) := by
(i j : I) [IsTotal I le1] [IsTrans I le1] (r : List I) (n : ℕ) (hn : n ≤ r.length) :
koszulSignInsert le1 q j (List.insertIdx n i r) = koszulSignInsert le1 q j (i :: r) := by
apply koszulSignInsert_eq_perm
exact List.perm_insertIdx i r hn
lemma take_insertIdx {I : Type} (i : I) : (r : List I) → (n : ℕ) → (hn : n ≤ r.length) →
lemma take_insertIdx {I : Type} (i : I) : (r : List I) → (n : ℕ) → (hn : n ≤ r.length) →
List.take n (List.insertIdx n i r) = List.take n r
| [], 0, h => by
simp
@ -466,12 +463,11 @@ lemma take_insertIdx {I : Type} (i : I) : (r : List I) → (n : ℕ) → (hn :
simp only [List.insertIdx_succ_cons, List.take_succ_cons, List.cons.injEq, true_and]
exact take_insertIdx i r n (Nat.le_of_lt_succ h)
lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(i : I) [IsTotal I le1] [IsTrans I le1] : (r : List I) → (n : ℕ) → (hn : n ≤ r.length) →
(i : I) [IsTotal I le1] [IsTrans I le1] : (r : List I) → (n : ℕ) → (hn : n ≤ r.length) →
koszulSign le1 q (List.insertIdx n i r) = insertSign q n i r
* koszulSign le1 q r
* insertSign q (insertionSortEquiv le1 (List.insertIdx n i r) ⟨n, by
* koszulSign le1 q r
* insertSign q (insertionSortEquiv le1 (List.insertIdx n i r) ⟨n, by
rw [List.length_insertIdx _ _ hn]
omega⟩) i
(List.insertionSort le1 (List.insertIdx n i r))
@ -482,7 +478,7 @@ lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
| r0 :: r, 0, h => by
simp only [List.insertIdx_zero, List.insertionSort, List.length_cons, Fin.zero_eta]
rw [koszulSign]
trans koszulSign le1 q (r0 :: r) * koszulSignInsert le1 q i (r0 :: r)
trans koszulSign le1 q (r0 :: r) * koszulSignInsert le1 q i (r0 :: r)
ring
simp only [insertionSortEquiv, List.length_cons, Nat.succ_eq_add_one, List.insertionSort,
orderedInsertEquiv, OrderIso.toEquiv_symm, Fin.symm_castOrderIso, HepLean.Fin.equivCons_trans,
@ -533,13 +529,14 @@ lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
omega
exact Nat.le_of_lt_succ h
let ni : Fin rs.length := (insertionSortEquiv le1 (List.insertIdx n i r))
⟨n, hnsL⟩
let nro : Fin (rs.length + 1) := ⟨↑(orderedInsertPos le1 rs r0), orderedInsertPos_lt_length le1 rs r0⟩
⟨n, hnsL⟩
let nro : Fin (rs.length + 1) :=
⟨↑(orderedInsertPos le1 rs r0), orderedInsertPos_lt_length le1 rs r0⟩
rw [koszulSignInsert_insertIdx, koszulSignInsert_cons]
trans koszulSignInsert le1 q r0 r * (koszulSignCons q le1 r0 i *insertSign q ni i rs)
trans koszulSignInsert le1 q r0 r * (koszulSignCons q le1 r0 i *insertSign q ni i rs)
· simp only [rs, ni]
ring
trans koszulSignInsert le1 q r0 r * (superCommuteCoef q [i] [r0] *
trans koszulSignInsert le1 q r0 r * (superCommuteCoef q [i] [r0] *
insertSign q (nro.succAbove ni) i (List.insertIdx nro r0 rs))
swap
· simp only [rs, nro, ni]
@ -596,7 +593,8 @@ lemma insertIdx_eraseIdx {I : Type} :
exact insertIdx_eraseIdx n r _
lemma superCommuteCoefLE_eq_get {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
[DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (i : I) (n : Fin r.length) (heq : q i = q (r.get n)) :
[DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (i : I) (n : Fin r.length)
(heq : q i = q (r.get n)) :
superCommuteCoefLE q le1 r i n = superCommuteCoef q [r.get n] (r.take n) := by
rw [superCommuteCoefLE_eq_q]
let r' := r.eraseIdx ↑n

172
HepLean/PerturbationTheory/Wick/Koszul/OfList.lean
View file

@ -57,7 +57,6 @@ lemma ofList_empty {I : Type} : ofList [] 1 = (1 : FreeAlgebra ℂ I) := by
lemma ofList_empty' {I : Type} : ofList [] x = x • (1 : FreeAlgebra ℂ I) := by
rw [ofList_eq_smul_one, ofList_empty]
lemma koszulOrder_ofList {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(l : List I) (x : ℂ) :
koszulOrder r q (ofList l x) = (koszulSign r q l) • ofList (List.insertionSort r l) x := by
@ -68,8 +67,8 @@ lemma koszulOrder_ofList {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
conv_rhs => rw [ofList_eq_smul_one]
rw [smul_smul]
lemma ofList_insertionSort_eq_koszulOrder {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(l : List I) (x : ℂ) :
lemma ofList_insertionSort_eq_koszulOrder {I : Type} (r : I → I → Prop) [DecidableRel r]
(q : I → Fin 2) (l : List I) (x : ℂ) :
ofList (List.insertionSort r l) x = (koszulSign r q l) • koszulOrder r q (ofList l x) := by
rw [koszulOrder_ofList]
rw [smul_smul]
@ -80,7 +79,7 @@ def freeAlgebraMap {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
FreeAlgebra ℂ I →ₐ[ℂ] FreeAlgebra ℂ (Σ i, f i) :=
FreeAlgebra.lift ℂ fun i => ∑ (j : f i), FreeAlgebra.ι ℂ ⟨i, j⟩
lemma freeAlgebraMap_ι {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
lemma freeAlgebraMap_ι {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
freeAlgebraMap f (FreeAlgebra.ι ℂ i) = ∑ (b : f i), FreeAlgebra.ι ℂ ⟨i, b⟩ := by
simp [freeAlgebraMap]
@ -88,20 +87,20 @@ def ofListM {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) (x :
FreeAlgebra ℂ (Σ i, f i) :=
freeAlgebraMap f (ofList l x)
lemma ofListM_empty {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
lemma ofListM_empty {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
ofListM f [] 1 = 1 := by
simp only [ofListM, EmbeddingLike.map_eq_one_iff]
rw [ofList_empty]
exact map_one (freeAlgebraMap f)
lemma ofListM_empty_smul {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ℂ) :
lemma ofListM_empty_smul {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ℂ) :
ofListM f [] x = x • 1 := by
simp only [ofListM, EmbeddingLike.map_eq_one_iff]
rw [ofList_eq_smul_one]
rw [ofList_empty]
simp
lemma ofListM_cons {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (r : List I) (x : ℂ) :
lemma ofListM_cons {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (r : List I) (x : ℂ) :
ofListM f (i :: r) x = (∑ j : f i, FreeAlgebra.ι ℂ ⟨i, j⟩) * (ofListM f r x) := by
rw [ofListM, ofList_cons_eq_ofList, ofList_singleton, map_mul]
conv_lhs => lhs; rw [freeAlgebraMap]
@ -115,20 +114,21 @@ lemma ofListM_singleton {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i :
rw [freeAlgebraMap_ι]
rw [Finset.smul_sum]
lemma ofListM_singleton_one {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
ofListM f [i] 1 = ∑ j : f i, FreeAlgebra.ι ℂ ⟨i, j⟩ := by
lemma ofListM_singleton_one {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
ofListM f [i] 1 = ∑ j : f i, FreeAlgebra.ι ℂ ⟨i, j⟩ := by
simp only [ofListM]
rw [ofList_eq_smul_one, ofList_singleton, map_smul]
rw [freeAlgebraMap_ι]
rw [Finset.smul_sum]
simp
lemma ofListM_cons_eq_ofListM {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (r : List I) (x : ℂ) :
ofListM f (i :: r) x = ofListM f [i] 1 * ofListM f r x := by
lemma ofListM_cons_eq_ofListM {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I)
(r : List I) (x : ℂ) :
ofListM f (i :: r) x = ofListM f [i] 1 * ofListM f r x := by
rw [ofListM_cons, ofListM_singleton]
simp only [one_smul]
def CreatAnnilateSect {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) : Type :=
def CreatAnnilateSect {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) : Type :=
Π i, f (l.get i)
namespace CreatAnnilateSect
@ -137,13 +137,13 @@ variable {I : Type} {f : I → Type} [∀ i, Fintype (f i)] {l : List I} (a : Cr
instance fintype : Fintype (CreatAnnilateSect f l) := Pi.fintype
def tail : {l : List I} → (a : CreatAnnilateSect f l) → CreatAnnilateSect f l.tail
def tail : {l : List I} → (a : CreatAnnilateSect f l) → CreatAnnilateSect f l.tail
| [], a => a
| _ :: _, a => fun i => a (Fin.succ i)
| _ :: _, a => fun i => a (Fin.succ i)
def head {i : I} (a : CreatAnnilateSect f (i :: l)) : f i := a ⟨0, Nat.zero_lt_succ l.length⟩
def toList : {l : List I} → (a : CreatAnnilateSect f l) → List (Σ i, f i)
def toList : {l : List I} → (a : CreatAnnilateSect f l) → List (Σ i, f i)
| [], _ => []
| i :: _, a => ⟨i, a.head⟩ :: toList a.tail
@ -155,12 +155,12 @@ lemma toList_length : (toList a).length = l.length := by
simp only [toList, List.length_cons, Fin.zero_eta]
rw [ih]
lemma toList_tail : {l : List I} → (a : CreatAnnilateSect f l) → toList a.tail = (toList a).tail
lemma toList_tail : {l : List I} → (a : CreatAnnilateSect f l) → toList a.tail = (toList a).tail
| [], _ => rfl
| i :: l, a => by
simp [toList]
lemma toList_cons {i : I} (a : CreatAnnilateSect f (i :: l)) :
lemma toList_cons {i : I} (a : CreatAnnilateSect f (i :: l)) :
(toList a) = ⟨i, a.head⟩ :: toList a.tail := by
rfl
@ -183,7 +183,7 @@ lemma toList_get (a : CreatAnnilateSect f l) :
simp [tail]
@[simp]
lemma toList_grade (q : I → Fin 2) :
lemma toList_grade (q : I → Fin 2) :
grade (fun i => q i.fst) a.toList = 1 ↔ grade q l = 1 := by
induction l with
| nil =>
@ -191,23 +191,22 @@ lemma toList_grade (q : I → Fin 2) :
| cons i r ih =>
simp only [grade, Fin.isValue, ite_eq_right_iff, zero_ne_one, imp_false]
have ih' := ih (fun i => a i.succ)
have h1 : grade (fun i => q i.fst) a.tail.toList = grade q r := by
have h1 : grade (fun i => q i.fst) a.tail.toList = grade q r := by
by_cases h : grade q r = 1
· simp_all
· have h0 : grade q r = 0 := by
omega
rw [h0] at ih'
simp only [Fin.isValue, zero_ne_one, iff_false] at ih'
have h0' : grade (fun i => q i.fst) a.tail.toList = 0 := by
simp [tail]
have h0' : grade (fun i => q i.fst) a.tail.toList = 0 := by
simp only [List.tail_cons, tail, Fin.isValue]
omega
rw [h0, h0']
rw [h1]
@[simp]
lemma toList_grade_take {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) : (r : List I) → (a : CreatAnnilateSect f r) → (n : ℕ) →
(q : I → Fin 2) : (r : List I) → (a : CreatAnnilateSect f r) → (n : ℕ) →
grade (fun i => q i.fst) (List.take n a.toList) = grade q (List.take n r)
| [], _, _ => by
simp [toList]
@ -217,8 +216,8 @@ lemma toList_grade_take {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
simp only [grade, Fin.isValue]
rw [toList_grade_take q r a.tail n]
def extractEquiv {I : Type} {f : I → Type} [(i : I) → Fintype (f i)] {l : List I} (n : Fin l.length) : CreatAnnilateSect f l ≃
def extractEquiv {I : Type} {f : I → Type} [(i : I) → Fintype (f i)] {l : List I}
(n : Fin l.length) : CreatAnnilateSect f l ≃
f (l.get n) × CreatAnnilateSect f (l.eraseIdx n) := by
match l with
| [] => exact Fin.elim0 n
@ -227,9 +226,10 @@ def extractEquiv {I : Type} {f : I → Type} [(i : I) → Fintype (f i)] {l : L
Equiv.piCongr (Fin.castOrderIso (by rw [eraseIdx_cons_length])).toEquiv
fun x => Equiv.cast (congrArg f (by
rw [HepLean.List.eraseIdx_get]
simp
simp only [List.length_cons, Function.comp_apply, List.get_eq_getElem, Fin.coe_cast,
RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply]
congr 1
simp [Fin.succAbove]
simp only [Fin.succAbove]
split
next h =>
simp_all only [Fin.coe_castSucc]
@ -237,27 +237,27 @@ def extractEquiv {I : Type} {f : I → Type} [(i : I) → Fintype (f i)] {l : L
next h_1 => simp_all only [Fin.coe_castSucc, Fin.coe_cast]
next h_1 =>
simp_all only [not_lt, Fin.val_succ, Fin.coe_cast, self_eq_add_right, one_ne_zero]
simp [Fin.le_def] at h_1
simp [Fin.lt_def] at h
simp only [Fin.le_def, List.length_cons, Fin.coe_castSucc, Fin.coe_cast] at h_1
simp only [Fin.lt_def, Fin.coe_castSucc, Fin.coe_cast] at h
omega
next h =>
simp_all only [not_lt, Fin.val_succ]
split
next h_1 =>
simp_all only [Fin.coe_castSucc, Fin.coe_cast, add_right_eq_self, one_ne_zero]
simp [Fin.lt_def] at h_1
simp [Fin.le_def] at h
simp only [Fin.lt_def, Fin.coe_castSucc, Fin.coe_cast] at h_1
simp only [Fin.le_def, Fin.coe_cast, Fin.coe_castSucc] at h
omega
next h_1 => simp_all only [not_lt, Fin.val_succ, Fin.coe_cast]))
exact (Fin.insertNthEquiv _ _).symm.trans (Equiv.prodCongr (Equiv.refl _) e1.symm)
lemma extractEquiv_symm_toList_get_same {I : Type} {f : I → Type} [(i : I) → Fintype (f i)]
lemma extractEquiv_symm_toList_get_same {I : Type} {f : I → Type} [(i : I) → Fintype (f i)]
{l : List I} (n : Fin l.length) (a0 : f (l.get n)) (a : CreatAnnilateSect f (l.eraseIdx n)) :
((extractEquiv n).symm (a0, a)).toList[n] = ⟨l[n], a0⟩ := by
match l with
| [] => exact Fin.elim0 n
| l0 :: l =>
trans (((CreatAnnilateSect.extractEquiv n).symm (a0, a)).toList).get (Fin.cast (by simp) n)
trans (((CreatAnnilateSect.extractEquiv n).symm (a0, a)).toList).get (Fin.cast (by simp) n)
· simp only [List.length_cons, List.get_eq_getElem, Fin.coe_cast]
rfl
rw [CreatAnnilateSect.toList_get]
@ -270,39 +270,51 @@ lemma extractEquiv_symm_toList_get_same {I : Type} {f : I → Type} [(i : I)
erw [Fin.insertNthEquiv_apply]
simp only [Fin.insertNth_apply_same]
def eraseIdx (n : Fin l.length) : CreatAnnilateSect f (l.eraseIdx n) :=
def eraseIdx (n : Fin l.length) : CreatAnnilateSect f (l.eraseIdx n) :=
(extractEquiv n a).2
@[simp]
lemma eraseIdx_zero_tail {i : I} {l : List I} (a : CreatAnnilateSect f (i :: l)) :
lemma eraseIdx_zero_tail {i : I} {l : List I} (a : CreatAnnilateSect f (i :: l)) :
(eraseIdx a (@OfNat.ofNat (Fin (l.length + 1)) 0 Fin.instOfNat : Fin (l.length + 1))) =
a.tail := by
simp [eraseIdx, extractEquiv]
simp only [List.length_cons, Fin.val_zero, List.eraseIdx_cons_zero, eraseIdx, List.get_eq_getElem,
List.getElem_cons_zero, extractEquiv, Fin.zero_succAbove, Fin.val_succ, List.getElem_cons_succ,
Fin.insertNthEquiv_zero, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.cast_eq_self,
Equiv.cast_refl, Equiv.trans_apply, Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_snd]
rfl
lemma eraseIdx_succ_head {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).length) (a : CreatAnnilateSect f (i :: l)) :
(eraseIdx a ⟨n + 1, hn⟩).head = a.head := by
lemma eraseIdx_succ_head {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).length)
(a : CreatAnnilateSect f (i :: l)) : (eraseIdx a ⟨n + 1, hn⟩).head = a.head := by
rw [eraseIdx, extractEquiv]
simp
simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, List.eraseIdx_cons_succ,
RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Equiv.trans_apply, Equiv.prodCongr_apply,
Equiv.coe_refl, Prod.map_snd]
conv_lhs =>
rhs
rhs
rhs
erw [Fin.insertNthEquiv_symm_apply]
simp [head, Equiv.piCongr, Equiv.piCongrRight, Equiv.piCongrLeft, Equiv.piCongrLeft']
simp [Fin.removeNth, Fin.succAbove]
simp only [head, Equiv.piCongr, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Equiv.piCongrRight,
Equiv.cast_symm, Equiv.piCongrLeft, OrderIso.toEquiv_symm, OrderIso.symm_symm,
Equiv.piCongrLeft', List.length_cons, Fin.zero_eta, Equiv.symm_trans_apply, Equiv.symm_symm,
Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk, Pi.map_apply, Fin.cast_zero, Fin.val_zero,
List.getElem_cons_zero, Equiv.cast_apply]
simp only [Fin.succAbove, Fin.castSucc_zero', Fin.removeNth]
refine cast_eq_iff_heq.mpr ?_
congr
simp [Fin.ext_iff]
lemma eraseIdx_succ_tail {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).length) (a : CreatAnnilateSect f (i :: l)) :
(eraseIdx a ⟨n + 1, hn⟩).tail = eraseIdx a.tail ⟨n , Nat.succ_lt_succ_iff.mp hn⟩ := by
lemma eraseIdx_succ_tail {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).length)
(a : CreatAnnilateSect f (i :: l)) :
(eraseIdx a ⟨n + 1, hn⟩).tail = eraseIdx a.tail ⟨n, Nat.succ_lt_succ_iff.mp hn⟩ := by
match l with
| [] =>
simp at hn
| r0 :: r =>
rw [eraseIdx, extractEquiv]
simp
simp only [List.length_cons, List.eraseIdx_cons_succ, List.tail_cons, List.get_eq_getElem,
List.getElem_cons_succ, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Equiv.trans_apply,
Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_snd, Nat.succ_eq_add_one]
conv_lhs =>
rhs
rhs
@ -314,18 +326,23 @@ lemma eraseIdx_succ_tail {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).l
rw [extractEquiv]
simp
erw [Fin.insertNthEquiv_symm_apply]
simp [tail, Equiv.piCongr, Equiv.piCongrRight, Equiv.piCongrLeft, Equiv.piCongrLeft']
simp only [tail, List.tail_cons, Equiv.piCongr, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Equiv.piCongrRight, Equiv.cast_symm, Equiv.piCongrLeft, OrderIso.toEquiv_symm,
OrderIso.symm_symm, Equiv.piCongrLeft', Equiv.symm_trans_apply, Equiv.symm_symm,
Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk, Pi.map_apply, Fin.cast_succ_eq, Fin.val_succ,
List.getElem_cons_succ, Equiv.cast_apply, List.get_eq_getElem, List.length_cons, Fin.succ_mk,
Prod.map_apply, id_eq]
funext i
simp
simp only [Pi.map_apply, Equiv.cast_apply]
have hcast {α β : Type} (h : α = β) (a : α) (b : β) : cast h a = b ↔ a = cast (Eq.symm h) b := by
cases h
simp
rw [hcast]
simp
simp only [cast_cast]
refine eq_cast_iff_heq.mpr ?_
simp [Fin.removeNth, Fin.succAbove]
simp only [Fin.succAbove, Fin.removeNth]
congr
simp [Fin.ext_iff]
simp only [List.length_cons, Fin.ext_iff, Fin.val_succ]
split
next h =>
simp_all only [Fin.coe_castSucc, Fin.val_succ, Fin.coe_cast, add_left_inj]
@ -333,29 +350,32 @@ lemma eraseIdx_succ_tail {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).l
next h_1 => simp_all only [Fin.coe_castSucc, Fin.coe_cast]
next h_1 =>
simp_all only [not_lt, Fin.val_succ, Fin.coe_cast, self_eq_add_right, one_ne_zero]
simp [Fin.lt_def] at h
simp [Fin.le_def] at h_1
simp only [Fin.lt_def, Fin.coe_castSucc, Fin.val_succ, Fin.coe_cast, add_lt_add_iff_right]
at h
simp only [Fin.le_def, Fin.coe_castSucc, Fin.coe_cast] at h_1
omega
next h =>
simp_all only [not_lt, Fin.val_succ, Fin.coe_cast, add_left_inj]
split
next h_1 =>
simp_all only [Fin.coe_castSucc, Fin.coe_cast, add_right_eq_self, one_ne_zero]
simp [Fin.le_def] at h
simp [Fin.lt_def] at h_1
simp only [Fin.le_def, Fin.coe_castSucc, Fin.val_succ, Fin.coe_cast, add_le_add_iff_right]
at h
simp only [Fin.lt_def, Fin.coe_castSucc, Fin.coe_cast] at h_1
omega
next h_1 => simp_all only [not_lt, Fin.val_succ, Fin.coe_cast]
lemma eraseIdx_toList : {l : List I} → {n : Fin l.length} → (a : CreatAnnilateSect f l) →
lemma eraseIdx_toList : {l : List I} → {n : Fin l.length} → (a : CreatAnnilateSect f l) →
(eraseIdx a n).toList = a.toList.eraseIdx n
| [], n, _ => Fin.elim0 n
| r0 :: r, ⟨0, h⟩, a => by
simp [toList_tail]
| r0 :: r, ⟨n + 1, h⟩, a => by
simp [toList]
simp only [toList, List.length_cons, List.tail_cons, List.eraseIdx_cons_succ, List.cons.injEq,
Sigma.mk.inj_iff, heq_eq_eq, true_and]
apply And.intro
· rw [eraseIdx_succ_head]
· conv_rhs => rw [← eraseIdx_toList (l := r) (n := ⟨n, Nat.succ_lt_succ_iff.mp h⟩) a.tail]
· conv_rhs => rw [← eraseIdx_toList (l := r) (n := ⟨n, Nat.succ_lt_succ_iff.mp h⟩) a.tail]
rw [eraseIdx_succ_tail]
lemma extractEquiv_symm_eraseIdx {I : Type} {f : I → Type} [(i : I) → Fintype (f i)]
@ -367,34 +387,33 @@ lemma extractEquiv_symm_eraseIdx {I : Type} {f : I → Type} [(i : I) → Fintyp
rw [eraseIdx, extractEquiv]
simp
lemma toList_koszulSignInsert {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
lemma toList_koszulSignInsert {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(l : List I) (a : CreatAnnilateSect f l) (x : (i : I) × f i):
koszulSignInsert (fun i j => le1 i.fst j.fst) (fun i => q i.fst) x a.toList =
(l : List I) (a : CreatAnnilateSect f l) (x : (i : I) × f i) :
koszulSignInsert (fun i j => le1 i.fst j.fst) (fun i => q i.fst) x a.toList =
koszulSignInsert le1 q x.1 l := by
induction l with
| nil => simp [koszulSignInsert]
| cons b l ih =>
simp [koszulSignInsert]
simp only [koszulSignInsert, List.tail_cons, Fin.isValue]
rw [ih]
lemma toList_koszulSign {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
lemma toList_koszulSign {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(l : List I) (a : CreatAnnilateSect f l) :
koszulSign (fun i j => le1 i.fst j.fst) (fun i => q i.fst) a.toList =
koszulSign (fun i j => le1 i.fst j.fst) (fun i => q i.fst) a.toList =
koszulSign le1 q l := by
induction l with
| nil => simp [koszulSign]
| cons i l ih =>
simp [koszulSign, liftM]
simp only [koszulSign, List.tail_cons]
rw [ih]
congr 1
rw [toList_koszulSignInsert]
lemma insertionSortEquiv_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(le1 : I → I → Prop) [DecidableRel le1](l : List I)
(a : CreatAnnilateSect f l) :
(a : CreatAnnilateSect f l) :
insertionSortEquiv (fun i j => le1 i.fst j.fst) a.toList =
(Fin.castOrderIso (by simp)).toEquiv.trans ((insertionSortEquiv le1 l).trans
(Fin.castOrderIso (by simp)).toEquiv) := by
@ -413,14 +432,14 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i
conv_rhs => simp [HepLean.List.insertionSortEquiv]
simp only [Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.cast_trans,
Fin.coe_cast]
have h2' (i : Σ i, f i) (l' : List ( Σ i, f i)) :
have h2' (i : Σ i, f i) (l' : List (Σ i, f i)) :
List.map (fun i => i.1) (List.orderedInsert (fun i j => le1 i.fst j.fst) i l') =
List.orderedInsert le1 i.1 (List.map (fun i => i.1) l') := by
induction l' with
| nil =>
simp [HepLean.List.orderedInsertEquiv]
| cons j l' ih' =>
by_cases hij : (fun i j => le1 i.fst j.fst) i j
by_cases hij : (fun i j => le1 i.fst j.fst) i j
· rw [List.orderedInsert_of_le]
· erw [List.orderedInsert_of_le]
· simp
@ -430,7 +449,7 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i
have hn : ¬ le1 i.1 j.1 := hij
simp only [hn, ↓reduceIte, List.cons.injEq, true_and]
simpa using ih'
have h2 (l' : List ( Σ i, f i)) :
have h2 (l' : List (Σ i, f i)) :
List.map (fun i => i.1) (List.insertionSort (fun i j => le1 i.fst j.fst) l') =
List.insertionSort le1 (List.map (fun i => i.1) l') := by
induction l' with
@ -462,7 +481,6 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i
Fin.cast_trans, Fin.cast_eq_self, Fin.coe_cast]
rfl
def sort (le1 : I → I → Prop) [DecidableRel le1] : CreatAnnilateSect f (List.insertionSort le1 l) :=
Equiv.piCongr (HepLean.List.insertionSortEquiv le1 l) (fun i => (Equiv.cast (by
congr 1
@ -470,8 +488,8 @@ def sort (le1 : I → I → Prop) [DecidableRel le1] : CreatAnnilateSect f (List
simp))) a
lemma sort_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(le1 : I → I → Prop) [DecidableRel le1](l : List I) (a : CreatAnnilateSect f l) :
(a.sort le1).toList = List.insertionSort (fun i j => le1 i.fst j.fst) a.toList := by
(le1 : I → I → Prop) [DecidableRel le1] (l : List I) (a : CreatAnnilateSect f l) :
(a.sort le1).toList = List.insertionSort (fun i j => le1 i.fst j.fst) a.toList := by
let l1 := List.insertionSort (fun i j => le1 i.fst j.fst) a.toList
let l2 := (a.sort le1).toList
symm
@ -483,14 +501,16 @@ lemma sort_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
rw [toList_get, toList_get]
funext i
rw [insertionSortEquiv_toList]
simp only [ Function.comp_apply, Equiv.symm_trans_apply,
simp only [Function.comp_apply, Equiv.symm_trans_apply,
OrderIso.toEquiv_symm, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Fin.cast_trans, Fin.cast_eq_self, id_eq, eq_mpr_eq_cast, Fin.coe_cast, Sigma.mk.inj_iff]
apply And.intro
· have h1 := congrFun (HepLean.List.insertionSortEquiv_get (r := le1) l) (Fin.cast (by simp) i)
rw [← h1]
simp
· simp [Equiv.piCongr, sort]
· simp only [List.get_eq_getElem, sort, Equiv.piCongr, Equiv.trans_apply, Fin.coe_cast,
Equiv.piCongrLeft_apply, Equiv.piCongrRight_apply, Pi.map_apply, Equiv.cast_apply,
heq_eqRec_iff_heq]
exact (cast_heq _ _).symm
apply List.ext_get hlen
rw [hget]
@ -498,8 +518,7 @@ lemma sort_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
end CreatAnnilateSect
lemma ofListM_expand {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ℂ) :
lemma ofListM_expand {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ℂ) :
(l : List I) → ofListM f l x = ∑ (a : CreatAnnilateSect f l), ofList a.toList x
| [] => by
simp only [ofListM, CreatAnnilateSect, List.length_nil, List.get_eq_getElem, Finset.univ_unique,
@ -543,7 +562,8 @@ lemma koszulOrder_ofListM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
intro n
rw [← CreatAnnilateSect.sort_toList]
rw [ofListM_expand]
refine Fintype.sum_equiv ((HepLean.List.insertionSortEquiv le1 l).piCongr fun i => Equiv.cast ?_) _ _ ?_
refine Fintype.sum_equiv
((HepLean.List.insertionSortEquiv le1 l).piCongr fun i => Equiv.cast ?_) _ _ ?_
congr 1
· rw [← HepLean.List.insertionSortEquiv_get]
simp

61
HepLean/PerturbationTheory/Wick/Koszul/OperatorMap.lean
View file

@ -16,17 +16,18 @@ namespace Wick
noncomputable section
class OperatorMap {A : Type} [Semiring A] [Algebra ℂ A]
(q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (F : FreeAlgebra ℂ I →ₐ[ℂ] A) : Prop where
superCommute_mem_center : ∀ i j, F (superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j)) ∈ Subalgebra.center ℂ A
superCommute_diff_grade_zero : ∀ i j, q i ≠ q j → F (superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j)) = 0
superCommute_ordered_zero : ∀ i j, ∀ a b,
class OperatorMap {A : Type} [Semiring A] [Algebra ℂ A] (q : I → Fin 2) (le1 : I → I → Prop)
[DecidableRel le1] (F : FreeAlgebra ℂ I →ₐ[ℂ] A) : Prop where
superCommute_mem_center : ∀ i j, F (superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j)) ∈
Subalgebra.center ℂ A
superCommute_diff_grade_zero : ∀ i j, q i ≠ q j →
F (superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j)) = 0
superCommute_ordered_zero : ∀ i j, ∀ a b,
F (koszulOrder le1 q (a * superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j) * b)) = 0
namespace OperatorMap
variable {A : Type} [Semiring A] [Algebra ℂ A] {q : I → Fin 2} {le1 : I → I → Prop}
variable {A : Type} [Semiring A] [Algebra ℂ A] {q : I → Fin 2} {le1 : I → I → Prop}
[DecidableRel le1] (F : FreeAlgebra ℂ I →ₐ[ℂ] A)
lemma superCommute_ofList_singleton_ι_center [OperatorMap q le1 F] (i j :I) :
@ -42,21 +43,20 @@ lemma superCommute_ofList_singleton_ι_center [OperatorMap q le1 F] (i j :I) :
refine Subalgebra.smul_mem (Subalgebra.center ℂ A) ?_ xa
exact superCommute_mem_center (le1 := le1) i j
end OperatorMap
lemma superCommuteTake_operatorMap {I : Type} (q : I → Fin 2)
(le1 : I → I → Prop) [DecidableRel le1]
(lb : List I) (xa xb : ℂ) (n : ℕ)
(hn : n < lb.length) {A : Type} [Semiring A] [Algebra ℂ A] (f : FreeAlgebra ℂ I →ₐ[ℂ] A)
(hn : n < lb.length) {A : Type} [Semiring A] [Algebra ℂ A] (f : FreeAlgebra ℂ I →ₐ[ℂ] A)
[OperatorMap q le1 f] (i : I) :
f (superCommuteTake q [i] lb xa xb n hn) =
f (superCommute q (ofList [i] xa) (FreeAlgebra.ι ℂ (lb.get ⟨n, hn⟩)))
* (superCommuteCoef q [i] (List.take n lb) •
f (ofList (List.eraseIdx lb n) xb)) := by
have hn : f ((superCommute q) (ofList [i] xa) (FreeAlgebra.ι ℂ (lb.get ⟨n, hn⟩))) ∈
Subalgebra.center ℂ A := OperatorMap.superCommute_ofList_singleton_ι_center (le1 := le1) f i (lb.get ⟨n, hn⟩)
Subalgebra.center ℂ A :=
OperatorMap.superCommute_ofList_singleton_ι_center (le1 := le1) f i (lb.get ⟨n, hn⟩)
rw [Subalgebra.mem_center_iff] at hn
rw [superCommuteTake, map_mul, map_mul, map_smul, hn, mul_assoc, smul_mul_assoc,
← map_mul, ← ofList_pair]
@ -64,22 +64,22 @@ lemma superCommuteTake_operatorMap {I : Type} (q : I → Fin 2)
· exact Eq.symm (List.eraseIdx_eq_take_drop_succ lb n)
· exact one_mul xb
lemma superCommuteTakeM_operatorMap {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (c : (Σ i, f i)) (r : List I) (x y : ℂ) (n : ℕ)
(q : I → Fin 2) (c : (Σ i, f i)) (r : List I) (x y : ℂ) (n : ℕ)
(hn : n < r.length)
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
{A : Type} [Semiring A] [Algebra ℂ A] (F : FreeAlgebra ℂ (Σ i, f i) →ₐ[ℂ] A)
{A : Type} [Semiring A] [Algebra ℂ A] (F : FreeAlgebra ℂ (Σ i, f i) →ₐ[ℂ] A)
[OperatorMap (fun i => q i.1) le1 F] :
F (superCommuteTakeM q [c] r x y n hn) = superCommuteCoefM q [c] (List.take n r) •
(F (superCommute (fun i => q i.1) (ofList [c] x) (freeAlgebraMap f (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩))))
(F (superCommute (fun i => q i.1) (ofList [c] x)
(freeAlgebraMap f (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩))))
* F (ofListM f (List.eraseIdx r n) y)) := by
rw [superCommuteTakeM]
rw [map_smul]
congr
rw [map_mul, map_mul]
have h1 : F ((superCommute fun i => q i.fst) (ofList [c] x) ((freeAlgebraMap f) (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩))))
∈ Subalgebra.center ℂ A := by
have h1 : F ((superCommute fun i => q i.fst) (ofList [c] x) ((freeAlgebraMap f)
(FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩)))) ∈ Subalgebra.center ℂ A := by
rw [freeAlgebraMap_ι]
rw [map_sum, map_sum]
refine Subalgebra.sum_mem _ ?_
@ -146,7 +146,7 @@ lemma koszulOrder_of_le_all_ofList {I : Type}
{A : Type} [Semiring A] [Algebra ℂ A]
(F : FreeAlgebra ℂ I →ₐ A) [OperatorMap q le1 F] :
F (koszulOrder le1 q (ofList r x * FreeAlgebra.ι ℂ i))
= superCommuteCoef q [i] r • F (koszulOrder le1 q (FreeAlgebra.ι ℂ i * ofList r x)) := by
= superCommuteCoef q [i] r • F (koszulOrder le1 q (FreeAlgebra.ι ℂ i * ofList r x)) := by
conv_lhs =>
enter [2, 2]
rw [← ofList_singleton]
@ -170,8 +170,8 @@ lemma koszulOrder_of_le_all_ofList {I : Type}
intro n
rw [Algebra.smul_mul_assoc, Algebra.smul_mul_assoc]
rw [map_smul, map_smul]
rw [OperatorMap.superCommute_ordered_zero ]
simp
rw [OperatorMap.superCommute_ordered_zero]
simp only [smul_zero, Finset.sum_const_zero, add_zero]
rw [ofList_singleton]
lemma le_all_mul_koszulOrder_ofList {I : Type}
@ -206,7 +206,8 @@ def superCommuteCenterOrder {I : Type}
(n : Option (Fin r.length)) : A :=
match n with
| none => 1
| some n => superCommuteCoef q [r.get n] (r.take n) • F (((superCommute q) (ofList [i] 1)) (FreeAlgebra.ι ℂ (r.get n)))
| some n => superCommuteCoef q [r.get n] (r.take n) • F (((superCommute q) (ofList [i] 1))
(FreeAlgebra.ι ℂ (r.get n)))
@[simp]
lemma superCommuteCenterOrder_none {I : Type}
@ -225,7 +226,8 @@ lemma le_all_mul_koszulOrder_ofList_expand {I : Type}
{A : Type} [Semiring A] [Algebra ℂ A]
(F : FreeAlgebra ℂ I →ₐ[ℂ] A) [OperatorMap q le1 F] :
F (FreeAlgebra.ι ℂ i * koszulOrder le1 q (ofList r x)) =
∑ n, superCommuteCenterOrder q r i F n * F ((koszulOrder le1 q) (ofList (optionEraseZ r i n) x)) := by
∑ n, superCommuteCenterOrder q r i F n *
F ((koszulOrder le1 q) (ofList (optionEraseZ r i n) x)) := by
rw [le_all_mul_koszulOrder_ofList]
conv_lhs =>
rhs
@ -272,7 +274,7 @@ lemma le_all_mul_koszulOrder_ofListM_expand {I : Type} {f : I → Type} [∀ i,
rhs
intro n
rw [Finset.sum_comm]
simp only [ Fintype.sum_option]
simp only [Fintype.sum_option]
congr 1
· simp only [List.length_cons, List.get_eq_getElem, superCommuteCenterOrder,
Equiv.optionCongr_symm, OrderIso.toEquiv_symm, Fin.symm_castOrderIso, Equiv.optionCongr_apply,
@ -290,15 +292,18 @@ lemma le_all_mul_koszulOrder_ofListM_expand {I : Type} {f : I → Type} [∀ i,
Fin.symm_castOrderIso, Equiv.optionCongr_apply, RelIso.coe_fn_toEquiv, Option.map_some',
Fin.castOrderIso_apply, Algebra.smul_mul_assoc, e1]
erw [Finset.sum_product]
have h1 (a0 : f (r0 :: r)[↑n]) (a : CreatAnnilateSect f ((r0 :: r).eraseIdx ↑n)):
superCommuteCenterOrder (fun i => q i.fst) ((CreatAnnilateSect.extractEquiv n).symm (a0, a)).toList i F
(some (Fin.cast (by simp) n)) = superCommuteCoef q [(r0 :: r).get n] (List.take (↑n) (r0 :: r)) •
F (((superCommute fun i => q i.fst) (ofList [i] 1)) (FreeAlgebra.ι ℂ ⟨(r0 :: r).get n, a0⟩)) := by
have h1 (a0 : f (r0 :: r)[↑n]) (a : CreatAnnilateSect f ((r0 :: r).eraseIdx ↑n)) :
superCommuteCenterOrder (fun i => q i.fst)
((CreatAnnilateSect.extractEquiv n).symm (a0, a)).toList i F
(some (Fin.cast (by simp) n)) =
superCommuteCoef q [(r0 :: r).get n] (List.take (↑n) (r0 :: r)) •
F (((superCommute fun i => q i.fst) (ofList [i] 1))
(FreeAlgebra.ι ℂ ⟨(r0 :: r).get n, a0⟩)) := by
simp only [superCommuteCenterOrder, List.get_eq_getElem, List.length_cons, Fin.coe_cast]
erw [CreatAnnilateSect.extractEquiv_symm_toList_get_same]
have hsc : superCommuteCoef (fun i => q i.fst) [⟨(r0 :: r).get n, a0⟩]
(List.take (↑n) ((CreatAnnilateSect.extractEquiv n).symm (a0, a)).toList) =
superCommuteCoef q [(r0 :: r).get n] (List.take (↑n) ((r0 :: r))) := by
superCommuteCoef q [(r0 :: r).get n] (List.take (↑n) ((r0 :: r))) := by
simp only [superCommuteCoef, List.get_eq_getElem, List.length_cons, Fin.isValue,
CreatAnnilateSect.toList_grade_take]
rfl

77
HepLean/PerturbationTheory/Wick/Koszul/Order.lean
View file

@ -33,24 +33,24 @@ lemma koszulSignInsert_boson {I : Type} (r : I → I → Prop) [DecidableRel r]
simp only [Fin.isValue, zero_ne_one, false_and, ↓reduceIte, ite_self]
@[simp]
lemma koszulSignInsert_mul_self {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I) :
(l : List I) → koszulSignInsert r q a l * koszulSignInsert r q a l = 1
lemma koszulSignInsert_mul_self {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(a : I) : (l : List I) → koszulSignInsert r q a l * koszulSignInsert r q a l = 1
| [] => by
simp [koszulSignInsert]
| b :: l => by
simp [koszulSignInsert]
simp only [koszulSignInsert, Fin.isValue, mul_ite, ite_mul, neg_mul, mul_neg]
by_cases hr : r a b
· simp [hr]
· simp only [hr, ↓reduceIte]
rw [koszulSignInsert_mul_self]
· simp [hr]
· simp only [hr, ↓reduceIte, Fin.isValue]
by_cases hq : q a = 1 ∧ q b = 1
· simp [hq]
· simp only [hq, Fin.isValue, and_self, ↓reduceIte, neg_neg]
rw [koszulSignInsert_mul_self]
· simp [hq]
· simp only [Fin.isValue, hq, ↓reduceIte]
rw [koszulSignInsert_mul_self]
lemma koszulSignInsert_le_forall {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I)
(l : List I) (hi : ∀ b, r a b) : koszulSignInsert r q a l = 1 := by
lemma koszulSignInsert_le_forall {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(a : I) (l : List I) (hi : ∀ b, r a b) : koszulSignInsert r q a l = 1 := by
induction l with
| nil => rfl
| cons j l ih =>
@ -60,7 +60,7 @@ lemma koszulSignInsert_le_forall {I : Type} (r : I → I → Prop) [DecidableRel
intro h
exact False.elim (h (hi j))
lemma koszulSignInsert_ge_forall_append {I : Type} (r : I → I → Prop) [DecidableRel r]
lemma koszulSignInsert_ge_forall_append {I : Type} (r : I → I → Prop) [DecidableRel r]
(q : I → Fin 2) (l : List I) (j i : I) (hi : ∀ j, r j i) :
koszulSignInsert r q j l = koszulSignInsert r q j (l ++ [i]) := by
induction l with
@ -87,13 +87,13 @@ lemma koszulSign_mul_self {I : Type} (r : I → I → Prop) [DecidableRel r] (q
induction l with
| nil => simp [koszulSign]
| cons a l ih =>
simp [koszulSign]
trans (koszulSignInsert r q a l * koszulSignInsert r q a l) * (koszulSign r q l * koszulSign r q l)
simp only [koszulSign]
trans (koszulSignInsert r q a l * koszulSignInsert r q a l) *
(koszulSign r q l * koszulSign r q l)
ring
rw [ih]
rw [koszulSignInsert_mul_self, mul_one]
@[simp]
lemma koszulSign_freeMonoid_of {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(i : I) : koszulSign r q (FreeMonoid.of i) = 1 := by
@ -101,45 +101,46 @@ lemma koszulSign_freeMonoid_of {I : Type} (r : I → I → Prop) [DecidableRel r
simp only [koszulSign, mul_one]
rfl
lemma koszulSignInsert_erase_boson {I : Type} (q : I → Fin 2) (le1 :I → I → Prop)
[DecidableRel le1] (r0 : I) :
(r : List I) → (n : Fin r.length) → (heq : q (r.get n) = 0) →
[DecidableRel le1] (r0 : I) :
(r : List I) → (n : Fin r.length) → (heq : q (r.get n) = 0) →
koszulSignInsert le1 q r0 (r.eraseIdx n) = koszulSignInsert le1 q r0 r
| [], _, _ => by
simp
| r1 :: r, ⟨0, h⟩, hr => by
simp
simp at hr
simp only [List.eraseIdx_zero, List.tail_cons]
simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
List.getElem_cons_zero, Fin.isValue] at hr
rw [koszulSignInsert]
simp [hr]
| r1 :: r, ⟨n + 1, h⟩, hr => by
simp
simp only [List.eraseIdx_cons_succ]
rw [koszulSignInsert, koszulSignInsert]
rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ hr]
rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ hr]
lemma koszulSign_erase_boson {I : Type} (q : I → Fin 2) (le1 :I → I → Prop)
[DecidableRel le1] :
(r : List I) → (n : Fin r.length) → (heq : q (r.get n) = 0) →
[DecidableRel le1] :
(r : List I) → (n : Fin r.length) → (heq : q (r.get n) = 0) →
koszulSign le1 q (r.eraseIdx n) = koszulSign le1 q r
| [], _ => by
simp
| r0 :: r, ⟨0, h⟩ => by
simp [koszulSign]
simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
List.getElem_cons_zero, Fin.isValue, List.eraseIdx_zero, List.tail_cons, koszulSign]
intro h
rw [koszulSignInsert_boson]
simp
simp only [one_mul]
exact h
| r0 :: r, ⟨n + 1, h⟩ => by
simp
simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, Fin.isValue,
List.eraseIdx_cons_succ]
intro h'
rw [koszulSign, koszulSign]
rw [koszulSign_erase_boson q le1 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩]
rw [koszulSign_erase_boson q le1 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩]
congr 1
rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
exact h'
noncomputable section
/-- Given a relation `r` on `I` sorts elements of `MonoidAlgebra ℂ (FreeMonoid I)` by `r` giving it
@ -199,7 +200,6 @@ lemma koszulOrder_ι {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I
koszulSign_freeMonoid_of, mul_one, Finsupp.single_zero, Finsupp.sum_single_index]
rfl
@[simp]
lemma koszulOrder_single {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(l : FreeMonoid I) :
@ -209,7 +209,7 @@ lemma koszulOrder_single {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
simp [koszulOrder]
@[simp]
lemma koszulOrder_ι_pair {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (i j : I) :
lemma koszulOrder_ι_pair {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (i j : I) :
koszulOrder r q (FreeAlgebra.ι ℂ i * FreeAlgebra.ι ℂ j) =
if r i j then FreeAlgebra.ι ℂ i * FreeAlgebra.ι ℂ j else
(koszulSign r q [i, j]) • (FreeAlgebra.ι ℂ j * FreeAlgebra.ι ℂ i) := by
@ -240,7 +240,7 @@ lemma koszulOrder_ι_pair {I : Type} (r : I → I → Prop) [DecidableRel r] (q
rfl
@[simp]
lemma koszulOrder_one {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
lemma koszulOrder_one {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
koszulOrder r q 1 = 1 := by
trans koszulOrder r q (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [] 1))
congr
@ -263,7 +263,8 @@ lemma mul_koszulOrder_le {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
f ((FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)))
= (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single (i :: l) x)) := by
simp only [LinearMap.coe_mk, AddHom.coe_mk, f]
have hf : FreeAlgebra.ι ℂ i = FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [i] 1) := by
have hf : FreeAlgebra.ι ℂ i = FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
(MonoidAlgebra.single [i] 1) := by
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
rfl
@ -295,7 +296,7 @@ lemma mul_koszulOrder_le {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
exact hi _
· congr 1
rw [koszulSign]
have h1 (l : List I) : koszulSignInsert r q i l = 1 := by
have h1 (l : List I) : koszulSignInsert r q i l = 1 := by
exact koszulSignInsert_le_forall r q i l hi
rw [h1]
simp
@ -303,18 +304,20 @@ lemma mul_koszulOrder_le {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
lemma koszulOrder_mul_ge {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(i : I) (A : FreeAlgebra ℂ I) (hi : ∀ j, r j i) :
koszulOrder r q A * FreeAlgebra.ι ℂ i = koszulOrder r q (A * FreeAlgebra.ι ℂ i) := by
koszulOrder r q A * FreeAlgebra.ι ℂ i = koszulOrder r q (A * FreeAlgebra.ι ℂ i) := by
let f : FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I := {
toFun := fun x => x * FreeAlgebra.ι ℂ i ,
toFun := fun x => x * FreeAlgebra.ι ℂ i,
map_add' := fun x y => by
simp [add_mul],
map_smul' := by simp}
change (f ∘ₗ koszulOrder r q) A = (koszulOrder r q ∘ₗ f) A
have f_single (l : FreeMonoid I) (x : ℂ) :
f ((FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)))
= (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single (l.toList ++ [i]) x)) := by
= (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
(MonoidAlgebra.single (l.toList ++ [i]) x)) := by
simp only [LinearMap.coe_mk, AddHom.coe_mk, f]
have hf : FreeAlgebra.ι ℂ i = FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [i] 1) := by
have hf : FreeAlgebra.ι ℂ i = FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
(MonoidAlgebra.single [i] 1) := by
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
rfl

28
HepLean/PerturbationTheory/Wick/Koszul/SuperCommute.lean
View file

@ -36,12 +36,13 @@ def superCommute {I : Type} (q : I → Fin 2) :
superCommuteAlgebra q
∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap
lemma equivMonoidAlgebraFreeMonoid_freeAlgebra {I : Type} (i : I) :
(FreeAlgebra.equivMonoidAlgebraFreeMonoid (FreeAlgebra.ι ℂ i)) = Finsupp.single (FreeMonoid.of i) 1 := by
lemma equivMonoidAlgebraFreeMonoid_freeAlgebra {I : Type} (i : I) :
(FreeAlgebra.equivMonoidAlgebraFreeMonoid (FreeAlgebra.ι ℂ i)) =
Finsupp.single (FreeMonoid.of i) 1 := by
simp [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.single]
@[simp]
lemma superCommute_ι {I : Type} (q : I → Fin 2) (i j : I) :
lemma superCommute_ι {I : Type} (q : I → Fin 2) (i j : I) :
superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j) =
FreeAlgebra.ι ℂ i * FreeAlgebra.ι ℂ j +
if q i = 1 ∧ q j = 1 then
@ -72,7 +73,7 @@ lemma superCommute_ι {I : Type} (q : I → Fin 2) (i j : I) :
simp only [map_neg, MonoidAlgebra.lift_single, one_smul, neg_inj]
rfl
lemma superCommute_ofList_ofList {I : Type} (q : I → Fin 2) (l r : List I) (x y : ℂ) :
lemma superCommute_ofList_ofList {I : Type} (q : I → Fin 2) (l r : List I) (x y : ℂ) :
superCommute q (ofList l x) (ofList r y) =
ofList (l ++ r) (x * y) + (if grade q l = 1 ∧ grade q r = 1 then
ofList (r ++ l) (y * x) else - ofList (r ++ l) (y * x)) := by
@ -118,7 +119,8 @@ lemma superCommute_zero {I : Type} (q : I → Fin 2) (a : FreeAlgebra ℂ I) :
lemma superCommute_one {I : Type} (q : I → Fin 2) (a : FreeAlgebra ℂ I) :
superCommute q a 1 = 0 := by
let f : FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I := (LinearMap.flip (superCommute q)) 1
have h1 : FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [] 1) = (1 : FreeAlgebra ℂ I) := by
have h1 : FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [] 1) =
(1 : FreeAlgebra ℂ I) := by
simp_all only [EmbeddingLike.map_eq_one_iff]
rfl
have f_single (l : FreeMonoid I) (x : ℂ) :
@ -170,7 +172,7 @@ lemma superCommute_ofList_mul {I : Type} (q : I → Fin 2) (la lb lc : List I) (
· simp only [Fin.isValue, hlc, ↓reduceIte]
simp only [mul_assoc, add_mul, mul_add]
abel
· have hc : grade q lc = 0 := by
· have hc : grade q lc = 0 := by
omega
simp only [Fin.isValue, hc, one_ne_zero, ↓reduceIte, zero_ne_one]
simp only [mul_assoc, add_mul, mul_add, mul_neg, neg_add_rev, neg_neg]
@ -182,7 +184,7 @@ lemma superCommute_ofList_mul {I : Type} (q : I → Fin 2) (la lb lc : List I) (
· simp only [Fin.isValue, hlc, zero_ne_one, ↓reduceIte]
simp only [mul_assoc, add_mul, neg_mul, mul_add]
abel
· have hc : grade q lc = 0 := by
· have hc : grade q lc = 0 := by
omega
simp only [Fin.isValue, hc, ↓reduceIte, zero_ne_one]
simp only [mul_assoc, add_mul, neg_mul, mul_add, mul_neg]
@ -208,7 +210,7 @@ lemma superCommute_ofList_cons {I : Type} (q : I → Fin 2) (la lb : List I) (xa
congr
· exact ofList_singleton b1
lemma superCommute_ofList_sum {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) :
lemma superCommute_ofList_sum {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) :
superCommute q (ofList la xa) (ofList lb xb) =
∑ (n : Fin lb.length), superCommuteTake q la lb xa xb n n.prop := by
induction lb with
@ -220,11 +222,11 @@ lemma superCommute_ofList_sum {I : Type} (q : I → Fin 2) (la lb : List I) (xa
abel
| cons b lb ih =>
rw [superCommute_ofList_cons, ih]
have h0 : ((superCommute q) (ofList la xa)) (FreeAlgebra.ι ℂ b) * ofList lb xb =
have h0 : ((superCommute q) (ofList la xa)) (FreeAlgebra.ι ℂ b) * ofList lb xb =
superCommuteTake q la (b :: lb) xa xb 0 (Nat.zero_lt_succ lb.length) := by
simp [superCommuteTake, superCommuteCoef_empty, ofList_empty]
rw [h0]
have hf (f : Fin (b :: lb).length → FreeAlgebra ℂ I) : ∑ n, f n = f ⟨0,
have hf (f : Fin (b :: lb).length → FreeAlgebra ℂ I) : ∑ n, f n = f ⟨0,
Nat.zero_lt_succ lb.length⟩ + ∑ n, f (Fin.succ n) := by
exact Fin.sum_univ_succAbove f ⟨0, Nat.zero_lt_succ lb.length⟩
rw [hf]
@ -241,13 +243,13 @@ lemma superCommute_ofList_sum {I : Type} (q : I → Fin 2) (la lb : List I) (xa
· simp only [← mul_assoc, mul_eq_mul_right_iff]
exact Or.inl (Or.inl (ofList_cons_eq_ofList (List.take (↑n) lb) b 1).symm)
lemma superCommute_ofList_ofList_superCommuteCoef {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) :
superCommute q (ofList la xa) (ofList lb xb) =
lemma superCommute_ofList_ofList_superCommuteCoef {I : Type} (q : I → Fin 2) (la lb : List I)
(xa xb : ℂ) : superCommute q (ofList la xa) (ofList lb xb) =
ofList la xa * ofList lb xb - superCommuteCoef q la lb • ofList lb xb * ofList la xa := by
rw [superCommute_ofList_ofList, superCommuteCoef]
by_cases hq : grade q la = 1 ∧ grade q lb = 1
· simp [hq, ofList_pair]
· simp [hq, ofList_pair]
· simp only [ofList_pair, Fin.isValue, hq, ↓reduceIte, one_smul]
abel
lemma ofList_ofList_superCommute {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) :

26
HepLean/PerturbationTheory/Wick/Koszul/SuperCommuteM.lean
View file

@ -14,7 +14,7 @@ namespace Wick
noncomputable section
lemma superCommute_ofList_ofListM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
lemma superCommute_ofList_ofListM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) =
ofList l x * ofListM f r y +
@ -39,21 +39,21 @@ lemma superCommute_ofList_ofListM {I : Type} {f : I → Type} [∀ i, Fintype (
funext a
rw [superCommute_ofList_ofList]
congr 1
· exact ofList_pair l a.toList x y
· exact ofList_pair l a.toList x y
congr 1
· simp
· exact ofList_pair a.toList l y x
· rw [ofList_pair]
simp only [neg_mul]
lemma superCommute_ofList_ofListM_superCommuteCoefM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
lemma superCommute_ofList_ofListM_superCommuteCoefM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) =
ofList l x * ofListM f r y - superCommuteCoefM q l r • ofListM f r y * ofList l x := by
rw [superCommute_ofList_ofListM, superCommuteCoefM]
by_cases hq : grade (fun i => q i.fst) l = 1 ∧ grade q r = 1
· simp [hq]
· simp [hq]
· simp only [Fin.isValue, hq, ↓reduceIte, neg_mul, one_smul]
abel
lemma ofList_ofListM_superCommute {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
@ -96,7 +96,7 @@ lemma superCommuteCoefM_append {I : Type} {f : I → Type} [∀ i, Fintype (f i)
simp [ha]
def superCommuteTakeM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) (n : ℕ)
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) (n : ℕ)
(hn : n < r.length) : FreeAlgebra ℂ (Σ i, f i) :=
superCommuteCoefM q l (List.take n r) •
(ofListM f (List.take n r) 1 *
@ -106,8 +106,8 @@ def superCommuteTakeM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
lemma superCommuteM_ofList_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) (b1 : I) :
superCommute (fun i => q i.1) (ofList l x) (ofListM f (b1 :: r) y) =
superCommute (fun i => q i.1) (ofList l x) (freeAlgebraMap f (FreeAlgebra.ι ℂ b1)) * ofListM f r y +
superCommuteCoefM q l [b1] •
superCommute (fun i => q i.1) (ofList l x) (freeAlgebraMap f (FreeAlgebra.ι ℂ b1))
* ofListM f r y + superCommuteCoefM q l [b1] •
(ofListM f [b1] 1) * superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) := by
rw [ofListM_cons]
conv_lhs =>
@ -115,7 +115,8 @@ lemma superCommuteM_ofList_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i
rw [ofListM_expand]
rw [Finset.mul_sum]
rw [map_sum]
trans ∑ (n : CreatAnnilateSect f r), ∑ j : f b1, ((superCommute fun i => q i.fst) (ofList l x)) (( FreeAlgebra.ι ℂ ⟨b1, j⟩) * ofList n.toList y)
trans ∑ (n : CreatAnnilateSect f r), ∑ j : f b1, ((superCommute fun i => q i.fst) (ofList l x))
((FreeAlgebra.ι ℂ ⟨b1, j⟩) * ofList n.toList y)
· apply congrArg
funext n
rw [← map_sum]
@ -152,10 +153,10 @@ lemma superCommuteM_ofList_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i
rw [ofList_singleton]
simp
lemma superCommute_ofList_ofListM_sum {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
lemma superCommute_ofList_ofListM_sum {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) =
∑ (n : Fin r.length), superCommuteTakeM q l r x y n n.prop := by
∑ (n : Fin r.length), superCommuteTakeM q l r x y n n.prop := by
induction r with
| nil =>
simp only [superCommute_ofList_ofListM, Fin.isValue, grade_empty, zero_ne_one, and_false,
@ -164,11 +165,12 @@ lemma superCommute_ofList_ofListM_sum {I : Type} {f : I → Type} [∀ i, Finty
simp
| cons b r ih =>
rw [superCommuteM_ofList_cons]
have h0 : ((superCommute fun i => q i.fst) (ofList l x)) ((freeAlgebraMap f) (FreeAlgebra.ι ℂ b)) * ofListM f r y =
have h0 : ((superCommute fun i => q i.fst) (ofList l x))
((freeAlgebraMap f) (FreeAlgebra.ι ℂ b)) * ofListM f r y =
superCommuteTakeM q l (b :: r) x y 0 (Nat.zero_lt_succ r.length) := by
simp [superCommuteTakeM, superCommuteCoefM_empty, ofListM_empty]
rw [h0]
have hf (g : Fin (b :: r).length → FreeAlgebra ℂ ((i : I) × f i)) : ∑ n, g n = g ⟨0,
have hf (g : Fin (b :: r).length → FreeAlgebra ℂ ((i : I) × f i)) : ∑ n, g n = g ⟨0,
Nat.zero_lt_succ r.length⟩ + ∑ n, g (Fin.succ n) := by
exact Fin.sum_univ_succAbove g ⟨0, Nat.zero_lt_succ r.length⟩
rw [hf]