Homotopy Type Theory measure > history (Rev #2)

Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In set theory

In measure theory, a measure on a $\sigma$-frame or more generally a $\sigma$-complete distributive lattice (L,,,,,,)(L, \leq, \bot, \vee, \top, \wedge, \Vee) is a valuation μ:L[0,]\mu:L \to [0, \infty] such that the elements are mutually disjoint and the probability valuation is denumerably/countably additive

sL .m.n.(mn)(s(m)s(n)=)\forall s\in L^\mathbb{N}. \forall m \in \mathbb{N}. \forall n \in \mathbb{N}. (m \neq n) \wedge (s(m) \wedge s(n) = \bot)
sL .μ( n:s(n))= n:μ(s(n))\forall s\in L^\mathbb{N}. \mu(\Vee_{n:\mathbb{N}} s(n)) = \sum_{n:\mathbb{N}} \mu(s(n))

In homotopy type theory

In measure theory, a measure on a $\sigma$-frame or more generally a $\sigma$-complete distributive lattice (L,,,,,,)(L, \leq, \bot, \vee, \top, \wedge, \Vee) is a valuation μ:L[0,]\mu:L \to [0, \infty] with

  • a family of dependent terms
    s:Lα(s):( m: n:(mn)×(s(m)s(n)=))×(μ( n:s(n))= n:μ(s(n)))s:\mathbb{N} \to L \vdash \alpha(s):\left(\prod_{m:\mathbb{N}} \prod_{n:\mathbb{N}} (m \neq n) \times (s(m) \wedge s(n) = \bot)\right) \times \left(\mu(\Vee_{n:\mathbb{N}} s(n)) = \sum_{n:\mathbb{N}} \mu(s(n)) \right)

    representing the mutually disjoint elements condition and the denumerably/countably additive condition.

See also

References

Revision on April 14, 2022 at 03:12:48 by Anonymous?. See the history of this page for a list of all contributions to it.