LEBESGUE INTEGRATION

-type defines Lebesgue integration over a measurable set with respect to a measure, yielding a real number. It generalizes Riemann integration and is pivotal in Schwartz’s theory of distributions.

In this system, leverages and to formalize integration, supporting both classical and constructive analysis.

Formation

(-Formation). Lebesgue integration is formed over a function , a measure , and a set , resulting in a real value.

type exp =
  | Lebesgue of exp * exp * exp  (* ∫ f dμ over S *)

Introduction

(-Introduction). An integral is introduced as , where is measurable, is a measure, and is in ’s -algebra.

let integral_term : exp =
  Lam ("f", Forall ("x", Real, Real),
    Lam ("a", Real,
      Lam ("b", Real,
        Lebesgue (Var "f",
          lebesgue_measure (Var "a") (Var "b"),
          interval_a_b (Var "a") (Var "b")))))

Elimination

(-Elimination). The integral yields a real number, usable in inequalities or further computations.

satisfies properties like

let infer env ctx (Lebesgue (f, mu, s)) = Real

Computation

(-Computation). For simple cases (e.g., intervals), reduces via the measure, verifiable by Z3.

let reduce env ctx = function
  | Lebesgue (f, Mu (_, _, Lam ("S", _, body)), s) when equal env ctx f One ->
      subst "S" s body
  | _ -> ...

Uniqueness

(-Uniqueness). The Lebesgue integral is unique for a given , , and , determined by the measure’s definition.

let equal env ctx (Lebesgue (f1, m1, s1)) (Lebesgue (f2, m2, s2)) =
  equal env ctx f1 f2 && equal env ctx m1 m2 && equal env ctx s1 s2

Theorems

(Monotonicity). If on , then , assuming is non-negative.

(Dominated Convergence). For a sequence converging to with and , .

let dom_conv (fn : exp) (f : exp) (g : exp) (mu : exp) (s : exp) =
  And (Limit (Seq (Lam ("n", Nat, Lebesgue (App (fn, Var "n"), mu, s))), Infinity,
             Lebesgue (f, mu, s), True),
       Lebesgue (g, mu, s))