Field statistics of a finite set.

def FieldStatistic.ofFinset {𝓕 : Type} {n : ℕ} (q : 𝓕 → FieldStatistic) (f : Fin n → 𝓕) (a : Finset (Fin n)) : FieldStatistic

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

Equations

• FieldStatistic.ofFinset q f a = FieldStatistic.ofList q (List.map f (Finset.sort (fun (x1 x2 : Fin n) => x1 ≤ x2) a))

@[simp]

theorem FieldStatistic.ofFinset_empty {𝓕 : Type} {n : ℕ} (q : 𝓕 → FieldStatistic) (f : Fin n → 𝓕) : ofFinset q f ∅ = 1

theorem FieldStatistic.ofFinset_singleton {𝓕 : Type} {n : ℕ} (q : 𝓕 → FieldStatistic) (f : Fin n → 𝓕) (i : Fin n) : ofFinset q f {i} = q (f i)

theorem FieldStatistic.ofFinset_finset_map {𝓕 : Type} {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 (Finset.map { toFun := i, inj' := hi } a)

theorem FieldStatistic.ofFinset_insert {𝓕 : Type} (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a : Finset (Fin φs.length)) (i : Fin φs.length) (h : i ∉ a) : ofFinset q φs.get (insert i a) = q φs[i] * ofFinset q φs.get a

theorem FieldStatistic.ofFinset_erase {𝓕 : Type} (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

theorem FieldStatistic.ofFinset_eq_prod {𝓕 : Type} (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

theorem FieldStatistic.ofFinset_union {𝓕 : Type} (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))

theorem FieldStatistic.ofFinset_union_disjoint {𝓕 : Type} (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)

theorem FieldStatistic.ofFinset_filter_mul_neg {𝓕 : Type} (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 : Fin φs.length) => ¬p i) a) = ofFinset q φs.get a

theorem FieldStatistic.ofFinset_filter {𝓕 : Type} (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 : Fin φs.length) => ¬p i) a) * ofFinset q φs.get a