The flow instance (docs/roleflow.tex, sec:flow; module Flow)

A sort is a dimension n with a reference measure on Vec n: Lebesgue (vec n, data), the standard normal (gauss n, randomness) or the standard logistic (unit n, a point of (0, 1)ⁿ in its logit chart). The operations are those of SemiInv2's flow signature, flat: arguments and results are separate variables. Each operation has at most one semi-inverse, which solves its first argument (or, for split/concat, all of them). An inverse pair is one constructor with a flag inv, and the semi-inverse flips it:

operation	inv = false	inv = true	log-weight
add	x + q	x - q (sub)	0
scaleexp	x ⊙ e^s	x ⊙ e^{-s} (scalenexp)	±Σ s
triu (Glow's LU factors)	M x	M⁻¹ x	±triuLogdet U
oddpow k	x ^ (2k+1)	y ^ (1/(2k+1))	opowLogdet k x, -opowLogdet k (y ^ (1/(2k+1)))

The other pairs are perm ps/perm ps⁻¹ (a permutation given by its steps, Flow.PermS; its index map is read as an Equiv.Perm by permOf), split/concat (log-weight 0), and rebase r r'/rebase r' r, the identity from the sort (r, n) to (r', n) with log-weight log ρ_{r'} - log ρ_r (score, sample, sigmoid and logit against Lebesgue measure). The conditioners (mvmul, mul, relu, conv3x3, attend, …) have none.

The model flowModel is a ModelInv. Leaves are proved at one flag (by measure preservation, the Jacobian formula or a density) and derived at the other by leaf_dag, whose derived log-weight agrees with the one given here; rebase has one leaf for all pairs of measures. Every declared pair is mutual, so the right law of an operation is the left law of its semi-inverse.

Sorts

inductive RoleFlow.Flow.Ref : Type

The reference measures: Lebesgue, the standard normal, and the standard logistic.

• leb : Ref
• normal : Ref
• logistic : Ref

@[implicit_reducible]

instance RoleFlow.Flow.instDecidableEqRef : DecidableEq Ref

Equations

• RoleFlow.Flow.instDecidableEqRef x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RoleFlow.Flow.instReprRef.repr : Ref → ℕ → Std.Format

Equations

• RoleFlow.Flow.instReprRef.repr RoleFlow.Flow.Ref.leb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RoleFlow.Flow.Ref.leb")).group prec✝
• RoleFlow.Flow.instReprRef.repr RoleFlow.Flow.Ref.normal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RoleFlow.Flow.Ref.normal")).group prec✝
• RoleFlow.Flow.instReprRef.repr RoleFlow.Flow.Ref.logistic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RoleFlow.Flow.Ref.logistic")).group prec✝

@[implicit_reducible]

instance RoleFlow.Flow.instReprRef : Repr Ref

Equations

• RoleFlow.Flow.instReprRef = { reprPrec := RoleFlow.Flow.instReprRef.repr }

noncomputable def RoleFlow.Flow.Ref.μ : Ref → (n : ℕ) → MeasureTheory.Measure (Vec n)

The reference measure on Vec n.

Equations

• RoleFlow.Flow.Ref.leb.μ x✝ = MeasureTheory.volume
• RoleFlow.Flow.Ref.normal.μ x✝ = RoleFlow.Flow.stdNormal x✝
• RoleFlow.Flow.Ref.logistic.μ x✝ = RoleFlow.Flow.stdLogistic x✝

instance RoleFlow.Flow.instSigmaFiniteVecμ (r : Ref) (n : ℕ) : MeasureTheory.SigmaFinite (r.μ n)

noncomputable def RoleFlow.Flow.Ref.logpdf : Ref → (n : ℕ) → Vec n → ℝ

The log-density of the reference measure against Lebesgue measure.

Equations

• RoleFlow.Flow.Ref.leb.logpdf x✝ = fun (x : RoleFlow.Flow.Vec x✝) => 0
• RoleFlow.Flow.Ref.normal.logpdf x✝ = fun (x : RoleFlow.Flow.Vec x✝) => Real.log (RoleFlow.Flow.stdNormalPDF x✝ x)
• RoleFlow.Flow.Ref.logistic.logpdf x✝ = fun (x : RoleFlow.Flow.Vec x✝) => Real.log (RoleFlow.Flow.logisticPDF x✝ x)

structure RoleFlow.Flow.FS : Type

The sorts: a reference measure and a dimension.

• ref : Ref
• dim : ℕ

@[implicit_reducible]

instance RoleFlow.Flow.instDecidableEqFS : DecidableEq FS

Equations

• RoleFlow.Flow.instDecidableEqFS = RoleFlow.Flow.instDecidableEqFS.decEq

def RoleFlow.Flow.instDecidableEqFS.decEq (x✝ x✝¹ : FS) : Decidable (x✝ = x✝¹)

Equations

• RoleFlow.Flow.instDecidableEqFS.decEq { ref := a, dim := a_1 } { ref := b, dim := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def RoleFlow.Flow.instReprFS.repr : FS → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RoleFlow.Flow.instReprFS : Repr FS

Equations

• RoleFlow.Flow.instReprFS = { reprPrec := RoleFlow.Flow.instReprFS.repr }

@[reducible, inline]

abbrev RoleFlow.Flow.FS.vec (n : ℕ) : FS

Data.

Equations

• RoleFlow.Flow.FS.vec n = { ref := RoleFlow.Flow.Ref.leb, dim := n }

@[reducible, inline]

abbrev RoleFlow.Flow.FS.gauss (n : ℕ) : FS

Standard-normal randomness.

Equations

• RoleFlow.Flow.FS.gauss n = { ref := RoleFlow.Flow.Ref.normal, dim := n }

@[reducible, inline]

abbrev RoleFlow.Flow.FS.unit (n : ℕ) : FS

Points of the unit cube in their logit chart.

Equations

• RoleFlow.Flow.FS.unit n = { ref := RoleFlow.Flow.Ref.logistic, dim := n }

@[implicit_reducible]

noncomputable instance RoleFlow.Flow.instSortsFS : Sorts FS

Equations

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

Operations

inductive RoleFlow.Flow.FOp : List FS → List FS → Type

The flow operations, flat. The flag inv selects the second operation of an inverse pair.

• nil : FOp [] [FS.vec 0]

  The empty vector (the initial key-value cache).

• split (m n : ℕ) : FOp [FS.vec (m + n)] [FS.vec m, FS.vec n]
• concat (m n : ℕ) : FOp [FS.vec m, FS.vec n] [FS.vec (m + n)]
• perm (n : ℕ) (ps : PermS) (inv : Bool := false) : FOp [FS.vec n] [FS.vec n]

  The permutation ps (its inverse if inv): output entry i is input entry ps.idx i.

• rebase (r r' : Ref) (n : ℕ) : FOp [{ ref := r, dim := n }] [{ ref := r', dim := n }]

  The identity, from the reference measure r to r'.

• relu (n : ℕ) : FOp [FS.vec n] [FS.vec n]
• tanh (n : ℕ) : FOp [FS.vec n] [FS.vec n]
• layernorm (n : ℕ) : FOp [FS.vec n] [FS.vec n]
• gelu (n : ℕ) : FOp [FS.vec n] [FS.vec n]
• oddpow (n k : ℕ) (inv : Bool := false) : FOp [FS.vec n] [FS.vec n]

  x ↦ x ^ (2k + 1), elementwise; y ↦ y ^ (1/(2k + 1)) (the odd real root) if inv.

• rows2 (m n : ℕ) : FOp [FS.vec ((m + m) * n)] [FS.vec (m * n), FS.vec (m * n)]
• add (n : ℕ) (inv : Bool := false) : FOp [FS.vec n, FS.vec n] [FS.vec n]

  x + q; x - q if inv.

• scaleexp (n : ℕ) (inv : Bool := false) : FOp [FS.vec n, FS.vec n] [FS.vec n]

  x ⊙ exp s; x ⊙ exp (-s) if inv.

• triu (c n : ℕ) (inv : Bool := false) : FOp [FS.vec (c * n), FS.vec (c * c)] [FS.vec (c * n)]

  M x (triuMat), M⁻¹ x if inv: with channel permutations, Glow's LU 1 × 1 convolution.

• mvmul (m n : ℕ) : FOp [FS.vec (m * n), FS.vec n] [FS.vec m]

  W · x for a row-major m × n matrix W.

• mul (n : ℕ) : FOp [FS.vec n, FS.vec n] [FS.vec n]

  x ⊙ y, elementwise.

• addc (c h w : ℕ) : FOp [FS.vec (c * (h * w)), FS.vec c] [FS.vec (c * (h * w))]

  A per-channel bias.

• conv1x1 (cin cout h w : ℕ) : FOp [FS.vec (cout * cin), FS.vec (cin * (h * w))] [FS.vec (cout * (h * w))]

  Kernel first, then the image.

• conv3x3 (cin cout h w : ℕ) : FOp [FS.vec (cout * (cin * 9)), FS.vec (cin * (h * w))] [FS.vec (cout * (h * w))]
• attend (m h : ℕ) : FOp [FS.vec h, FS.vec (h * m), FS.vec (h * m)] [FS.vec h]

  A query against a key-value cache.

Names for the flipped flags and the changes of sort that the models use.

@[reducible, inline]

abbrev RoleFlow.Flow.FOp.sub (n : ℕ) : FOp [FS.vec n, FS.vec n] [FS.vec n]

Equations

• RoleFlow.Flow.FOp.sub n = RoleFlow.Flow.FOp.add n true

@[reducible, inline]

abbrev RoleFlow.Flow.FOp.scalenexp (n : ℕ) : FOp [FS.vec n, FS.vec n] [FS.vec n]

Equations

• RoleFlow.Flow.FOp.scalenexp n = RoleFlow.Flow.FOp.scaleexp n true

@[reducible, inline]

abbrev RoleFlow.Flow.FOp.score (n : ℕ) : FOp [FS.vec n] [FS.gauss n]

Equations

• RoleFlow.Flow.FOp.score n = RoleFlow.Flow.FOp.rebase RoleFlow.Flow.Ref.leb RoleFlow.Flow.Ref.normal n

@[reducible, inline]

abbrev RoleFlow.Flow.FOp.sample (n : ℕ) : FOp [FS.gauss n] [FS.vec n]

Equations

• RoleFlow.Flow.FOp.sample n = RoleFlow.Flow.FOp.rebase RoleFlow.Flow.Ref.normal RoleFlow.Flow.Ref.leb n

@[reducible, inline]

abbrev RoleFlow.Flow.FOp.logit (n : ℕ) : FOp [FS.unit n] [FS.vec n]

Equations

• RoleFlow.Flow.FOp.logit n = RoleFlow.Flow.FOp.rebase RoleFlow.Flow.Ref.logistic RoleFlow.Flow.Ref.leb n

@[reducible, inline]

abbrev RoleFlow.Flow.FOp.cube (n : ℕ) : FOp [FS.vec n] [FS.vec n]

Equations

• RoleFlow.Flow.FOp.cube n = RoleFlow.Flow.FOp.oddpow n 1

@[reducible, inline]

abbrev RoleFlow.Flow.FOp.cbrt (n : ℕ) : FOp [FS.vec n] [FS.vec n]

Equations

• RoleFlow.Flow.FOp.cbrt n = RoleFlow.Flow.FOp.oddpow n 1 true

@[reducible, inline]

abbrev RoleFlow.Flow.si1 {a b c : FS} (o : FOp [c, b] [a]) : SemiInv FOp [a, b] [c]

A semi-inverse solving the first argument from the result and the second argument.

Equations

• RoleFlow.Flow.si1 o = { cs := [a], ps := [b], split := ⋯, cs_ne := ⋯, op := o }

@[reducible, inline]

abbrev RoleFlow.Flow.si0 {a b : FS} (o : FOp [b] [a]) : SemiInv FOp [a] [b]

A semi-inverse of a one-argument operation.

Equations

• RoleFlow.Flow.si0 o = { cs := [a], ps := [], split := ⋯, cs_ne := ⋯, op := o }

def RoleFlow.Flow.FOp.inv {as bs : List FS} : FOp as bs → Option (SemiInv FOp as bs)

The declared semi-inverses.

Equations

• (RoleFlow.Flow.FOp.split m n).inv = some { cs := [RoleFlow.Flow.FS.vec (m + n)], ps := [], split := ⋯, cs_ne := ⋯, op := RoleFlow.Flow.FOp.concat m n }
• (RoleFlow.Flow.FOp.concat m n).inv = some { cs := [RoleFlow.Flow.FS.vec m, RoleFlow.Flow.FS.vec n], ps := [], split := ⋯, cs_ne := ⋯, op := RoleFlow.Flow.FOp.split m n }
• (RoleFlow.Flow.FOp.perm n ps inv).inv = some (RoleFlow.Flow.si0 (RoleFlow.Flow.FOp.perm n ps !inv))
• (RoleFlow.Flow.FOp.rebase r r' n).inv = some (RoleFlow.Flow.si0 (RoleFlow.Flow.FOp.rebase r' r n))
• (RoleFlow.Flow.FOp.oddpow n k inv).inv = some (RoleFlow.Flow.si0 (RoleFlow.Flow.FOp.oddpow n k !inv))
• (RoleFlow.Flow.FOp.add n inv).inv = some (RoleFlow.Flow.si1 (RoleFlow.Flow.FOp.add n !inv))
• (RoleFlow.Flow.FOp.scaleexp n inv).inv = some (RoleFlow.Flow.si1 (RoleFlow.Flow.FOp.scaleexp n !inv))
• (RoleFlow.Flow.FOp.triu c n inv).inv = some (RoleFlow.Flow.si1 (RoleFlow.Flow.FOp.triu c n !inv))
• x✝.inv = none

def RoleFlow.Flow.flowSig : Sig FS

The flow signature.

Equations

• RoleFlow.Flow.flowSig = { Op := RoleFlow.Flow.FOp, bs_ne := @RoleFlow.Flow.flowSig._proof_1, inv := fun {as bs : List RoleFlow.Flow.FS} => RoleFlow.Flow.FOp.inv }

Tuples

@[reducible, inline]

noncomputable abbrev RoleFlow.Flow.one {a : FS} (x : X a) : Val [a]

A one-element tuple.

Equations

• RoleFlow.Flow.one x = RoleFlow.Val.cons x RoleFlow.Val.nil

@[reducible, inline]

noncomputable abbrev RoleFlow.Flow.two {a b : FS} (x : X a) (y : X b) : Val [a, b]

A two-element tuple.

Equations

• RoleFlow.Flow.two x y = RoleFlow.Val.cons x (RoleFlow.Flow.one y)

@[reducible, inline]

noncomputable abbrev RoleFlow.Flow.a₀ {a : FS} {Γ : List FS} (v : Val (a :: Γ)) : X a

The arguments of a tuple.

Equations

• RoleFlow.Flow.a₀ v = v.head

@[reducible, inline]

noncomputable abbrev RoleFlow.Flow.a₁ {a b : FS} {Γ : List FS} (v : Val (a :: b :: Γ)) : X b

Equations

• RoleFlow.Flow.a₁ v = v.tail.head

@[reducible, inline]

noncomputable abbrev RoleFlow.Flow.a₂ {a b c : FS} {Γ : List FS} (v : Val (a :: b :: c :: Γ)) : X c

Equations

• RoleFlow.Flow.a₂ v = v.tail.tail.head

The model

def RoleFlow.Flow.negIf : Bool → ℝ → ℝ

t, or -t if inv.

Equations

• RoleFlow.Flow.negIf false x✝ = x✝
• RoleFlow.Flow.negIf true x✝ = -x✝

theorem RoleFlow.Flow.negIf_not (inv : Bool) (t : ℝ) : negIf (!inv) t = -negIf inv t

noncomputable def RoleFlow.Flow.permS (n : ℕ) (ps : PermS) : Equiv.Perm (Fin n)

The permutation of Fin n whose index map is ps.idx (taken mod n), if that map is injective; otherwise the identity. A PermS.valid permutation is one, but nothing here needs it: every operation is interpreted, and Print.certify refuses invalid ones.

Equations

• RoleFlow.Flow.permS n ps = if h : Function.Injective fun (i : Fin n) => ⟨ps.idx ↑i % n, ⋯⟩ then Equiv.ofBijective (fun (i : Fin n) => ⟨ps.idx ↑i % n, ⋯⟩) ⋯ else Equiv.refl (Fin n)

noncomputable def RoleFlow.Flow.permOf (n : ℕ) (ps : PermS) (inv : Bool) : Equiv.Perm (Fin n)

perm n ps inv as a permutation of the entries.

Equations

• RoleFlow.Flow.permOf n ps inv = if inv = true then Equiv.symm (RoleFlow.Flow.permS n ps) else RoleFlow.Flow.permS n ps

theorem RoleFlow.Flow.permOf_not (n : ℕ) (ps : PermS) (inv : Bool) : (permOf n ps !inv) = Equiv.symm (permOf n ps inv)

noncomputable def RoleFlow.Flow.semOp {as bs : List FS} : FOp as bs → Val as → Val bs

The interpretation of the operations.

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.Flow.semOp RoleFlow.Flow.FOp.nil = fun (x : RoleFlow.Val []) => RoleFlow.Flow.one Fin.elim0
• RoleFlow.Flow.semOp (RoleFlow.Flow.FOp.concat m n) = fun (v : RoleFlow.Val [RoleFlow.Flow.FS.vec m, RoleFlow.Flow.FS.vec n]) => RoleFlow.Flow.one (RoleFlow.Flow.vjoin v.head v.tail.head)
• RoleFlow.Flow.semOp (RoleFlow.Flow.FOp.rebase r r' n) = fun (v : RoleFlow.Val [{ ref := r, dim := n }]) => RoleFlow.Flow.one v.head
• RoleFlow.Flow.semOp (RoleFlow.Flow.FOp.relu n) = fun (v : RoleFlow.Val [RoleFlow.Flow.FS.vec n]) => RoleFlow.Flow.one (RoleFlow.Flow.fvrelu v.head)
• RoleFlow.Flow.semOp (RoleFlow.Flow.FOp.tanh n) = fun (v : RoleFlow.Val [RoleFlow.Flow.FS.vec n]) => RoleFlow.Flow.one (RoleFlow.Flow.fvtanh v.head)
• RoleFlow.Flow.semOp (RoleFlow.Flow.FOp.layernorm n) = fun (v : RoleFlow.Val [RoleFlow.Flow.FS.vec n]) => RoleFlow.Flow.one (RoleFlow.Flow.flayernorm v.head)
• RoleFlow.Flow.semOp (RoleFlow.Flow.FOp.gelu n) = fun (v : RoleFlow.Val [RoleFlow.Flow.FS.vec n]) => RoleFlow.Flow.one (RoleFlow.Flow.fgelu v.head)

noncomputable def RoleFlow.Flow.ℓOp {as bs : List FS} : FOp as bs → Val as → ℝ

The log-weights, on the whole argument tuple; 0 for the structural bijections and for the conditioners.

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.Flow.ℓOp (RoleFlow.Flow.FOp.rebase r r' n) = fun (v : RoleFlow.Val [{ ref := r, dim := n }]) => r'.logpdf n v.head - r.logpdf n v.head
• RoleFlow.Flow.ℓOp x✝ = fun (x : RoleFlow.Val x✝²) => 0

Measurability

theorem RoleFlow.Flow.measurable_a₀ {a : FS} {Γ : List FS} : Measurable fun (v : Val (a :: Γ)) => a₀ v

theorem RoleFlow.Flow.measurable_a₁ {a b : FS} {Γ : List FS} : Measurable fun (v : Val (a :: b :: Γ)) => a₁ v

theorem RoleFlow.Flow.measurable_a₂ {a b c : FS} {Γ : List FS} : Measurable fun (v : Val (a :: b :: c :: Γ)) => a₂ v

theorem RoleFlow.Flow.measurable_one {a : FS} : Measurable fun (x : X a) => one x

theorem RoleFlow.Flow.measurable_one' {a b : FS} {Γ : List FS} {f : X a → X b} (hf : Measurable f) : Measurable fun (v : Val (a :: Γ)) => one (f (a₀ v))

theorem RoleFlow.Flow.measurable_two' {a b c : FS} {Γ : List FS} {f : X a → X b × X c} (hf : Measurable f) : Measurable fun (v : Val (a :: Γ)) => two (f (a₀ v)).1 (f (a₀ v)).2

theorem RoleFlow.Flow.measurable_one₂ {a b c : FS} {Γ : List FS} {f : X a → X b → X c} (hf : Measurable fun (p : X a × X b) => f p.1 p.2) : Measurable fun (v : Val (a :: b :: Γ)) => one (f (a₀ v) (a₁ v))

theorem RoleFlow.Flow.measurable_one₃ {a b c d : FS} {Γ : List FS} {f : X a → X b → X c → X d} (hf : Measurable fun (p : X a × X b × X c) => f p.1 p.2.1 p.2.2) : Measurable fun (v : Val (a :: b :: c :: Γ)) => one (f (a₀ v) (a₁ v) (a₂ v))

theorem RoleFlow.Flow.measurable_negIf (inv : Bool) : Measurable (negIf inv)

theorem RoleFlow.Flow.measurable_logpdf (r : Ref) (n : ℕ) : Measurable (r.logpdf n)

theorem RoleFlow.Flow.measurable_semOp {as bs : List FS} (o : FOp as bs) : Measurable (semOp o)

theorem RoleFlow.Flow.measurable_ℓOp {as bs : List FS} (o : FOp as bs) : Measurable (ℓOp o)

Laws

theorem RoleFlow.Flow.eq_one {a : FS} (v : Val [a]) : one v.head = v

@[reducible, inline]

abbrev RoleFlow.Flow.LeftLaw {as bs : List FS} (o : FOp as bs) (si : SemiInv FOp as bs) : Prop

The left law of o with the semi-inverse si.

Equations

• RoleFlow.Flow.LeftLaw o si = ∀ (c : RoleFlow.Val si.cs) (p : RoleFlow.Val si.ps), RoleFlow.Flow.semOp si.op ((RoleFlow.Flow.semOp o (si.glue c p)).append p) = c

theorem RoleFlow.Flow.left0 {a b : FS} {o : FOp [a] [b]} {o' : FOp [b] [a]} (F : X a → X b) (G : X b → X a) (hF : ∀ (v : Val [a]), semOp o v = one (F v.head)) (hG : ∀ (v : Val [b]), semOp o' v = one (G v.head)) (h : ∀ (x : X a), G (F x) = x) : LeftLaw o (si0 o')

The left law of a one-argument operation.

theorem RoleFlow.Flow.left1 {a b c : FS} {o : FOp [a, b] [c]} {o' : FOp [c, b] [a]} (F : X a → X b → X c) (G : X c → X b → X a) (hF : ∀ (v : Val [a, b]), semOp o v = one (F v.head v.tail.head)) (hG : ∀ (v : Val [c, b]), semOp o' v = one (G v.head v.tail.head)) (h : ∀ (x : X a) (q : X b), G (F x q) q = x) : LeftLaw o (si1 o')

The left law of an operation that consumes its first argument.

theorem RoleFlow.Flow.left_split (m n : ℕ) (c : Val [FS.vec (m + n)]) (p : Val []) : semOp (FOp.concat m n) ((semOp (FOp.split m n) (Val.cast ⋯ (c.append p))).append p) = c

theorem RoleFlow.Flow.left_concat (m n : ℕ) (c : Val [FS.vec m, FS.vec n]) (p : Val []) : semOp (FOp.split m n) ((semOp (FOp.concat m n) (Val.cast ⋯ (c.append p))).append p) = c

theorem RoleFlow.Flow.left_perm (n : ℕ) (ps : PermS) (inv : Bool) : LeftLaw (FOp.perm n ps inv) (si0 (FOp.perm n ps !inv))

theorem RoleFlow.Flow.left_rebase (r r' : Ref) (n : ℕ) : LeftLaw (FOp.rebase r r' n) (si0 (FOp.rebase r' r n))

theorem RoleFlow.Flow.left_oddpow (n k : ℕ) (inv : Bool) : LeftLaw (FOp.oddpow n k inv) (si0 (FOp.oddpow n k !inv))

theorem RoleFlow.Flow.left_add (n : ℕ) (inv : Bool) : LeftLaw (FOp.add n inv) (si1 (FOp.add n !inv))

theorem RoleFlow.Flow.left_scaleexp (n : ℕ) (inv : Bool) : LeftLaw (FOp.scaleexp n inv) (si1 (FOp.scaleexp n !inv))

theorem RoleFlow.Flow.left_triu (c n : ℕ) (inv : Bool) : LeftLaw (FOp.triu c n inv) (si1 (FOp.triu c n !inv))

Leaves

theorem RoleFlow.Flow.cov_one {a b : FS} {f : X a → X b} {J : X a → ENNReal} (hf : Measurable f) (hJ : Measurable J) (h : Cov (μ a) (μ b) f J) : Cov (vol [a]) (vol [b]) (fun (x : Val [a]) => one (f x.head)) fun (x : Val [a]) => J x.head

Change of variables on one value, carried to one-element contexts.

theorem RoleFlow.Flow.cov_toRef (r : Ref) (n : ℕ) : Cov MeasureTheory.volume (r.μ n) (fun (x : Vec n) => x) fun (x : Vec n) => expw (r.logpdf n x)

From Lebesgue measure to a reference measure by the identity.

theorem RoleFlow.Flow.leaf_rebase (r r' : Ref) (n : ℕ) (p : Val []) : Cov (vol [{ ref := r, dim := n }]) (vol [{ ref := r', dim := n }]) (fun (c : Val [{ ref := r, dim := n }]) => semOp (FOp.rebase r r' n) (Val.cast ⋯ (c.append p))) fun (c : Val [{ ref := r, dim := n }]) => expw (ℓOp (FOp.rebase r r' n) (Val.cast ⋯ (c.append p)))

rebase: from r to Lebesgue measure by Cov.inv, then to r'.

theorem RoleFlow.Flow.leaf_add (n : ℕ) (p : Val [FS.vec n]) : Cov (vol [FS.vec n]) (vol [FS.vec n]) (fun (c : Val [FS.vec n]) => semOp (FOp.add n) (Val.cast ⋯ (c.append p))) fun (c : Val [FS.vec n]) => expw (ℓOp (FOp.add n) (Val.cast ⋯ (c.append p)))

theorem RoleFlow.Flow.leaf_scaleexp (n : ℕ) (p : Val [FS.vec n]) : Cov (vol [FS.vec n]) (vol [FS.vec n]) (fun (c : Val [FS.vec n]) => semOp (FOp.scaleexp n) (Val.cast ⋯ (c.append p))) fun (c : Val [FS.vec n]) => expw (ℓOp (FOp.scaleexp n) (Val.cast ⋯ (c.append p)))

theorem RoleFlow.Flow.leaf_triu (c n : ℕ) (p : Val [FS.vec (c * c)]) : Cov (vol [FS.vec (c * n)]) (vol [FS.vec (c * n)]) (fun (x : Val [FS.vec (c * n)]) => semOp (FOp.triu c n) (Val.cast ⋯ (x.append p))) fun (x : Val [FS.vec (c * n)]) => expw (ℓOp (FOp.triu c n) (Val.cast ⋯ (x.append p)))

theorem RoleFlow.Flow.leaf_perm (n : ℕ) (ps : PermS) (inv : Bool) (p : Val []) : Cov (vol [FS.vec n]) (vol [FS.vec n]) (fun (c : Val [FS.vec n]) => semOp (FOp.perm n ps inv) (Val.cast ⋯ (c.append p))) fun (c : Val [FS.vec n]) => expw (ℓOp (FOp.perm n ps inv) (Val.cast ⋯ (c.append p)))

theorem RoleFlow.Flow.leaf_oddpow (n k : ℕ) (p : Val []) : Cov (vol [FS.vec n]) (vol [FS.vec n]) (fun (c : Val [FS.vec n]) => semOp (FOp.oddpow n k) (Val.cast ⋯ (c.append p))) fun (c : Val [FS.vec n]) => expw (ℓOp (FOp.oddpow n k) (Val.cast ⋯ (c.append p)))

theorem RoleFlow.Flow.leaf_split (m n : ℕ) (p : Val []) : Cov (vol [FS.vec (m + n)]) (vol [FS.vec m, FS.vec n]) (fun (c : Val [FS.vec (m + n)]) => semOp (FOp.split m n) (Val.cast ⋯ (c.append p))) fun (c : Val [FS.vec (m + n)]) => expw (ℓOp (FOp.split m n) (Val.cast ⋯ (c.append p)))

Derived leaves

theorem RoleFlow.Flow.leaf_of_dag {as bs : List FS} {o : FOp as bs} {si : SemiInv FOp as bs} (left : LeftLaw o si) (leaf : ∀ (p : Val si.ps), Cov (vol si.cs) (vol bs) (fun (c : Val si.cs) => semOp o (Val.cast ⋯ (c.append p))) fun (c : Val si.cs) => expw (ℓOp o (Val.cast ⋯ (c.append p)))) {L : Val (bs ++ si.ps) → ℝ} (hL : ∀ (w : Val (bs ++ si.ps)), dagWeight (semOp si.op) (ℓOp o) ⋯ w = L w) (p : Val si.ps) : Cov (vol bs) (vol si.cs) (fun (b : Val bs) => semOp si.op (b.append p)) fun (b : Val bs) => expw (L (b.append p))

The leaf of a semi-inverse, derived by leaf_dag from the leaf and the left law of the operation it inverts; the derived log-weight is checked against ℓOp.

Right laws

theorem RoleFlow.Flow.flow_right {as bs : List FS} (o : FOp as bs) (si : SemiInv FOp as bs) (h : o.inv = some si) (b : Val bs) (p : Val si.ps) : semOp o (si.glue (semOp si.op (b.append p)) p) = b

The right law: every declared pair is mutual, so the right law of an operation is the left law of its semi-inverse, at the flipped flag.

noncomputable def RoleFlow.Flow.flowModel : ModelInv flowSig

The model of the flow signature.

Equations

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