MEASURE TYPE

The type classifies measure spaces, pairing a base type with a -algebra to define the domain of measure functions. It provides a higher-level construct for typing measures () and enabling integration in Schwartz’s analysis. Measures are introduced via the constructor, ensuring well-defined measurable spaces.

This framework supports Lebesgue integration and custom measures, with evaluation tied to real arithmetic and measure axioms.

Compared to Lean’s measure theory library in , which defines measures as functions from a -algebra to the extended reals with axioms encoded as typeclass constraints, our system emphasizes a more explicit type-theoretic construction. Lean’s approach leverages its dependent type system to integrate measures seamlessly with its calculus library, prioritizing automation and proof reuse (e.g., for Lebesgue integrals). In contrast, our type and constructor offer a minimalist, MLTT-inspired design tailored for Schwartz’s analysis, trading some of Lean’s generality and tooling for clarity in specifying custom measures and their computational behavior.

Formation

(-Formation). The measure type is formed over a base type and a -algebra , classifying measure functions.

type exp =
  | Measure of exp * exp  (* Measure (A, Σ) *)

Introduction

(-Introduction). A measure is introduced by the constructor , where is a function satisfying measure axioms (non-negativity, countable additivity).

let measure_intro (a : exp) (sigma : exp) (f : exp) : exp =
  Mu (a, sigma, f)

For example, the Lebesgue measure is introduced as:

let lebesgue_measure =
  Mu (Real, Power (Set Real),
      Lam ("S", Set Real,
          If (RealIneq (Lte, a, b), RealOps (Minus, b, a), Zero)))

Elimination

(-Elimination). A measure is applied to a set , yielding a real number .

let apply_measure (mu : exp) (s : exp) : exp =
  App (mu, s)  (* μ S *)

Computation

(-Computation). Applying a measure reduces to substituting the set argument into the measure function:

let reduce env ctx = function
  | App (Mu (_, _, Lam (s, _, body)), arg) -> subst s arg body
  | _ -> ...

Uniqueness

(-Uniqueness). Two measure types and are equal if and . Two measures are equal if they agree on all sets in .

let equal_measure env ctx (Mu (a1, s1, f1)) (Mu (a2, s2, f2)) =
  equal env ctx a1 a2 && equal env ctx s1 s2 (* and functional equivalence *)

Theorems

(Measurable Space). defines a measurable space if is a -algebra over , supporting integration.

(Lebesgue Measure Typing). The Lebesgue measure over is typed as .

let lebesgue_type = Measure (Real, Power (Set Real))

(Non-Negativity). For any measure and set , .

(Countable Additivity). If is a countable collection of disjoint sets in , then:

let sigma_algebra = is_sigma_algebra (Power (Set Real))