%------------------------------------------------------------------------------
% Indefinite Integrals
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Properties of \int_E f i.e. integrals of f over measurable subsets E
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

indefinite_integral[T:TYPE,         (IMPORTING subset_algebra_def[T])
                    S:sigma_algebra,(IMPORTING measure_def[T,S])
                    m:measure_type]: THEORY

BEGIN

  IMPORTING measure_props[T,S,m],
            integral[T,S,m],
            integral_convergence[T,S,m]

  f,f1,f2: VAR integrable
  g:       VAR [T->real]
  h:       VAR measurable_function[T,S]
  DX:      VAR disjoint_indexed_measurable
  E,E1,E2: VAR measurable_set
  F:       VAR (mu_fin?)
  N:       VAR null_set
  c:       VAR real
  x:       VAR T
  n:       VAR nat

  integrable?(E)(g):bool = integrable?(phi(E)*g)

  integral(E:measurable_set,f:(integrable?(E))):real = integral(phi(E)*f)
                                                                       % 4.4.22

  indefinite_emptyset: LEMMA integral(emptyset,g) = 0
  indefinite_fullset:  LEMMA integral(fullset,f)  = integral(f)

  indefinite_eq_0: LEMMA FORALL (E:measurable_set,f:(integrable?(E))): % 4.4.23
                         ae_in?(LAMBDA x: f(x) > 0)(E) AND
                         integral(phi(E)*f) = 0 =>
                         (mu_fin?(E) AND mu(E) = 0)

  indefinite_eq:   LEMMA (FORALL E: integral(E,f1) = integral(E,f2)) =>
                         ae_eq?(f1,f2)                                 % 4.4.24

  indefinite_phi:  LEMMA integral(E,phi(F)) = mu(intersection(E,F))
                                                                       % 4.7.2
  indefinite_add:  LEMMA FORALL (E:measurable_set,f1,f2:(integrable?(E))):
                         integral(E,f1+f2) = integral(E,f1) + integral(E,f2)
  indefinite_scal: LEMMA FORALL (E:measurable_set,f:(integrable?(E))):
                         integral(E,(c*f)) = c*integral(E,f)
  indefinite_opp:  LEMMA FORALL (E:measurable_set,f:(integrable?(E))):
                         integral(E,-f)    = -integral(E,f)
  indefinite_diff: LEMMA FORALL (E:measurable_set,f1,f2:(integrable?(E))):
                         integral(E,f1-f2) = integral(E,f1) - integral(E,f2)

  indefinite_ae_eq:LEMMA
                 ae_eq?(f1,f2) <=>
                 (FORALL E: integral(E,f1)=integral(E,f2))
  indefinite_0_le: LEMMA
                 ae_nonneg?(f) <=> (FORALL E: 0 <= integral(E,f))
  indefinite_le:   LEMMA
                 ae_le?(f1,f2) <=> (FORALL E: integral(E,f1) <= integral(E,f2))
  indefinite_pm:   LEMMA FORALL (E:measurable_set,f:(integrable?(E))):
                 integral(E,f) = integral(E,plus(f)) - integral(E,minus(f))

  indefinite_union: LEMMA FORALL (E1,E2:measurable_set,
                                  f:(integrable?(union(E1,E2)))):
    disjoint?(E1,E2) =>
    integral(union(E1,E2),f) = integral(E1,f) + integral(E2,f)

  indefinite_subset: LEMMA FORALL (E1,E2:measurable_set,f:(integrable?(E2))):
                           subset?(E1,E2) AND ae_nonneg?(f) =>
                           integral(E1,f) <= integral(E2,f)

  indefinite_null: LEMMA integral(N,h) = 0

  indefinite_countably_additive: LEMMA                                  % 4.7.3
    convergence?(series(lambda n: integral(DX(n),f)), integral(IUnion(DX),f))

END indefinite_integral