The subfamilies of a listing, as a bag

A world of an occurrence family is a set of positions of its listing, and what a reading takes from it is three things: the product of the annotations it keeps, the sum of those it leaves out, and the sequence of occurrences it selects. subWorlds ann L is the bag of those triples, one per subset of positions, built by a recursion over the listing rather than over Finset (Fin L.length) (univ_map_eq_subWorlds).

Its point is what a recursion over the list makes easy: two listings that differ by a tie-block permutation – adjacent occurrences swapped where the swapped occurrences look alike – give the same bag once each selected occurrence is read through a map that cannot tell them apart (subWorlds_tiePerm). Several readings of one listing, which is what a joint reading of several aggregate values of one family is, are then blind to the permutation together, since all of them are read off the same selected sequence.

@[reducible, inline]

abbrev CommSemiringWithMonus.toCommSemiringSW {K : Type} [CommSemiringWithMonus K] : CommSemiring K

The commutative semiring underlying a commutative m-semiring, which the subfamilies are counted in. A definition rather than an instance, to be made local where it is used.

Equations

• CommSemiringWithMonus.toCommSemiringSW = { toSemiring := inferInstance, mul_comm := ⋯ }

def subWorlds {β K : Type} [CommSemiring K] (ann : β → K) : List β → Multiset (K × K × List β)

The subfamilies of a listing: per subset of its positions, the product of the annotations kept, the sum of those left out, and the occurrences selected, in order.

Equations

• One or more equations did not get rendered due to their size.
• subWorlds ann [] = {(1, 0, [])}

def SubWorldsAux.succEmb (n : ℕ) : Fin n ↪ Fin (n + 1)

Equations

• SubWorldsAux.succEmb n = { toFun := Fin.succ, inj' := ⋯ }

theorem univ_map_eq_subWorlds {β K : Type} [CommSemiring K] (ann : β → K) (L : List β) : Multiset.map (fun (W : Finset (Fin L.length)) => (∏ i ∈ W, ann (L.get i), ∑ i ∈ Wᶜ, ann (L.get i), Having.seqOf L W)) Finset.univ.val = subWorlds ann L

The bag of subfamilies is the enumeration of the subsets of positions.

theorem subWorlds_tiePerm {β K : Type} [CommSemiring K] {γ : Type} (ann : β → K) (rd : β → γ) {eqv : β → β → Prop} (hrd : ∀ {a b : β}, eqv a b → rd a = rd b) {L₁ L₂ : List β} (h : TiePerm eqv L₁ L₂) : Multiset.map (fun (w : K × K × List β) => (w.1, w.2.1, List.map rd w.2.2)) (subWorlds ann L₁) = Multiset.map (fun (w : K × K × List β) => (w.1, w.2.1, List.map rd w.2.2)) (subWorlds ann L₂)

A tie-block permutation leaves the subfamilies alone, read through a map rd of the selected occurrences that cannot tell two tied occurrences apart. Only the selected sequence needs rd: the two worlds that keep one of two swapped occurrences and leave out the other trade places, and their annotations go with them.

theorem subWorlds_map {β β' K K' : Type} [CommSemiring K] [CommSemiring K'] (f : K →+* K') (ann : β → K) (ann' : β' → K') (e : β → β') (hann : ∀ (b : β), ann' (e b) = f (ann b)) (L : List β) : subWorlds ann' (List.map e L) = Multiset.map (fun (w : K × K × List β) => (f w.1, f w.2.1, List.map e w.2.2)) (subWorlds ann L)

The subfamilies of a listing pushed through a map of annotations: the annotations of every world pushed through it.

An aggregate expression read off its selected sequence

def AggExpr.okSeq {K T : Type} (e : AggExpr T K) (s : List ((Fin e.arity → T) × K × (Fin e.arity → Bool) × (Fin e.arity → Bool))) : Prop

Whether a selected sequence of occurrences is a world: it holds an occurrence of the group of every grouped leaf.

Equations

• e.okSeq s = ∀ (j : Fin e.arity), e.scalar j = false → ∃ z ∈ s, z.2.2.1 j = true

def AggExpr.valSeq {K T : Type} (e : AggExpr T K) (s : List ((Fin e.arity → T) × K × (Fin e.arity → Bool) × (Fin e.arity → Bool))) : T

The value of the expression on a selected sequence of occurrences.

Equations

• One or more equations did not get rendered due to their size.

theorem AggExpr.isWorld_iff_okSeq {K T : Type} (e : AggExpr T K) (W : Finset (Fin e.occs.length)) : e.IsWorld W ↔ e.okSeq (Having.seqOf e.occs W)

A world is read off the occurrences it selects.

Home · Documentation · Publications · Contributors · Source · Cite