Physlib.QFT.PerturbationTheory.FieldSpecification.Filters

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QFT.PerturbationTheory.FieldSpecification.CrAnFieldOp

Filters of lists of CrAnFieldOp

@[expose] public section

Given a list of creation and annihilation states, the filtered list only containing the creation states. As a schematic example, for the list:

[φ1c, φ1a, φ2c, φ2a] this will return [φ1c, φ2c].

def createFilter (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp :=
  List.filter (fun φ => 𝓕 |>ᶜ φ = CreateAnnihilate.create) φs

              

lemma createFilter_cons_create {φ : 𝓕.CrAnFieldOp}
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnFieldOp) :
    createFilter (φ :: φs) = φ :: createFilter φs := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ createFilter (φ :: φs) = φ :: createFilter φs
  simp only [createFilter]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) (φ :: φs) =
  φ :: List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs
  rw [List.filter_cons_of_pos𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ φ :: List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs =
  φ :: List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ decide (𝓕|>ᶜφ = CreateAnnihilate.create) = true𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ decide (𝓕|>ᶜφ = CreateAnnihilate.create) = true]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ decide (𝓕|>ᶜφ = CreateAnnihilate.create) = true
  simp [hφ]All goals completed! 🐙

lemma createFilter_cons_annihilate {φ : 𝓕.CrAnFieldOp}
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnFieldOp) :
    createFilter (φ :: φs) = createFilter φs := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ createFilter (φ :: φs) = createFilter φs
  simp only [createFilter]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) (φ :: φs) =
  List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs
  rw [List.filter_cons_of_neg𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs =
  List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ ¬decide (𝓕|>ᶜφ = CreateAnnihilate.create) = true𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ ¬decide (𝓕|>ᶜφ = CreateAnnihilate.create) = true]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ ¬decide (𝓕|>ᶜφ = CreateAnnihilate.create) = true
  simp [hφ]All goals completed! 🐙

lemma createFilter_append (φs φs' : List 𝓕.CrAnFieldOp) :
    createFilter (φs ++ φs') = createFilter φs ++ createFilter φs' := by𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ createFilter (φs ++ φs') = createFilter φs ++ createFilter φs'
  rw [createFilter,𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) (φs ++ φs') = createFilter φs ++ createFilter φs'𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs ++
    List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs' =
  createFilter φs ++ createFilter φs' List.filter_append𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs ++
    List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs' =
  createFilter φs ++ createFilter φs'𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs ++
    List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs' =
  createFilter φs ++ createFilter φs']𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs ++
    List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.create)) φs' =
  createFilter φs ++ createFilter φs'
  rflAll goals completed! 🐙lemma createFilter_singleton_create (φ : 𝓕.CrAnFieldOp)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) :
    createFilter [φ] = [φ] := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.create⊢ createFilter [φ] = [φ]
  simp [createFilter, hφ]All goals completed! 🐙lemma createFilter_singleton_annihilate (φ : 𝓕.CrAnFieldOp)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) : createFilter [φ] = [] := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilate⊢ createFilter [φ] = []
  simp [createFilter, hφ]All goals completed! 🐙

Given a list of creation and annihilation states, the filtered list only containing the annihilation states. As a schematic example, for the list:

[φ1c, φ1a, φ2c, φ2a] this will return [φ1a, φ2a].

def annihilateFilter (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp :=
  List.filter (fun φ => 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) φs

              

lemma annihilateFilter_cons_create {φ : 𝓕.CrAnFieldOp}
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnFieldOp) :
    annihilateFilter (φ :: φs) = annihilateFilter φs := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ annihilateFilter (φ :: φs) = annihilateFilter φs
  simp only [annihilateFilter]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) (φ :: φs) =
  List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs
  rw [List.filter_cons_of_neg𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs =
  List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ ¬decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate) = true𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ ¬decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate) = true]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ ¬decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate) = true
  simp [hφ]All goals completed! 🐙

lemma annihilateFilter_cons_annihilate {φ : 𝓕.CrAnFieldOp}
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnFieldOp) :
    annihilateFilter (φ :: φs) = φ :: annihilateFilter φs := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ annihilateFilter (φ :: φs) = φ :: annihilateFilter φs
  simp only [annihilateFilter]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) (φ :: φs) =
  φ :: List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs
  rw [List.filter_cons_of_pos𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ φ :: List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs =
  φ :: List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate) = true𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate) = true]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate) = true
  simp [hφ]All goals completed! 🐙

lemma annihilateFilter_append (φs φs' : List 𝓕.CrAnFieldOp) :
    annihilateFilter (φs ++ φs') = annihilateFilter φs ++ annihilateFilter φs' := by𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ annihilateFilter (φs ++ φs') = annihilateFilter φs ++ annihilateFilter φs'
  rw [annihilateFilter,𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) (φs ++ φs') =
  annihilateFilter φs ++ annihilateFilter φs'𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs ++
    List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs' =
  annihilateFilter φs ++ annihilateFilter φs' List.filter_append𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs ++
    List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs' =
  annihilateFilter φs ++ annihilateFilter φs'𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs ++
    List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs' =
  annihilateFilter φs ++ annihilateFilter φs']𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs ++
    List.filter (fun φ => decide (𝓕|>ᶜφ = CreateAnnihilate.annihilate)) φs' =
  annihilateFilter φs ++ annihilateFilter φs'
  rflAll goals completed! 🐙lemma annihilateFilter_singleton_create (φ : 𝓕.CrAnFieldOp)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) :
    annihilateFilter [φ] = [] := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.create⊢ annihilateFilter [φ] = []
  simp [annihilateFilter, hφ]All goals completed! 🐙lemma annihilateFilter_singleton_annihilate (φ : 𝓕.CrAnFieldOp)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) :
    annihilateFilter [φ] = [φ] := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilate⊢ annihilateFilter [φ] = [φ]
  simp [annihilateFilter, hφ]All goals completed! 🐙