BOCHNER INTEGRATION

-type defines integration over a measurable set with respect to a measure, yielding a vector in a Banach space . It generalizes the Lebesgue integral to vector-valued functions and is crucial for functional analysis and PDEs.

In this system, leverages and to formalize vector integration, building on scalar Lebesgue integration for norm integrability.

Formation

(-Formation). Bochner integration is formed over a function , a measure , and a Banach space , resulting in a vector value in .

type exp =
  | Bochner of exp * exp * exp  (* ∫ f dμ in Vec_n *)

Introduction

(-Introduction). An integral is introduced as , where is Bochner measurable, is a measure, and is a Banach space of dimension .

let vector_integral_term : exp =
  Lam ("f", Forall ("x", Real, Vec (Var "n", Real, Var "scalar_mult", Var "vec_plus")),
    Lam ("mu", Measure (Real, Set (Set Real)),
      Bochner (Var "f", Var "mu", Vec (Var "n", Real, Var "scalar_mult", Var "vec_plus"))))

Elimination

(-Elimination). The integral yields a vector in , usable in vector operations or norms.

satisfies properties like

let infer env ctx (Bochner (f, mu, vec)) = vec

Computation

(-Computation). For simple cases (e.g., step functions), reduces via the measure to a vector sum.

let reduce env ctx = function
  | Bochner (f, Mu (_, _, Lam ("S", _, body)), vec) when is_simple f ->
      (* Compute ∑ μ(E_i) v_i in Vec_n *)
      vector_sum ctx f body
  | _ -> ...

Uniqueness

(-Uniqueness). The Bochner integral is unique for a given , , and , determined by the measure and space.

let equal env ctx (Bochner (f1, m1, v1)) (Bochner (f2, m2, v2)) =
  equal env ctx f1 f2 && equal env ctx m1 m2 && equal env ctx v1 v2

Theorems

(Linearity). For and scalars , .

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

let dom_conv_vec (fn : exp) (f : exp) (g : exp) (mu : exp) (vec : exp) =
  And (Limit (Seq (Lam ("n", Nat, Bochner (App (fn, Var "n"), mu, vec))), Infinity,
             Bochner (f, mu, vec), True),
       Lebesgue (Lam ("x", Real, App (Var "norm", App (g, Var "x"))), mu, Set Real))