From c9deac6cfe567503ffa62a8abaaff226169f847a Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 23 Jan 2025 10:46:50 +0000 Subject: [PATCH] refactor: Rename asymptotic states --- HepLean/Meta/Basic.lean | 7 ++ .../Algebras/CrAnAlgebra/Basic.lean | 28 ++--- .../Algebras/CrAnAlgebra/NormalOrder.lean | 44 ++++---- .../Algebras/CrAnAlgebra/SuperCommute.lean | 48 ++++----- .../Algebras/ProtoOperatorAlgebra/Basic.lean | 28 ++--- .../ProtoOperatorAlgebra/NormalOrder.lean | 8 +- .../FieldSpecification/Basic.lean | 16 +-- .../FieldSpecification/CrAnStates.lean | 16 +-- .../FieldSpecification/TimeOrder.lean | 24 ++--- .../FieldStatistics/ExchangeSign.lean | 6 +- HepLean/PerturbationTheory/WicksTheorem.lean | 41 ++++--- docs/CuratedNotes/PerturbationTheory.html | 47 ++++++-- docs/assets/css/lean.min.js | 20 ++++ scripts/MetaPrograms/notes.lean | 101 +++++++++++++----- 14 files changed, 279 insertions(+), 155 deletions(-) create mode 100644 docs/assets/css/lean.min.js diff --git a/HepLean/Meta/Basic.lean b/HepLean/Meta/Basic.lean index 197662c..7a41f24 100644 --- a/HepLean/Meta/Basic.lean +++ b/HepLean/Meta/Basic.lean @@ -123,6 +123,13 @@ def Name.hasDocString (c : Name) : MetaM Bool := do | some _ => pure true | none => pure false +def Name.getDocString (c : Name) : MetaM String := do + let env ← getEnv + let doc ← Lean.findDocString? env c + match doc with + | some doc => pure doc + | none => pure "" + /-- Given a name, returns the source code defining that name. -/ def Name.getDeclString (name : Name) : MetaM String := do let env ← getEnv diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean index 9922467..99c3198 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean @@ -137,13 +137,13 @@ lemma ofStateList_sum (Ο†s : List 𝓕.States) : def crPart : 𝓕.StateAlgebra →ₐ[β„‚] 𝓕.CrAnAlgebra := FreeAlgebra.lift β„‚ fun Ο† => match Ο† with - | States.negAsymp Ο† => ofCrAnState ⟨States.negAsymp Ο†, ()⟩ + | States.inAsymp Ο† => ofCrAnState ⟨States.inAsymp Ο†, ()⟩ | States.position Ο† => ofCrAnState ⟨States.position Ο†, CreateAnnihilate.create⟩ - | States.posAsymp _ => 0 + | States.outAsymp _ => 0 @[simp] -lemma crPart_negAsymp (Ο† : 𝓕.AsymptoticNegTime) : - crPart (StateAlgebra.ofState (States.negAsymp Ο†)) = ofCrAnState ⟨States.negAsymp Ο†, ()⟩ := by +lemma crPart_negAsymp (Ο† : 𝓕.IncomingAsymptotic) : + crPart (StateAlgebra.ofState (States.inAsymp Ο†)) = ofCrAnState ⟨States.inAsymp Ο†, ()⟩ := by dsimp only [crPart, StateAlgebra.ofState] rw [FreeAlgebra.lift_ΞΉ_apply] @@ -155,8 +155,8 @@ lemma crPart_position (Ο† : 𝓕.PositionStates) : rw [FreeAlgebra.lift_ΞΉ_apply] @[simp] -lemma crPart_posAsymp (Ο† : 𝓕.AsymptoticPosTime) : - crPart (StateAlgebra.ofState (States.posAsymp Ο†)) = 0 := by +lemma crPart_posAsymp (Ο† : 𝓕.OutgoingAsymptotic) : + crPart (StateAlgebra.ofState (States.outAsymp Ο†)) = 0 := by dsimp only [crPart, StateAlgebra.ofState] rw [FreeAlgebra.lift_ΞΉ_apply] @@ -166,13 +166,13 @@ lemma crPart_posAsymp (Ο† : 𝓕.AsymptoticPosTime) : def anPart : 𝓕.StateAlgebra →ₐ[β„‚] 𝓕.CrAnAlgebra := FreeAlgebra.lift β„‚ fun Ο† => match Ο† with - | States.negAsymp _ => 0 + | States.inAsymp _ => 0 | States.position Ο† => ofCrAnState ⟨States.position Ο†, CreateAnnihilate.annihilate⟩ - | States.posAsymp Ο† => ofCrAnState ⟨States.posAsymp Ο†, ()⟩ + | States.outAsymp Ο† => ofCrAnState ⟨States.outAsymp Ο†, ()⟩ @[simp] -lemma anPart_negAsymp (Ο† : 𝓕.AsymptoticNegTime) : - anPart (StateAlgebra.ofState (States.negAsymp Ο†)) = 0 := by +lemma anPart_negAsymp (Ο† : 𝓕.IncomingAsymptotic) : + anPart (StateAlgebra.ofState (States.inAsymp Ο†)) = 0 := by dsimp only [anPart, StateAlgebra.ofState] rw [FreeAlgebra.lift_ΞΉ_apply] @@ -184,8 +184,8 @@ lemma anPart_position (Ο† : 𝓕.PositionStates) : rw [FreeAlgebra.lift_ΞΉ_apply] @[simp] -lemma anPart_posAsymp (Ο† : 𝓕.AsymptoticPosTime) : - anPart (StateAlgebra.ofState (States.posAsymp Ο†)) = ofCrAnState ⟨States.posAsymp Ο†, ()⟩ := by +lemma anPart_posAsymp (Ο† : 𝓕.OutgoingAsymptotic) : + anPart (StateAlgebra.ofState (States.outAsymp Ο†)) = ofCrAnState ⟨States.outAsymp Ο†, ()⟩ := by dsimp only [anPart, StateAlgebra.ofState] rw [FreeAlgebra.lift_ΞΉ_apply] @@ -193,14 +193,14 @@ lemma ofState_eq_crPart_add_anPart (Ο† : 𝓕.States) : ofState Ο† = crPart (StateAlgebra.ofState Ο†) + anPart (StateAlgebra.ofState Ο†) := by rw [ofState] cases Ο† with - | negAsymp Ο† => + | inAsymp Ο† => dsimp only [statesToCrAnType] simp | position Ο† => dsimp only [statesToCrAnType] rw [CreateAnnihilate.sum_eq] simp - | posAsymp Ο† => + | outAsymp Ο† => dsimp only [statesToCrAnType] simp diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean index 3d85a37..c8674a6 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean @@ -107,30 +107,30 @@ lemma normalOrder_crPart_mul (Ο† : 𝓕.States) (a : CrAnAlgebra 𝓕) : normalOrder (crPart (StateAlgebra.ofState Ο†) * a) = crPart (StateAlgebra.ofState Ο†) * normalOrder a := by match Ο† with - | .negAsymp Ο† => + | .inAsymp Ο† => dsimp only [crPart, StateAlgebra.ofState] simp only [FreeAlgebra.lift_ΞΉ_apply] - exact normalOrder_create_mul ⟨States.negAsymp Ο†, ()⟩ rfl a + exact normalOrder_create_mul ⟨States.inAsymp Ο†, ()⟩ rfl a | .position Ο† => dsimp only [crPart, StateAlgebra.ofState] simp only [FreeAlgebra.lift_ΞΉ_apply] refine normalOrder_create_mul _ ?_ _ simp [crAnStatesToCreateAnnihilate] - | .posAsymp Ο† => + | .outAsymp Ο† => simp lemma normalOrder_mul_anPart (Ο† : 𝓕.States) (a : CrAnAlgebra 𝓕) : normalOrder (a * anPart (StateAlgebra.ofState Ο†)) = normalOrder a * anPart (StateAlgebra.ofState Ο†) := by match Ο† with - | .negAsymp Ο† => + | .inAsymp Ο† => simp | .position Ο† => dsimp only [anPart, StateAlgebra.ofState] simp only [FreeAlgebra.lift_ΞΉ_apply] refine normalOrder_mul_annihilate _ ?_ _ simp [crAnStatesToCreateAnnihilate] - | .posAsymp Ο† => + | .outAsymp Ο† => dsimp only [anPart, StateAlgebra.ofState] simp only [FreeAlgebra.lift_ΞΉ_apply] refine normalOrder_mul_annihilate _ ?_ _ @@ -221,9 +221,9 @@ lemma normalOrder_swap_crPart_anPart (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra normalOrder (a * (anPart (StateAlgebra.ofState Ο†')) * (crPart (StateAlgebra.ofState Ο†)) * b) := by match Ο†, Ο†' with - | _, .negAsymp Ο†' => + | _, .inAsymp Ο†' => simp - | .posAsymp Ο†, _ => + | .outAsymp Ο†, _ => simp | .position Ο†, .position Ο†' => simp only [crPart_position, anPart_position, instCommGroup.eq_1] @@ -231,19 +231,19 @@ lemma normalOrder_swap_crPart_anPart (Ο† Ο†' : 𝓕.States) (a b : CrAnAlgebra simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod] rfl rfl - | .negAsymp Ο†, .posAsymp Ο†' => + | .inAsymp Ο†, .outAsymp Ο†' => simp only [crPart_negAsymp, anPart_posAsymp, instCommGroup.eq_1] rw [normalOrder_swap_create_annihlate] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod] rfl rfl - | .negAsymp Ο†, .position Ο†' => + | .inAsymp Ο†, .position Ο†' => simp only [crPart_negAsymp, anPart_position, instCommGroup.eq_1] rw [normalOrder_swap_create_annihlate] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod] rfl rfl - | .position Ο†, .posAsymp Ο†' => + | .position Ο†, .outAsymp Ο†' => simp only [crPart_position, anPart_posAsymp, instCommGroup.eq_1] rw [normalOrder_swap_create_annihlate] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod] @@ -270,20 +270,20 @@ lemma normalOrder_superCommute_crPart_anPart (Ο† Ο†' : 𝓕.States) (a b : CrAnA normalOrder (a * superCommute (crPart (StateAlgebra.ofState Ο†)) (anPart (StateAlgebra.ofState Ο†')) * b) = 0 := by match Ο†, Ο†' with - | _, .negAsymp Ο†' => + | _, .inAsymp Ο†' => simp - | .posAsymp Ο†', _ => + | .outAsymp Ο†', _ => simp | .position Ο†, .position Ο†' => simp only [crPart_position, anPart_position] refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _ - | .negAsymp Ο†, .posAsymp Ο†' => + | .inAsymp Ο†, .outAsymp Ο†' => simp only [crPart_negAsymp, anPart_posAsymp] refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _ - | .negAsymp Ο†, .position Ο†' => + | .inAsymp Ο†, .position Ο†' => simp only [crPart_negAsymp, anPart_position] refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _ - | .position Ο†, .posAsymp Ο†' => + | .position Ο†, .outAsymp Ο†' => simp only [crPart_position, anPart_posAsymp] refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _ @@ -291,20 +291,20 @@ lemma normalOrder_superCommute_anPart_crPart (Ο† Ο†' : 𝓕.States) (a b : CrAnA normalOrder (a * superCommute (anPart (StateAlgebra.ofState Ο†)) (crPart (StateAlgebra.ofState Ο†')) * b) = 0 := by match Ο†, Ο†' with - | .negAsymp Ο†', _ => + | .inAsymp Ο†', _ => simp - | _, .posAsymp Ο†' => + | _, .outAsymp Ο†' => simp | .position Ο†, .position Ο†' => simp only [anPart_position, crPart_position] refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _ - | .posAsymp Ο†', .negAsymp Ο† => + | .outAsymp Ο†', .inAsymp Ο† => simp only [anPart_posAsymp, crPart_negAsymp] refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _ - | .position Ο†', .negAsymp Ο† => + | .position Ο†', .inAsymp Ο† => simp only [anPart_position, crPart_negAsymp] refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _ - | .posAsymp Ο†, .position Ο†' => + | .outAsymp Ο†, .position Ο†' => simp only [anPart_posAsymp, crPart_position] refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _ @@ -576,13 +576,13 @@ lemma anPart_mul_normalOrder_ofStateList_eq_superCommute (Ο† : 𝓕.States) + ⟨anPart (StateAlgebra.ofState Ο†), normalOrder (ofStateList Ο†s')βŸ©β‚›ca := by rw [normalOrder_mul_anPart] match Ο† with - | .negAsymp Ο† => + | .inAsymp Ο† => simp | .position Ο† => simp only [anPart_position, instCommGroup.eq_1] rw [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute] simp [crAnStatistics] - | .posAsymp Ο† => + | .outAsymp Ο† => simp only [anPart_posAsymp, instCommGroup.eq_1] rw [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute] simp [crAnStatistics] diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean index a2f2757..ee936be 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean @@ -101,26 +101,26 @@ lemma superCommute_anPart_crPart (Ο† Ο†' : 𝓕.States) : anPart (StateAlgebra.ofState Ο†) * crPart (StateAlgebra.ofState Ο†') - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ crPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†) := by match Ο†, Ο†' with - | States.negAsymp Ο†, _ => + | States.inAsymp Ο†, _ => simp - | _, States.posAsymp Ο† => + | _, States.outAsymp Ο† => simp only [crPart_posAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul, sub_self] | States.position Ο†, States.position Ο†' => simp only [anPart_position, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] - | States.posAsymp Ο†, States.position Ο†' => + | States.outAsymp Ο†, States.position Ο†' => simp only [anPart_posAsymp, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] - | States.position Ο†, States.negAsymp Ο†' => + | States.position Ο†, States.inAsymp Ο†' => simp only [anPart_position, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp only [List.singleton_append, instCommGroup.eq_1, crAnStatistics, FieldStatistic.ofList_singleton, Function.comp_apply, crAnStatesToStates_prod, ← ofCrAnList_append] - | States.posAsymp Ο†, States.negAsymp Ο†' => + | States.outAsymp Ο†, States.inAsymp Ο†' => simp only [anPart_posAsymp, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] @@ -131,25 +131,25 @@ lemma superCommute_crPart_anPart (Ο† Ο†' : 𝓕.States) : 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ anPart (StateAlgebra.ofState Ο†') * crPart (StateAlgebra.ofState Ο†) := by match Ο†, Ο†' with - | States.posAsymp Ο†, _ => + | States.outAsymp Ο†, _ => simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1, mul_zero, sub_self] - | _, States.negAsymp Ο† => + | _, States.inAsymp Ο† => simp only [anPart_negAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul, sub_self] | States.position Ο†, States.position Ο†' => simp only [crPart_position, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] - | States.position Ο†, States.posAsymp Ο†' => + | States.position Ο†, States.outAsymp Ο†' => simp only [crPart_position, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] - | States.negAsymp Ο†, States.position Ο†' => + | States.inAsymp Ο†, States.position Ο†' => simp only [crPart_negAsymp, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] - | States.negAsymp Ο†, States.posAsymp Ο†' => + | States.inAsymp Ο†, States.outAsymp Ο†' => simp only [crPart_negAsymp, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] @@ -160,24 +160,24 @@ lemma superCommute_crPart_crPart (Ο† Ο†' : 𝓕.States) : 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ crPart (StateAlgebra.ofState Ο†') * crPart (StateAlgebra.ofState Ο†) := by match Ο†, Ο†' with - | States.posAsymp Ο†, _ => + | States.outAsymp Ο†, _ => simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1, mul_zero, sub_self] - | _, States.posAsymp Ο† => + | _, States.outAsymp Ο† => simp only [crPart_posAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul, sub_self] | States.position Ο†, States.position Ο†' => simp only [crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] - | States.position Ο†, States.negAsymp Ο†' => + | States.position Ο†, States.inAsymp Ο†' => simp only [crPart_position, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] - | States.negAsymp Ο†, States.position Ο†' => + | States.inAsymp Ο†, States.position Ο†' => simp only [crPart_negAsymp, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] - | States.negAsymp Ο†, States.negAsymp Ο†' => + | States.inAsymp Ο†, States.inAsymp Ο†' => simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] @@ -188,23 +188,23 @@ lemma superCommute_anPart_anPart (Ο† Ο†' : 𝓕.States) : 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ anPart (StateAlgebra.ofState Ο†') * anPart (StateAlgebra.ofState Ο†) := by match Ο†, Ο†' with - | States.negAsymp Ο†, _ => + | States.inAsymp Ο†, _ => simp - | _, States.negAsymp Ο† => + | _, States.inAsymp Ο† => simp | States.position Ο†, States.position Ο†' => simp only [anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] - | States.position Ο†, States.posAsymp Ο†' => + | States.position Ο†, States.outAsymp Ο†' => simp only [anPart_position, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] - | States.posAsymp Ο†, States.position Ο†' => + | States.outAsymp Ο†, States.position Ο†' => simp only [anPart_posAsymp, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] - | States.posAsymp Ο†, States.posAsymp Ο†' => + | States.outAsymp Ο†, States.outAsymp Ο†' => simp only [anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, ← ofCrAnList_append] @@ -214,7 +214,7 @@ lemma superCommute_crPart_ofStateList (Ο† : 𝓕.States) (Ο†s : List 𝓕.States crPart (StateAlgebra.ofState Ο†) * ofStateList Ο†s - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s) β€’ ofStateList Ο†s * crPart (StateAlgebra.ofState Ο†) := by match Ο† with - | States.negAsymp Ο† => + | States.inAsymp Ο† => simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList] simp [crAnStatistics] @@ -222,7 +222,7 @@ lemma superCommute_crPart_ofStateList (Ο† : 𝓕.States) (Ο†s : List 𝓕.States simp only [crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList] simp [crAnStatistics] - | States.posAsymp Ο† => + | States.outAsymp Ο† => simp lemma superCommute_anPart_ofStateList (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : @@ -230,13 +230,13 @@ lemma superCommute_anPart_ofStateList (Ο† : 𝓕.States) (Ο†s : List 𝓕.States anPart (StateAlgebra.ofState Ο†) * ofStateList Ο†s - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s) β€’ ofStateList Ο†s * anPart (StateAlgebra.ofState Ο†) := by match Ο† with - | States.negAsymp Ο† => + | States.inAsymp Ο† => simp | States.position Ο† => simp only [anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList] simp [crAnStatistics] - | States.posAsymp Ο† => + | States.outAsymp Ο† => simp only [anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList] simp [crAnStatistics] diff --git a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean index db2709d..125d9ee 100644 --- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean @@ -63,13 +63,13 @@ lemma crAnF_superCommute_ofCrAnState_ofState_mem_center (Ο† : 𝓕.CrAnStates) ( lemma crAnF_superCommute_anPart_ofState_mem_center (Ο† ψ : 𝓕.States) : π“ž.crAnF ⟨anPart (StateAlgebra.ofState Ο†), ofState ΟˆβŸ©β‚›ca ∈ Subalgebra.center β„‚ π“ž.A := by match Ο† with - | States.negAsymp _ => + | States.inAsymp _ => simp only [anPart_negAsymp, map_zero, LinearMap.zero_apply] exact Subalgebra.zero_mem (Subalgebra.center β„‚ π“ž.A) | States.position Ο† => simp only [anPart_position] exact π“ž.crAnF_superCommute_ofCrAnState_ofState_mem_center _ _ - | States.posAsymp _ => + | States.outAsymp _ => simp only [anPart_posAsymp] exact π“ž.crAnF_superCommute_ofCrAnState_ofState_mem_center _ _ @@ -86,13 +86,13 @@ lemma crAnF_superCommute_anPart_ofState_diff_grade_zero (Ο† ψ : 𝓕.States) (h : (𝓕 |>β‚› Ο†) β‰  (𝓕 |>β‚› ψ)) : π“ž.crAnF (superCommute (anPart (StateAlgebra.ofState Ο†)) (ofState ψ)) = 0 := by match Ο† with - | States.negAsymp _ => + | States.inAsymp _ => simp | States.position Ο† => simp only [anPart_position] apply π“ž.crAnF_superCommute_ofCrAnState_ofState_diff_grade_zero _ _ _ simpa [crAnStatistics] using h - | States.posAsymp _ => + | States.outAsymp _ => simp only [anPart_posAsymp] apply π“ž.crAnF_superCommute_ofCrAnState_ofState_diff_grade_zero _ _ simpa [crAnStatistics] using h @@ -108,26 +108,26 @@ lemma crAnF_superCommute_ofState_ofState_mem_center (Ο† ψ : 𝓕.States) : lemma crAnF_superCommute_anPart_anPart (Ο† ψ : 𝓕.States) : π“ž.crAnF ⟨anPart (StateAlgebra.ofState Ο†), anPart (StateAlgebra.ofState ψ)βŸ©β‚›ca = 0 := by match Ο†, ψ with - | _, States.negAsymp _ => + | _, States.inAsymp _ => simp - | States.negAsymp _, _ => + | States.inAsymp _, _ => simp | States.position Ο†, States.position ψ => simp only [anPart_position] rw [π“ž.superCommute_annihilate_annihilate] rfl rfl - | States.position Ο†, States.posAsymp _ => + | States.position Ο†, States.outAsymp _ => simp only [anPart_position, anPart_posAsymp] rw [π“ž.superCommute_annihilate_annihilate] rfl rfl - | States.posAsymp _, States.posAsymp _ => + | States.outAsymp _, States.outAsymp _ => simp only [anPart_posAsymp] rw [π“ž.superCommute_annihilate_annihilate] rfl rfl - | States.posAsymp _, States.position _ => + | States.outAsymp _, States.position _ => simp only [anPart_posAsymp, anPart_position] rw [π“ž.superCommute_annihilate_annihilate] rfl @@ -136,26 +136,26 @@ lemma crAnF_superCommute_anPart_anPart (Ο† ψ : 𝓕.States) : lemma crAnF_superCommute_crPart_crPart (Ο† ψ : 𝓕.States) : π“ž.crAnF ⟨crPart (StateAlgebra.ofState Ο†), crPart (StateAlgebra.ofState ψ)βŸ©β‚›ca = 0 := by match Ο†, ψ with - | _, States.posAsymp _ => + | _, States.outAsymp _ => simp - | States.posAsymp _, _ => + | States.outAsymp _, _ => simp | States.position Ο†, States.position ψ => simp only [crPart_position] rw [π“ž.superCommute_create_create] rfl rfl - | States.position Ο†, States.negAsymp _ => + | States.position Ο†, States.inAsymp _ => simp only [crPart_position, crPart_negAsymp] rw [π“ž.superCommute_create_create] rfl rfl - | States.negAsymp _, States.negAsymp _ => + | States.inAsymp _, States.inAsymp _ => simp only [crPart_negAsymp] rw [π“ž.superCommute_create_create] rfl rfl - | States.negAsymp _, States.position _ => + | States.inAsymp _, States.position _ => simp only [crPart_negAsymp, crPart_position] rw [π“ž.superCommute_create_create] rfl diff --git a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean index 0c5a538..87905b6 100644 --- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean @@ -222,13 +222,13 @@ lemma crAnF_normalOrder_anPart_ofStatesList_swap (Ο† : 𝓕.States) 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ π“ž.crAnF (normalOrder (ofStateList Ο†' * anPart (StateAlgebra.ofState Ο†))) := by match Ο† with - | .negAsymp Ο† => + | .inAsymp Ο† => simp | .position Ο† => simp only [anPart_position, instCommGroup.eq_1] rw [crAnF_normalOrder_ofCrAnState_ofStatesList_swap] rfl - | .posAsymp Ο† => + | .outAsymp Ο† => simp only [anPart_posAsymp, instCommGroup.eq_1] rw [crAnF_normalOrder_ofCrAnState_ofStatesList_swap] rfl @@ -309,13 +309,13 @@ lemma crAnF_anPart_superCommute_normalOrder_ofStateList_eq_sum (Ο† : 𝓕.States π“ž.crAnF (⟨anPart (StateAlgebra.ofState Ο†), ofState Ο†s[n]βŸ©β‚›ca) * π“ž.crAnF (normalOrder (ofStateList (Ο†s.eraseIdx n))) := by match Ο† with - | .negAsymp Ο† => + | .inAsymp Ο† => simp | .position Ο† => simp only [anPart_position, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc] rw [crAnF_ofCrAnState_superCommute_normalOrder_ofStateList_eq_sum] simp [crAnStatistics] - | .posAsymp Ο† => + | .outAsymp Ο† => simp only [anPart_posAsymp, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc] rw [crAnF_ofCrAnState_superCommute_normalOrder_ofStateList_eq_sum] simp [crAnStatistics] diff --git a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean index aff7605..fee180c 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean @@ -44,26 +44,26 @@ structure FieldSpecification where namespace FieldSpecification variable (𝓕 : FieldSpecification) -/-- Negative asymptotic states are specified by a field and a momentum. -/ -def AsymptoticNegTime : Type := 𝓕.Fields Γ— Lorentz.Contr 4 +/-- Incoming asymptotic states are specified by a field and a momentum. -/ +def IncomingAsymptotic : Type := 𝓕.Fields Γ— Lorentz.Contr 4 -/-- Positive asymptotic states are specified by a field and a momentum. -/ -def AsymptoticPosTime : Type := 𝓕.Fields Γ— Lorentz.Contr 4 +/-- Outgoing asymptotic states are specified by a field and a momentum. -/ +def OutgoingAsymptotic : Type := 𝓕.Fields Γ— Lorentz.Contr 4 /-- States specified by a field and a space-time position. -/ def PositionStates : Type := 𝓕.Fields Γ— SpaceTime /-- The combination of asymptotic states and position states. -/ inductive States (𝓕 : FieldSpecification) where - | negAsymp : 𝓕.AsymptoticNegTime β†’ 𝓕.States + | inAsymp : 𝓕.IncomingAsymptotic β†’ 𝓕.States | position : 𝓕.PositionStates β†’ 𝓕.States - | posAsymp : 𝓕.AsymptoticPosTime β†’ 𝓕.States + | outAsymp : 𝓕.OutgoingAsymptotic β†’ 𝓕.States /-- Taking a state to its underlying field. -/ def statesToField : 𝓕.States β†’ 𝓕.Fields - | States.negAsymp Ο† => Ο†.1 + | States.inAsymp Ο† => Ο†.1 | States.position Ο† => Ο†.1 - | States.posAsymp Ο† => Ο†.1 + | States.outAsymp Ο† => Ο†.1 /-- The statistics associated to a state. -/ def statesStatistic : 𝓕.States β†’ FieldStatistic := 𝓕.statistics ∘ 𝓕.statesToField diff --git a/HepLean/PerturbationTheory/FieldSpecification/CrAnStates.lean b/HepLean/PerturbationTheory/FieldSpecification/CrAnStates.lean index dae35ee..5ecab57 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/CrAnStates.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/CrAnStates.lean @@ -38,23 +38,23 @@ variable (𝓕 : FieldSpecification) For asymptotic staes there is only one allowed part, whilst for position states there is two. -/ def statesToCrAnType : 𝓕.States β†’ Type - | States.negAsymp _ => Unit + | States.inAsymp _ => Unit | States.position _ => CreateAnnihilate - | States.posAsymp _ => Unit + | States.outAsymp _ => Unit /-- The instance of a finite type on `𝓕.statesToCreateAnnihilateType i`. -/ instance : βˆ€ i, Fintype (𝓕.statesToCrAnType i) := fun i => match i with - | States.negAsymp _ => inferInstanceAs (Fintype Unit) + | States.inAsymp _ => inferInstanceAs (Fintype Unit) | States.position _ => inferInstanceAs (Fintype CreateAnnihilate) - | States.posAsymp _ => inferInstanceAs (Fintype Unit) + | States.outAsymp _ => inferInstanceAs (Fintype Unit) /-- The instance of a decidable equality on `𝓕.statesToCreateAnnihilateType i`. -/ instance : βˆ€ i, DecidableEq (𝓕.statesToCrAnType i) := fun i => match i with - | States.negAsymp _ => inferInstanceAs (DecidableEq Unit) + | States.inAsymp _ => inferInstanceAs (DecidableEq Unit) | States.position _ => inferInstanceAs (DecidableEq CreateAnnihilate) - | States.posAsymp _ => inferInstanceAs (DecidableEq Unit) + | States.outAsymp _ => inferInstanceAs (DecidableEq Unit) /-- The equivalence between `𝓕.statesToCreateAnnihilateType i` and `𝓕.statesToCreateAnnihilateType j` from an equality `i = j`. -/ @@ -77,10 +77,10 @@ lemma crAnStatesToStates_prod (s : 𝓕.States) (t : 𝓕.statesToCrAnType s) : /-- The map from creation and annihlation states to the type `CreateAnnihilate` specifying if a state is a creation or an annihilation state. -/ def crAnStatesToCreateAnnihilate : 𝓕.CrAnStates β†’ CreateAnnihilate - | ⟨States.negAsymp _, _⟩ => CreateAnnihilate.create + | ⟨States.inAsymp _, _⟩ => CreateAnnihilate.create | ⟨States.position _, CreateAnnihilate.create⟩ => CreateAnnihilate.create | ⟨States.position _, CreateAnnihilate.annihilate⟩ => CreateAnnihilate.annihilate - | ⟨States.posAsymp _, _⟩ => CreateAnnihilate.annihilate + | ⟨States.outAsymp _, _⟩ => CreateAnnihilate.annihilate /-- Takes a `CrAnStates` state to its corresponding fields statistic (bosonic or fermionic). -/ def crAnStatistics : 𝓕.CrAnStates β†’ FieldStatistic := diff --git a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean index f3396cb..7cf30ed 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean @@ -19,24 +19,24 @@ variable {𝓕 : FieldSpecification} if and only if `Ο†1` has a time less-then or equal to `Ο†0`, or `Ο†1` is a negative asymptotic state, or `Ο†0` is a positive asymptotic state. -/ def timeOrderRel : 𝓕.States β†’ 𝓕.States β†’ Prop - | States.posAsymp _, _ => True + | States.outAsymp _, _ => True | States.position Ο†0, States.position Ο†1 => Ο†1.2 0 ≀ Ο†0.2 0 - | States.position _, States.negAsymp _ => True - | States.position _, States.posAsymp _ => False - | States.negAsymp _, States.posAsymp _ => False - | States.negAsymp _, States.position _ => False - | States.negAsymp _, States.negAsymp _ => True + | States.position _, States.inAsymp _ => True + | States.position _, States.outAsymp _ => False + | States.inAsymp _, States.outAsymp _ => False + | States.inAsymp _, States.position _ => False + | States.inAsymp _, States.inAsymp _ => True /-- The relation `timeOrderRel` is decidable, but not computablly so due to `Real.decidableLE`. -/ noncomputable instance : (Ο† Ο†' : 𝓕.States) β†’ Decidable (timeOrderRel Ο† Ο†') - | States.posAsymp _, _ => isTrue True.intro + | States.outAsymp _, _ => isTrue True.intro | States.position Ο†0, States.position Ο†1 => inferInstanceAs (Decidable (Ο†1.2 0 ≀ Ο†0.2 0)) - | States.position _, States.negAsymp _ => isTrue True.intro - | States.position _, States.posAsymp _ => isFalse (fun a => a) - | States.negAsymp _, States.posAsymp _ => isFalse (fun a => a) - | States.negAsymp _, States.position _ => isFalse (fun a => a) - | States.negAsymp _, States.negAsymp _ => isTrue True.intro + | States.position _, States.inAsymp _ => isTrue True.intro + | States.position _, States.outAsymp _ => isFalse (fun a => a) + | States.inAsymp _, States.outAsymp _ => isFalse (fun a => a) + | States.inAsymp _, States.position _ => isFalse (fun a => a) + | States.inAsymp _, States.inAsymp _ => isTrue True.intro /-- Time ordering is total. -/ instance : IsTotal 𝓕.States 𝓕.timeOrderRel where diff --git a/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean b/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean index dfd91df..115f0a9 100644 --- a/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean +++ b/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean @@ -24,8 +24,10 @@ namespace FieldStatistic variable {𝓕 : Type} -/-- The echange sign of two field statistics. - Defined to be `-1` if both field statistics are `fermionic` and `1` otherwise. -/ +/-- The exchange sign of two field statistics is defined to be + `-1` if both field statistics are `fermionic` and `1` otherwise. + It is a group homomorphism from `FieldStatistic` to the group of homomorphisms from + `FieldStatistic` to `β„‚`. -/ def exchangeSign : FieldStatistic β†’* FieldStatistic β†’* β„‚ where toFun a := { diff --git a/HepLean/PerturbationTheory/WicksTheorem.lean b/HepLean/PerturbationTheory/WicksTheorem.lean index cdb4a11..9f3f786 100644 --- a/HepLean/PerturbationTheory/WicksTheorem.lean +++ b/HepLean/PerturbationTheory/WicksTheorem.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.TimeContract +import HepLean.Meta.Remark.Basic /-! # Wick's theorem @@ -260,19 +261,6 @@ lemma wicks_theorem_congr {Ο†s Ο†s' : List 𝓕.States} (h : Ο†s = Ο†s') : subst h simp -/-- Wick's theorem for the empty list. -/ -lemma wicks_theorem_nil : - π“ž.crAnF (ofStateAlgebra (timeOrder (ofList []))) = βˆ‘ (c : WickContraction [].length), - (c.sign [] β€’ c.timeContract π“ž) * - π“ž.crAnF (normalOrder (ofStateList (c.uncontractedList.map [].get))) := by - rw [timeOrder_ofList_nil] - simp only [map_one, List.length_nil, Algebra.smul_mul_assoc] - rw [sum_WickContraction_nil, nil_zero_uncontractedList] - simp only [List.map_nil] - have h1 : ofStateList (𝓕 := 𝓕) [] = CrAnAlgebra.ofCrAnList [] := by simp - rw [h1, normalOrder_ofCrAnList] - simp [WickContraction.timeContract, empty, sign] - lemma timeOrder_eq_maxTimeField_mul_finset (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : timeOrder (ofList (Ο† :: Ο†s)) = 𝓒(𝓕 |>β‚› maxTimeField Ο† Ο†s, 𝓕 |>β‚› ⟨(eraseMaxTimeField Ο† Ο†s).get, (Finset.filter (fun x => @@ -320,6 +308,33 @@ lemma timeOrder_eq_maxTimeField_mul_finset (Ο† : 𝓕.States) (Ο†s : List 𝓕.S (Finset.filter (fun x => (maxTimeFieldPosFin Ο† Ο†s).succAbove x < maxTimeFieldPosFin Ο† Ο†s) Finset.univ) + +/-! + +## Wick's theorem + +-/ + +/-- Wick's theorem for the empty list. -/ +lemma wicks_theorem_nil : + π“ž.crAnF (ofStateAlgebra (timeOrder (ofList []))) = βˆ‘ (c : WickContraction [].length), + (c.sign [] β€’ c.timeContract π“ž) * + π“ž.crAnF (normalOrder (ofStateList (c.uncontractedList.map [].get))) := by + rw [timeOrder_ofList_nil] + simp only [map_one, List.length_nil, Algebra.smul_mul_assoc] + rw [sum_WickContraction_nil, nil_zero_uncontractedList] + simp only [List.map_nil] + have h1 : ofStateList (𝓕 := 𝓕) [] = CrAnAlgebra.ofCrAnList [] := by simp + rw [h1, normalOrder_ofCrAnList] + simp [WickContraction.timeContract, empty, sign] + +remark wicks_theorem_context := " + Wick's theorem is one of the most important results in perturbative quantum field theory. + It expresses a time-ordered product of fields as a sum of terms consisting of + time-contractions of pairs of fields multiplied by the normal-ordered product of + the remaining fields. Wick's theorem is also the precursor to the diagrammatic + approach to quantum field theory called Feynman diagrams." + /-- Wick's theorem for time-ordered products of bosonic and fermionic fields. -/ theorem wicks_theorem : (Ο†s : List 𝓕.States) β†’ π“ž.crAnF (ofStateAlgebra (timeOrder (ofList Ο†s))) = βˆ‘ (c : WickContraction Ο†s.length), (c.sign Ο†s β€’ c.timeContract π“ž) * diff --git a/docs/CuratedNotes/PerturbationTheory.html b/docs/CuratedNotes/PerturbationTheory.html index 8d0bc0d..8f65dad 100644 --- a/docs/CuratedNotes/PerturbationTheory.html +++ b/docs/CuratedNotes/PerturbationTheory.html @@ -1,7 +1,16 @@ --- layout: default --- + + + + + +

{{ site.data.perturbationTheory.title }}

+

Note Curators: {{ site.data.perturbationTheory.curators }}

+

Note: @@ -16,27 +25,45 @@ layout: default here.

+ +
+

Table of content

+

+{% for entry in site.data.perturbationTheory.parts %} +{% if entry.type == "h1" %} + {{ entry.sectionNo }}. {{ entry.content }}
+{% endif %} +{% if entry.type == "h2" %} + - {{ entry.sectionNo }}. {{ entry.content }}
+{% endif %} +{% endfor %} +

+
+
{% for entry in site.data.perturbationTheory.parts %} {% if entry.type == "h1" %} -

{{ entry.content }}

+

{{ entry.sectionNo }}. {{ entry.content }}

{% endif %} {% if entry.type == "h2" %} -

{{ entry.content }}

+

{{ entry.sectionNo }}. {{ entry.content }}

{% endif %} {% if entry.type == "p" %}

{{ entry.content }}

{% endif %} {% if entry.type == "name" %} -
- 

-{{ entry.content }}
-
-
+ +
+

{{ entry.name }}: {{ entry.docString }}

+
+ Show Lean code: + 
{{ entry.declString }}
+
+
+ {% endif %} {% if entry.type == "remark" %} -

Remark: - {{ entry.content|markdownify }} -

+

Remark:{{ entry.content|markdownify }} +

{% endif %} {% endfor %} diff --git a/docs/assets/css/lean.min.js b/docs/assets/css/lean.min.js new file mode 100644 index 0000000..855ecf6 --- /dev/null +++ b/docs/assets/css/lean.min.js @@ -0,0 +1,20 @@ +/*! `lean` grammar compiled for Highlight.js 11.9.0 */ +(()=>{var e=(()=>{"use strict";function e(e){ +return e&&e.__esModule&&Object.prototype.hasOwnProperty.call(e,"default")?e.default:e +}return e((e=>{var a={$pattern:/\w+|\u03bb|\u2200|\u03a0|\u2203|:=?/u, +keyword:"theorem|10 lemma|10 definition def class structure instance example inductive coinductive axiom axioms hypothesis constant constants universe universes variable variables parameter parameters begin end infix infixr import open theory prelude renaming hiding exposing calc match do by let in extends fun assume #check #eval #reduce #print \u03bb \u2200 \u2203 \u2a01 \u03a0", +built_in:"Type Prop|10 Sort rw|10 rewrite rwa erw subst substs simp dsimp simpa simp_intros finish unfold unfold1 dunfold unfold_projs unfold_coes delta cc ac_reflexivity ac_refl existsi|10 cases rcases with intro intros introv by_cases refl rfl funext propext exact exacts refine apply eapply fapply apply_with apply_instance induction rename assumption revert generalize specialize clear contradiction by_contradiction by_contra trivial exfalso symmetry transitivity destruct constructor econstructor left right split injection injections repeat try continue skip swap solve1 abstract all_goals any_goals done fail_if_success success_if_fail guard_target guard_hyp have replace at suffices show from congr congr_n congr_arg norm_num ring ", +literal:"tt ff",meta:"noncomputable|10 private protected meta mutual", +section:"section namespace end",sorry:"sorry admit",symbol:":=" +},n=e.COMMENT("--","$"),s=e.COMMENT("/-[^-]","-/"),t={className:"theorem", +beginKeywords:"def theorem lemma class instance structure",end:/:=/, +excludeEnd:!0,contains:[{className:"keyword",begin:/extends/,contains:[{ +className:"symbol",begin:/:=/,endsParent:!0}]},e.inherit(e.TITLE_MODE,{ +begin:/[A-Za-z_][\w\u207F-\u209C\u1D62-\u1D6A\u2079\']*/}),{className:"params", +begin:/[([{]/,end:/[)\]}]/,endsParent:!1,keywords:a},{className:"symbol", +begin:/:=/,endsParent:!0},{className:"symbol",begin:/:/,endsParent:!0}], +keywords:a};return{name:"lean",keywords:a, +contains:[e.QUOTE_STRING_MODE,e.NUMBER_MODE,n,s,{className:"doctag", +begin:"/-[-!]",end:"-/"},t,{className:"meta",begin:"@\\[",end:"\\]"},{ +className:"meta",begin:"^attribute",end:"$"},{begin:/\u27e8/}]}}))})() +;hljs.registerLanguage("lean",e)})(); \ No newline at end of file diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean index abbd4ea..3b04336 100644 --- a/scripts/MetaPrograms/notes.lean +++ b/scripts/MetaPrograms/notes.lean @@ -20,43 +20,70 @@ inductive NotePart | p : String β†’ NotePart | name : Name β†’ NotePart -def formalContent (name : Name) : MetaM String := do - let line ← Name.lineNumber name - let decl ← Name.getDeclString name - let fileName ← Name.fileName name - let webAddress : String ← Name.toGitHubLink fileName line - pure decl +structure DeclInfo where + line : Nat + fileName : Name + name : Name + declString : String + docString : String +def DeclInfo.ofName (n : Name) : MetaM DeclInfo := do + let line ← Name.lineNumber n + let fileName ← Name.fileName n + let declString ← Name.getDeclString n + let docString ← Name.getDocString n + pure { + line := line, + fileName := fileName, + name := n, + declString := declString, + docString := docString} -def NotePart.toYMLM : NotePart β†’ MetaM String - | NotePart.h1 s => pure s!" +def DeclInfo.toYML (d : DeclInfo) : String := + let declStringIndent := d.declString.replace "\n" "\n " + s!" + - type: name + name: {d.name} + line: {d.line} + fileName: {d.fileName} + docString: \"{d.docString}\" + declString: | + {declStringIndent}" + +def NotePart.toYMLM : ((List String) Γ— Nat Γ— Nat) β†’ NotePart β†’ MetaM ((List String) Γ— Nat Γ— Nat) + | x, NotePart.h1 s => + let newString := s!" - type: h1 + sectionNo: {x.2.1.succ} content: \"{s}\"" - | NotePart.h2 s => pure s!" + return ⟨x.1 ++ [newString], ⟨Nat.succ x.2.1, 0⟩⟩ + | x, NotePart.h2 s => + let newString := s!" - type: h2 + sectionNo: \"{x.2.1}.{x.2.2.succ}\" content: \"{s}\"" - | NotePart.p s => pure s!" + return ⟨x.1 ++ [newString], ⟨x.2.1, Nat.succ x.2.2⟩⟩ + | x, NotePart.p s => + let newString := s!" - type: p content: \"{s}\"" - | NotePart.name n => do + return ⟨x.1 ++ [newString], x.2⟩ + | x, NotePart.name n => do match (← RemarkInfo.IsRemark n) with | true => let remarkInfo ← RemarkInfo.getRemarkInfo n let content := remarkInfo.content let contentIndent := content.replace "\n" "\n " let shortName := remarkInfo.name.toString - return s!" + let newString := s!" - type: remark name: \"{shortName}\" content: | {contentIndent}" + return ⟨x.1 ++ [newString], x.2⟩ | false => - let content ← formalContent n - let contentIndent := content.replace "\n" "\n " - return s!" - - type: name - content: | - {contentIndent}" + let newString := (← DeclInfo.ofName n).toYML + return ⟨x.1 ++ [newString], x.2⟩ structure Note where title : String @@ -66,23 +93,49 @@ structure Note where parts : List NotePart def Note.toYML : Note β†’ MetaM String - | ⟨title, curators, parts⟩ => return s!" + | ⟨title, curators, parts⟩ => do + let parts ← parts.foldlM NotePart.toYMLM ([], ⟨0, 0⟩) + return s!" title: \"{title}\" -curators: {curators} +curators: {String.intercalate "," curators} parts: - {String.intercalate "\n" (← parts.mapM NotePart.toYMLM)}" + {String.intercalate "\n" parts.1}" def perturbationTheory : Note where title := "Proof of Wick's theorem" curators := ["Joseph Tooby-Smith"] parts := [ - .h1 "Field statistics", + .h1 "Introduction", + .name `FieldSpecification.wicks_theorem_context, + .p "In this note we walk through the important parts of the proof of Wick's theorem + for both fermions and bosons, + as it appears in HepLean. We start with some basic definitions.", + .h1 "Preliminary definitions", + .h2 "Field statistics", .p "A quantum field can either be a bosonic or fermionic. This information is contained in the inductive type `FieldStatistic`. This is defined as follows:", .name `FieldStatistic, - .h1 "Field specifications", + .p "Field statistics form a commuative group isomorphic to β„€β‚‚, with + the bosonic element of `FieldStatistic` being the identity element.", + .p "Most of our use of field statistics will come by comparing two field statistics + and picking up a minus sign when they are both fermionic. This concept is + made precise using the notion of an exchange sign, defined as:", + .name `FieldStatistic.exchangeSign, + .p "We use the notation `𝓒(a,b)` as shorthand for the exchange sign of + `a` and `b`.", + .h2 "Field specifications", .name `fieldSpecification_intro, - .name `FieldSpecification] + .name `FieldSpecification, + .h2 "States", + .h2 "Time ordering", + .h2 "Creation and annihilation states", + .h2 "Normal ordering", + .h1 "Algebras", + .h2 "State free-algebra", + .h2 "CrAnState free-algebra", + .h2 "Proto operator algebra", + .h1 "Contractions" + ] unsafe def main (_ : List String) : IO UInt32 := do initSearchPath (← findSysroot)