Live states (docs/roleflow.tex, sec:live)

The density proof runs on live states: the values of the positions in a finite set A, X_A = ∏_{v ∈ A} X_{σ v}. Here the sorts σ are read from one fixed context Γ (the context of all variables of a program), so a live state is a function on the positions of Γ that lie in A (LState Γ A), measured by the product lvol Γ A. Positions of A beyond Γ are ignored.

The reorders between live states and values of contexts are measure-preserving measurable equivalences, built from reorderEquiv:

• reading a live state at a duplicate-free list of positions that covers A (LState.pick) gives X_A ≅ X_as (LState.pickEquiv, measurePreserving_pick);
• if A is the disjoint union of B and the positions of such a list, keeping B and reading the list gives X_A ≅ X_B × X_as (LState.extract, measurePreserving_extract), with Mathlib's measurePreserving_piEquivPiSubtypeProd.

@[reducible, inline]

abbrev RoleFlow.Pos {S : Type} (Γ : List S) (A : Finset ℕ) : Type

The positions of Γ that lie in A.

Equations

• RoleFlow.Pos Γ A = { i : Fin Γ.length // ↑i ∈ A }

@[reducible, inline]

abbrev RoleFlow.LState {S : Type} [Sorts S] (Γ : List S) (A : Finset ℕ) : Type

A live state: a value for each position of Γ in A.

Equations

• RoleFlow.LState Γ A = ((i : RoleFlow.Pos Γ A) → RoleFlow.X (Γ.get ↑i))

noncomputable def RoleFlow.lvol {S : Type} [Sorts S] (Γ : List S) (A : Finset ℕ) : MeasureTheory.Measure (LState Γ A)

The product measure on live states.

Equations

• RoleFlow.lvol Γ A = MeasureTheory.Measure.pi fun (i : RoleFlow.Pos Γ A) => RoleFlow.μ (Γ.get ↑i)

instance RoleFlow.instSigmaFiniteLStateLvol {S : Type} [Sorts S] (Γ : List S) (A : Finset ℕ) : MeasureTheory.SigmaFinite (lvol Γ A)

def RoleFlow.LState.restrict {S : Type} [Sorts S] {Γ : List S} (A : Finset ℕ) (v : Val Γ) : LState Γ A

The live state of a value of Γ.

Equations

• RoleFlow.LState.restrict A v i = v ↑i

def RoleFlow.LState.sub {S : Type} [Sorts S] {Γ : List S} {A B : Finset ℕ} (h : A ⊆ B) (s : LState Γ B) : LState Γ A

Forget the positions outside A.

Equations

• RoleFlow.LState.sub h s i = s ⟨↑i, ⋯⟩

@[simp]

theorem RoleFlow.LState.sub_restrict {S : Type} [Sorts S] {Γ : List S} {A B : Finset ℕ} (h : A ⊆ B) (v : Val Γ) : sub h (restrict B v) = restrict A v

theorem RoleFlow.LState.measurable_sub {S : Type} [Sorts S] {Γ : List S} {A B : Finset ℕ} (h : A ⊆ B) : Measurable (sub h)

def RoleFlow.LState.get {S : Type} [Sorts S] {Γ : List S} {A : Finset ℕ} {a : S} (s : LState Γ A) (i : ℕ) (hi : i ∈ A) (h : Γ[i]? = some a) : X a

The value at the position i ∈ A.

Equations

• s.get i hi h = RoleFlow.tr RoleFlow.X ⋯ (s ⟨⟨i, ⋯⟩, hi⟩)

theorem RoleFlow.LState.measurable_get {S : Type} [Sorts S] {Γ : List S} {A : Finset ℕ} {a : S} {i : ℕ} (hi : i ∈ A) (h : Γ[i]? = some a) : Measurable fun (s : LState Γ A) => s.get i hi h

@[simp]

theorem RoleFlow.LState.get_restrict {S : Type} [Sorts S] {Γ : List S} {A : Finset ℕ} {a : S} (v : Val Γ) {i : ℕ} (hi : i ∈ A) (h : Γ[i]? = some a) : (restrict A v).get i hi h = v.get i h

Reading a live state at a list of positions

def RoleFlow.LState.pickPos {S : Type} {Γ : List S} {A : Finset ℕ} {xs : List ℕ} {as : List S} (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) (j : Fin as.length) : Pos Γ A

The position of the j-th entry of xs.

Equations

• RoleFlow.LState.pickPos hA h j = ⟨⟨xs[↑j], ⋯⟩, ⋯⟩

theorem RoleFlow.LState.pickPos_sort {S : Type} {Γ : List S} {A : Finset ℕ} {xs : List ℕ} {as : List S} (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) (j : Fin as.length) : Γ.get ↑(pickPos hA h j) = as.get j

def RoleFlow.LState.pick {S : Type} [Sorts S] {Γ : List S} {A : Finset ℕ} {as : List S} (s : LState Γ A) (xs : List ℕ) (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) : Val as

Read a live state at the positions xs.

Equations

• s.pick xs hA h j = RoleFlow.tr RoleFlow.X ⋯ (s (RoleFlow.LState.pickPos hA h j))

theorem RoleFlow.LState.measurable_pick {S : Type} [Sorts S] {Γ : List S} {A : Finset ℕ} {xs : List ℕ} {as : List S} (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) : Measurable fun (s : LState Γ A) => s.pick xs hA h

@[simp]

theorem RoleFlow.LState.pick_restrict {S : Type} [Sorts S] {Γ : List S} {A : Finset ℕ} {xs : List ℕ} {as : List S} (v : Val Γ) (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) : (restrict A v).pick xs hA h = v.pick xs h

theorem RoleFlow.LState.pickPos_bijective {S : Type} {Γ : List S} {A : Finset ℕ} {xs : List ℕ} {as : List S} (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) (hnd : xs.Nodup) (hcov : ∀ x ∈ A, x ∈ xs) : Function.Bijective (pickPos hA h)

If xs has no duplicates and covers A, the positions of xs are the positions of A.

noncomputable def RoleFlow.LState.pickEquiv {S : Type} [Sorts S] {Γ : List S} {A : Finset ℕ} {xs : List ℕ} {as : List S} (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) (hnd : xs.Nodup) (hcov : ∀ x ∈ A, x ∈ xs) : LState Γ A ≃ᵐ Val as

Reorder: reading a live state at a duplicate-free list that covers A, as a measurable equivalence X_A ≅ X_as.

Equations

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

theorem RoleFlow.LState.pickEquiv_apply {S : Type} [Sorts S] {Γ : List S} {A : Finset ℕ} {xs : List ℕ} {as : List S} (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) (hnd : xs.Nodup) (hcov : ∀ x ∈ A, x ∈ xs) (s : LState Γ A) : (pickEquiv hA h hnd hcov) s = s.pick xs hA h

theorem RoleFlow.LState.measurePreserving_pick {S : Type} [Sorts S] {Γ : List S} {A : Finset ℕ} {xs : List ℕ} {as : List S} (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) (hnd : xs.Nodup) (hcov : ∀ x ∈ A, x ∈ xs) : MeasureTheory.MeasurePreserving (⇑(pickEquiv hA h hnd hcov)) (lvol Γ A) (vol as)

Extracting positions from a live state

def RoleFlow.LState.posIn {S : Type} {Γ : List S} {A B : Finset ℕ} (hB : B ⊆ A) : Pos Γ B ≃ { i : Pos Γ A // ↑↑i ∈ B }

The positions of B ⊆ A among those of A.

Equations

• RoleFlow.LState.posIn hB = { toFun := fun (i : RoleFlow.Pos Γ B) => ⟨⟨↑i, ⋯⟩, ⋯⟩, invFun := fun (i : { i : RoleFlow.Pos Γ A // ↑↑i ∈ B }) => ⟨↑↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def RoleFlow.LState.posOut {S : Type} {Γ : List S} {A B : Finset ℕ} {xs : List ℕ} (hA : ∀ x ∈ xs, x ∈ A) (hBx : ∀ i ∈ A, i ∈ B ↔ i ∉ xs) : Pos Γ xs.toFinset ≃ { i : Pos Γ A // ↑↑i ∉ B }

The positions of xs among those of A: those not in B.

Equations

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

noncomputable def RoleFlow.LState.extract {S : Type} [Sorts S] {Γ : List S} {A B : Finset ℕ} {xs : List ℕ} {as : List S} (hB : B ⊆ A) (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) (hnd : xs.Nodup) (hBx : ∀ i ∈ A, i ∈ B ↔ i ∉ xs) : LState Γ A ≃ᵐ LState Γ B × Val as

Splitting: X_A ≅ X_B × X_as when A is the disjoint union of B and the positions xs; it keeps the positions of B and reads those of xs.

Equations

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

theorem RoleFlow.LState.extract_apply {S : Type} [Sorts S] {Γ : List S} {A B : Finset ℕ} {xs : List ℕ} {as : List S} (hB : B ⊆ A) (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) (hnd : xs.Nodup) (hBx : ∀ i ∈ A, i ∈ B ↔ i ∉ xs) (s : LState Γ A) : (extract hB hA h hnd hBx) s = (sub hB s, s.pick xs hA h)

theorem RoleFlow.LState.extract_restrict {S : Type} [Sorts S] {Γ : List S} {A B : Finset ℕ} {xs : List ℕ} {as : List S} (hB : B ⊆ A) (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) (hnd : xs.Nodup) (hBx : ∀ i ∈ A, i ∈ B ↔ i ∉ xs) (v : Val Γ) : (extract hB hA h hnd hBx) (restrict A v) = (restrict B v, v.pick xs h)

theorem RoleFlow.LState.measurePreserving_extract {S : Type} [Sorts S] {Γ : List S} {A B : Finset ℕ} {xs : List ℕ} {as : List S} (hB : B ⊆ A) (hA : ∀ x ∈ xs, x ∈ A) (h : Args Γ xs as) (hnd : xs.Nodup) (hBx : ∀ i ∈ A, i ∈ B ↔ i ∉ xs) : MeasureTheory.MeasurePreserving (⇑(extract hB hA h hnd hBx)) (lvol Γ A) ((lvol Γ B).prod (vol as))