Physlib.QFT.PerturbationTheory.FieldStatistics.OfFinset

Imports

/-
Copyright (c) 2024 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.FieldStatistics.Basic
public import Mathlib.Data.Finset.Sort

Field statistics of a finite set.

@[expose] public section

The field statistic associated with a map f : Fin n → 𝓕 (usually .get of a list) and a finite set of elements of Fin n.

def ofFinset {n : ℕ} (q : 𝓕 → FieldStatistic) (f : Fin n → 𝓕) (a : Finset (Fin n)) :
    FieldStatistic :=
  ofList q ((a.sort (· ≤ ·)).map f)

              @[simp]
lemma ofFinset_empty (q : 𝓕 → FieldStatistic) (f : Fin n → 𝓕) :
    ofFinset q f ∅ = 1 := by𝓕:Typen:ℕq:𝓕 → FieldStatisticf:Fin n → 𝓕⊢ ofFinset q f ∅ = 1
  simp only [ofFinset, Finset.sort_empty, List.map_nil, ofList_empty]𝓕:Typen:ℕq:𝓕 → FieldStatisticf:Fin n → 𝓕⊢ bosonic = 1
  rflAll goals completed! 🐙lemma ofFinset_singleton {n : ℕ} (q : 𝓕 → FieldStatistic) (f : Fin n → 𝓕) (i : Fin n) :
    ofFinset q f {i} = q (f i) := by𝓕:Typen:ℕq:𝓕 → FieldStatisticf:Fin n → 𝓕i:Fin n⊢ ofFinset q f {i} = q (f i)
  simp [ofFinset]All goals completed! 🐙

lemma ofFinset_finset_map {n m : ℕ}
    (q : 𝓕 → FieldStatistic) (i : Fin m → Fin n) (hi : Function.Injective i)
    (f : Fin n → 𝓕) (a : Finset (Fin m)) :
    ofFinset q (f ∘ i) a = ofFinset q f (a.map ⟨i, hi⟩) := by𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ ofFinset q (f ∘ i) a = ofFinset q f (Finset.map { toFun := i, inj' := hi } a)
  simp only [ofFinset]𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ ofList q (List.map (f ∘ i) (a.sort fun x1 x2 => x1 ≤ x2)) =
  ofList q (List.map f ((Finset.map { toFun := i, inj' := hi } a).sort fun x1 x2 => x1 ≤ x2))
  apply FieldStatistic.ofList_perm𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ (List.map (f ∘ i) (a.sort fun x1 x2 => x1 ≤ x2)).Perm
  (List.map f ((Finset.map { toFun := i, inj' := hi } a).sort fun x1 x2 => x1 ≤ x2))
  rw [← List.map_map𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ (List.map f (List.map i (a.sort fun x1 x2 => x1 ≤ x2))).Perm
  (List.map f ((Finset.map { toFun := i, inj' := hi } a).sort fun x1 x2 => x1 ≤ x2))𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ (List.map f (List.map i (a.sort fun x1 x2 => x1 ≤ x2))).Perm
  (List.map f ((Finset.map { toFun := i, inj' := hi } a).sort fun x1 x2 => x1 ≤ x2))]𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ (List.map f (List.map i (a.sort fun x1 x2 => x1 ≤ x2))).Perm
  (List.map f ((Finset.map { toFun := i, inj' := hi } a).sort fun x1 x2 => x1 ≤ x2))
  refine List.Perm.map f ?_𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ (List.map i (a.sort fun x1 x2 => x1 ≤ x2)).Perm ((Finset.map { toFun := i, inj' := hi } a).sort fun x1 x2 => x1 ≤ x2)
  apply List.perm_of_nodup_nodup_toFinset_eqhl𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ (List.map i (a.sort fun x1 x2 => x1 ≤ x2)).Noduphl'𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ ((Finset.map { toFun := i, inj' := hi } a).sort fun x1 x2 => x1 ≤ x2).Noduph𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ (List.map i (a.sort fun x1 x2 => x1 ≤ x2)).toFinset =
  ((Finset.map { toFun := i, inj' := hi } a).sort fun x1 x2 => x1 ≤ x2).toFinset
  ·hl𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ (List.map i (a.sort fun x1 x2 => x1 ≤ x2)).Nodup refine (List.nodup_map_iff_inj_on ?_).mpr ?_hl.refine_1𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ (a.sort fun x1 x2 => x1 ≤ x2).Noduphl.refine_2𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ ∀ x ∈ a.sort fun x1 x2 => x1 ≤ x2, ∀ y ∈ a.sort fun x1 x2 => x1 ≤ x2, i x = i y → x = y
    exact a.sort_nodup (fun x1 x2 => x1 ≤ x2)hl.refine_2𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ ∀ x ∈ a.sort fun x1 x2 => x1 ≤ x2, ∀ y ∈ a.sort fun x1 x2 => x1 ≤ x2, i x = i y → x = y
    simp only [Finset.mem_sort]hl.refine_2𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ ∀ x ∈ a, ∀ y ∈ a, i x = i y → x = y
    intro x hx y hyhl.refine_2𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)x:Fin mhx:x ∈ ay:Fin mhy:y ∈ a⊢ i x = i y → x = y
    exact fun a => hi aAll goals completed! 🐙
  ·hl'𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ ((Finset.map { toFun := i, inj' := hi } a).sort fun x1 x2 => x1 ≤ x2).Nodup exact (Finset.map { toFun := i, inj' := hi } a).sort_nodup (fun x1 x2 => x1 ≤ x2)All goals completed! 🐙
  ·h𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a:Finset (Fin m)⊢ (List.map i (a.sort fun x1 x2 => x1 ≤ x2)).toFinset =
  ((Finset.map { toFun := i, inj' := hi } a).sort fun x1 x2 => x1 ≤ x2).toFinset ext ah𝓕:Typen:ℕm:ℕq:𝓕 → FieldStatistici:Fin m → Fin nhi:Function.Injective if:Fin n → 𝓕a✝:Finset (Fin m)a:Fin n⊢ a ∈ (List.map i (a✝.sort fun x1 x2 => x1 ≤ x2)).toFinset ↔
  a ∈ ((Finset.map { toFun := i, inj' := hi } a✝).sort fun x1 x2 => x1 ≤ x2).toFinset
    simpAll goals completed! 🐙

lemma ofFinset_insert (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a : Finset (Fin φs.length))
    (i : Fin φs.length) (h : i ∉ a) :
    ofFinset q φs.get (Insert.insert i a) = (q φs[i]) * ofFinset q φs.get a := by𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ a⊢ ofFinset q φs.get (insert i a) = q φs[i] * ofFinset q φs.get a
  simp only [ofFinset, Fin.getElem_fin]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ a⊢ ofList q (List.map φs.get ((insert i a).sort fun x1 x2 => x1 ≤ x2)) =
  q φs[↑i] * ofList q (List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2))
  rw [← ofList_cons_eq_mul𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ a⊢ ofList q (List.map φs.get ((insert i a).sort fun x1 x2 => x1 ≤ x2)) =
  ofList q (φs[↑i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2))𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ a⊢ ofList q (List.map φs.get ((insert i a).sort fun x1 x2 => x1 ≤ x2)) =
  ofList q (φs[↑i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2))]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ a⊢ ofList q (List.map φs.get ((insert i a).sort fun x1 x2 => x1 ≤ x2)) =
  ofList q (φs[↑i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2))
  have h1 : (φs[↑i] :: List.map φs.get (a.sort (fun x1 x2 => x1 ≤ x2)))
      = List.map φs.get (i :: a.sort (fun x1 x2 => x1 ≤ x2)) := by𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ a⊢ ofFinset q φs.get (insert i a) = q φs[i] * ofFinset q φs.get a𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ ofList q (List.map φs.get ((insert i a).sort fun x1 x2 => x1 ≤ x2)) =
  ofList q (φs[↑i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2))
      simp𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ ofList q (List.map φs.get ((insert i a).sort fun x1 x2 => x1 ≤ x2)) =
  ofList q (φs[↑i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2))𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ ofList q (List.map φs.get ((insert i a).sort fun x1 x2 => x1 ≤ x2)) =
  ofList q (φs[↑i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2))
  erw [h1𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ ofList q (List.map φs.get ((insert i a).sort fun x1 x2 => x1 ≤ x2)) =
  ofList q (List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2))]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ ofList q (List.map φs.get ((insert i a).sort fun x1 x2 => x1 ≤ x2)) =
  ofList q (List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2))
  apply ofList_perm𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ (List.map φs.get ((insert i a).sort fun x1 x2 => x1 ≤ x2)).Perm (List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2))
  refine List.Perm.map φs.get ?_𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ ((insert i a).sort fun x1 x2 => x1 ≤ x2).Perm (i :: a.sort fun x1 x2 => x1 ≤ x2)
  refine (List.perm_ext_iff_of_nodup ?_ ?_).mpr ?_refine_1𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ ((insert i a).sort fun x1 x2 => x1 ≤ x2).Noduprefine_2𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ (i :: a.sort fun x1 x2 => x1 ≤ x2).Noduprefine_3𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ ∀ (a_1 : Fin φs.length), (a_1 ∈ (insert i a).sort fun x1 x2 => x1 ≤ x2) ↔ a_1 ∈ i :: a.sort fun x1 x2 => x1 ≤ x2
  ·refine_1𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ ((insert i a).sort fun x1 x2 => x1 ≤ x2).Nodup exact (Insert.insert i a).sort_nodup (fun x1 x2 => x1 ≤ x2)All goals completed! 🐙
  ·refine_2𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ (i :: a.sort fun x1 x2 => x1 ≤ x2).Nodup simp only [List.nodup_cons, Finset.mem_sort, Finset.sort_nodup, and_true]refine_2𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)⊢ i ∉ a
    exact hAll goals completed! 🐙
  intro arefine_3𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a✝:Finset (Fin φs.length)i:Fin φs.lengthh:i ∉ ah1:φs[i] :: List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (i :: a.sort fun x1 x2 => x1 ≤ x2)a:Fin φs.length⊢ (a ∈ (insert i a✝).sort fun x1 x2 => x1 ≤ x2) ↔ a ∈ i :: a✝.sort fun x1 x2 => x1 ≤ x2
  simpAll goals completed! 🐙

lemma ofFinset_erase (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a : Finset (Fin φs.length))
    (i : Fin φs.length) (h : i ∈ a) :
    ofFinset q φs.get (a.erase i) = (q φs[i]) * ofFinset q φs.get a := by𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ a⊢ ofFinset q φs.get (a.erase i) = q φs[i] * ofFinset q φs.get a
  have ha : a = Insert.insert i (a.erase i) := by
    exact Eq.symm (Finset.insert_erase h)𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ ofFinset q φs.get (a.erase i) = q φs[i] * ofFinset q φs.get a𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ ofFinset q φs.get (a.erase i) = q φs[i] * ofFinset q φs.get a
  conv_rhs => rw [ha]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)| q φs[i] * ofFinset q φs.get (insert i (a.erase i))
  rw [ofFinset_insert𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ ofFinset q φs.get (a.erase i) = q φs[i] * (q φs[i] * ofFinset q φs.get (a.erase i))h𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ i ∉ a.erase i𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ ofFinset q φs.get (a.erase i) = q φs[i] * (q φs[i] * ofFinset q φs.get (a.erase i))h𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ i ∉ a.erase i]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ ofFinset q φs.get (a.erase i) = q φs[i] * (q φs[i] * ofFinset q φs.get (a.erase i))h𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ i ∉ a.erase i
  rw [← mul_assoc𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ ofFinset q φs.get (a.erase i) = q φs[i] * q φs[i] * ofFinset q φs.get (a.erase i)h𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ i ∉ a.erase i𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ ofFinset q φs.get (a.erase i) = q φs[i] * q φs[i] * ofFinset q φs.get (a.erase i)h𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ i ∉ a.erase i]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ ofFinset q φs.get (a.erase i) = q φs[i] * q φs[i] * ofFinset q φs.get (a.erase i)h𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ i ∉ a.erase i
  simp only [Fin.getElem_fin, mul_self, one_mul]h𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.lengthh:i ∈ aha:a = insert i (a.erase i)⊢ i ∉ a.erase i
  simpAll goals completed! 🐙

lemma ofFinset_eq_prod (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a : Finset (Fin φs.length)) :
    ofFinset q φs.get a = ∏ (i : Fin φs.length), if i ∈ a then (q φs[i]) else 1 := by𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ ofFinset q φs.get a = ∏ i, if i ∈ a then q φs[i] else 1
  rw [ofFinset𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ ofList q (List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2)) = ∏ i, if i ∈ a then q φs[i] else 1𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ ofList q (List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2)) = ∏ i, if i ∈ a then q φs[i] else 1]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ ofList q (List.map φs.get (a.sort fun x1 x2 => x1 ≤ x2)) = ∏ i, if i ∈ a then q φs[i] else 1
  rw [ofList_map_eq_finset_prod𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ (∏ i, if i ∈ a.sort fun x1 x2 => x1 ≤ x2 then q φs[i] else 1) = ∏ i, if i ∈ a then q φs[i] else 1hl𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ (a.sort fun x1 x2 => x1 ≤ x2).Nodup𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ (∏ i, if i ∈ a.sort fun x1 x2 => x1 ≤ x2 then q φs[i] else 1) = ∏ i, if i ∈ a then q φs[i] else 1hl𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ (a.sort fun x1 x2 => x1 ≤ x2).Nodup]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ (∏ i, if i ∈ a.sort fun x1 x2 => x1 ≤ x2 then q φs[i] else 1) = ∏ i, if i ∈ a then q φs[i] else 1hl𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ (a.sort fun x1 x2 => x1 ≤ x2).Nodup
  congre_f𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ (fun i => if i ∈ a.sort fun x1 x2 => x1 ≤ x2 then q φs[i] else 1) = fun i => if i ∈ a then q φs[i] else 1hl𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ (a.sort fun x1 x2 => x1 ≤ x2).Nodup
  funext ie_f𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)i:Fin φs.length⊢ (if i ∈ a.sort fun x1 x2 => x1 ≤ x2 then q φs[i] else 1) = if i ∈ a then q φs[i] else 1hl𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ (a.sort fun x1 x2 => x1 ≤ x2).Nodup
  simp only [Finset.mem_sort, Fin.getElem_fin]hl𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)⊢ (a.sort fun x1 x2 => x1 ≤ x2).Nodup
  exact a.sort_nodup (fun x1 x2 => x1 ≤ x2)All goals completed! 🐙

lemma ofFinset_union (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a b : Finset (Fin φs.length)) :
    ofFinset q φs.get a * ofFinset q φs.get b = ofFinset q φs.get ((a ∪ b) \ (a ∩ b)) := by𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)⊢ ofFinset q φs.get a * ofFinset q φs.get b = ofFinset q φs.get ((a ∪ b) \ (a ∩ b))
  rw [ofFinset_eq_prod,𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)⊢ (∏ i, if i ∈ a then q φs[i] else 1) * ofFinset q φs.get b = ofFinset q φs.get ((a ∪ b) \ (a ∩ b))𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)⊢ ((∏ i, if i ∈ a then q φs[i] else 1) * ∏ i, if i ∈ b then q φs[i] else 1) =
  ∏ i, if i ∈ (a ∪ b) \ (a ∩ b) then q φs[i] else 1 ofFinset_eq_prod,𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)⊢ ((∏ i, if i ∈ a then q φs[i] else 1) * ∏ i, if i ∈ b then q φs[i] else 1) = ofFinset q φs.get ((a ∪ b) \ (a ∩ b))𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)⊢ ((∏ i, if i ∈ a then q φs[i] else 1) * ∏ i, if i ∈ b then q φs[i] else 1) =
  ∏ i, if i ∈ (a ∪ b) \ (a ∩ b) then q φs[i] else 1 ofFinset_eq_prod𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)⊢ ((∏ i, if i ∈ a then q φs[i] else 1) * ∏ i, if i ∈ b then q φs[i] else 1) =
  ∏ i, if i ∈ (a ∪ b) \ (a ∩ b) then q φs[i] else 1𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)⊢ ((∏ i, if i ∈ a then q φs[i] else 1) * ∏ i, if i ∈ b then q φs[i] else 1) =
  ∏ i, if i ∈ (a ∪ b) \ (a ∩ b) then q φs[i] else 1]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)⊢ ((∏ i, if i ∈ a then q φs[i] else 1) * ∏ i, if i ∈ b then q φs[i] else 1) =
  ∏ i, if i ∈ (a ∪ b) \ (a ∩ b) then q φs[i] else 1
  rw [← Finset.prod_mul_distrib𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)⊢ (∏ x, (if x ∈ a then q φs[x] else 1) * if x ∈ b then q φs[x] else 1) = ∏ i, if i ∈ (a ∪ b) \ (a ∩ b) then q φs[i] else 1𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)⊢ (∏ x, (if x ∈ a then q φs[x] else 1) * if x ∈ b then q φs[x] else 1) = ∏ i, if i ∈ (a ∪ b) \ (a ∩ b) then q φs[i] else 1]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)⊢ (∏ x, (if x ∈ a then q φs[x] else 1) * if x ∈ b then q φs[x] else 1) = ∏ i, if i ∈ (a ∪ b) \ (a ∩ b) then q φs[i] else 1
  congre_f𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)⊢ (fun x => (if x ∈ a then q φs[x] else 1) * if x ∈ b then q φs[x] else 1) = fun i =>
  if i ∈ (a ∪ b) \ (a ∩ b) then q φs[i] else 1
  funext xe_f𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)x:Fin φs.length⊢ ((if x ∈ a then q φs[x] else 1) * if x ∈ b then q φs[x] else 1) = if x ∈ (a ∪ b) \ (a ∩ b) then q φs[x] else 1
  simp only [Fin.getElem_fin, mul_ite, ite_mul, mul_self, one_mul, mul_one,
    Finset.mem_sdiff, Finset.mem_union, Finset.mem_inter, not_and]e_f𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)x:Fin φs.length⊢ (if x ∈ b then if x ∈ a then 1 else q φs[↑x] else if x ∈ a then q φs[↑x] else 1) =
  if (x ∈ a ∨ x ∈ b) ∧ (x ∈ a → x ∉ b) then q φs[↑x] else 1
  splite_f.isTrue𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)x:Fin φs.lengthh✝:x ∈ b⊢ (if x ∈ a then 1 else q φs[↑x]) = if (x ∈ a ∨ x ∈ b) ∧ (x ∈ a → x ∉ b) then q φs[↑x] else 1e_f.isFalse𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)x:Fin φs.lengthh✝:x ∉ b⊢ (if x ∈ a then q φs[↑x] else 1) = if (x ∈ a ∨ x ∈ b) ∧ (x ∈ a → x ∉ b) then q φs[↑x] else 1
  ·e_f.isTrue𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)x:Fin φs.lengthh✝:x ∈ b⊢ (if x ∈ a then 1 else q φs[↑x]) = if (x ∈ a ∨ x ∈ b) ∧ (x ∈ a → x ∉ b) then q φs[↑x] else 1 rename_i he_f.isTrue𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)x:Fin φs.lengthh:x ∈ b⊢ (if x ∈ a then 1 else q φs[↑x]) = if (x ∈ a ∨ x ∈ b) ∧ (x ∈ a → x ∉ b) then q φs[↑x] else 1
    simp [h]All goals completed! 🐙
  ·e_f.isFalse𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)x:Fin φs.lengthh✝:x ∉ b⊢ (if x ∈ a then q φs[↑x] else 1) = if (x ∈ a ∨ x ∈ b) ∧ (x ∈ a → x ∉ b) then q φs[↑x] else 1 rename_i he_f.isFalse𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)x:Fin φs.lengthh:x ∉ b⊢ (if x ∈ a then q φs[↑x] else 1) = if (x ∈ a ∨ x ∈ b) ∧ (x ∈ a → x ∉ b) then q φs[↑x] else 1
    simp [h]All goals completed! 🐙

lemma ofFinset_union_disjoint (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a b : Finset (Fin φs.length))
    (h : Disjoint a b) :
    ofFinset q φs.get a * ofFinset q φs.get b = ofFinset q φs.get (a ∪ b) := by𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)h:Disjoint a b⊢ ofFinset q φs.get a * ofFinset q φs.get b = ofFinset q φs.get (a ∪ b)
  rw [ofFinset_union,𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)h:Disjoint a b⊢ ofFinset q φs.get ((a ∪ b) \ (a ∩ b)) = ofFinset q φs.get (a ∪ b)𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)h:Disjoint a b⊢ ofFinset q φs.get ((a ∪ b) \ ∅) = ofFinset q φs.get (a ∪ b) Finset.disjoint_iff_inter_eq_empty.mp h𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)h:Disjoint a b⊢ ofFinset q φs.get ((a ∪ b) \ ∅) = ofFinset q φs.get (a ∪ b)𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)h:Disjoint a b⊢ ofFinset q φs.get ((a ∪ b) \ ∅) = ofFinset q φs.get (a ∪ b)]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)b:Finset (Fin φs.length)h:Disjoint a b⊢ ofFinset q φs.get ((a ∪ b) \ ∅) = ofFinset q φs.get (a ∪ b)
  simpAll goals completed! 🐙

lemma ofFinset_filter_mul_neg (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a : Finset (Fin φs.length))
    (p : Fin φs.length → Prop) [DecidablePred p] :
    ofFinset q φs.get (Finset.filter p a) *
    ofFinset q φs.get (Finset.filter (fun i => ¬ p i) a) = ofFinset q φs.get a := by𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ ofFinset q φs.get (Finset.filter p a) * ofFinset q φs.get ({i ∈ a | ¬p i}) = ofFinset q φs.get a
  rw [ofFinset_union_disjoint𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ ofFinset q φs.get (Finset.filter p a ∪ {i ∈ a | ¬p i}) = ofFinset q φs.get ah𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ Disjoint (Finset.filter p a) ({i ∈ a | ¬p i})𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ ofFinset q φs.get (Finset.filter p a ∪ {i ∈ a | ¬p i}) = ofFinset q φs.get ah𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ Disjoint (Finset.filter p a) ({i ∈ a | ¬p i})]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ ofFinset q φs.get (Finset.filter p a ∪ {i ∈ a | ¬p i}) = ofFinset q φs.get ah𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ Disjoint (Finset.filter p a) ({i ∈ a | ¬p i})
  congre_a𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ Finset.filter p a ∪ {i ∈ a | ¬p i} = ah𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ Disjoint (Finset.filter p a) ({i ∈ a | ¬p i})
  exact Finset.filter_union_filter_not_eq p ah𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ Disjoint (Finset.filter p a) ({i ∈ a | ¬p i})
  exact Finset.disjoint_filter_filter_not a a pAll goals completed! 🐙

lemma ofFinset_filter (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a : Finset (Fin φs.length))
    (p : Fin φs.length → Prop) [DecidablePred p] :
    ofFinset q φs.get (Finset.filter p a) = ofFinset q φs.get (Finset.filter (fun i => ¬ p i) a) *
    ofFinset q φs.get a := by𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ ofFinset q φs.get (Finset.filter p a) = ofFinset q φs.get ({i ∈ a | ¬p i}) * ofFinset q φs.get a
  rw [← ofFinset_filter_mul_neg q φs a p𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ ofFinset q φs.get (Finset.filter p a) =
  ofFinset q φs.get ({i ∈ a | ¬p i}) * (ofFinset q φs.get (Finset.filter p a) * ofFinset q φs.get ({i ∈ a | ¬p i}))𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ ofFinset q φs.get (Finset.filter p a) =
  ofFinset q φs.get ({i ∈ a | ¬p i}) * (ofFinset q φs.get (Finset.filter p a) * ofFinset q φs.get ({i ∈ a | ¬p i}))]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ ofFinset q φs.get (Finset.filter p a) =
  ofFinset q φs.get ({i ∈ a | ¬p i}) * (ofFinset q φs.get (Finset.filter p a) * ofFinset q φs.get ({i ∈ a | ¬p i}))
  conv_rhs =>
    rhs𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p| ofFinset q φs.get (Finset.filter p a) * ofFinset q φs.get ({i ∈ a | ¬p i})
    rw [mul_comm]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p| ofFinset q φs.get ({i ∈ a | ¬p i}) * ofFinset q φs.get (Finset.filter p a)
  rw [← mul_assoc𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ ofFinset q φs.get (Finset.filter p a) =
  ofFinset q φs.get ({i ∈ a | ¬p i}) * ofFinset q φs.get ({i ∈ a | ¬p i}) * ofFinset q φs.get (Finset.filter p a)𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ ofFinset q φs.get (Finset.filter p a) =
  ofFinset q φs.get ({i ∈ a | ¬p i}) * ofFinset q φs.get ({i ∈ a | ¬p i}) * ofFinset q φs.get (Finset.filter p a)]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕a:Finset (Fin φs.length)p:Fin φs.length → Propinst✝:DecidablePred p⊢ ofFinset q φs.get (Finset.filter p a) =
  ofFinset q φs.get ({i ∈ a | ¬p i}) * ofFinset q φs.get ({i ∈ a | ¬p i}) * ofFinset q φs.get (Finset.filter p a)
  simpAll goals completed! 🐙