Quellcode-Bibliothek integral.pvs

%------------------------------------------------------------------------------
% Integrals
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Definition and basic properties of integrals for functions f: [T->real]
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

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

BEGIN

  IMPORTING measure_space[T,S],
            measure_theory[T,S,m],
            nn_integral[T,S,m]

  g,g1,g2,g3,g4: VAR nn_integrable
  x:             VAR T

  integrable?(f:[T->real]):bool = EXISTS (g,h:nn_integrable): f = g-h  % 4.4.7

  integrable: TYPE+ = (integrable?) CONTAINING (lambda x: 0)

  nn_integrable_is_integrable:
               JUDGEMENT nn_integrable SUBTYPE_OF integrable           % 4.4.10
  isf_is_integrable:
               JUDGEMENT isf           SUBTYPE_OF integrable           % 4.4.15
  integrable_is_measurable:
               JUDGEMENT integrable    SUBTYPE_OF measurable_function

  f,f1,f2: VAR integrable
  w:       VAR sequence[integrable]
  f0:      VAR [T->real]
  h:       VAR measurable_function
  epsilon: VAR posreal
  c:       VAR real
  nnc:     VAR nnreal
  E:       VAR measurable_set
  F:       VAR (mu_fin?)
  i:       VAR isf
  n:       VAR nat

  integrable_equiv: LEMMA g1 - g3 = g2 - g4 =>                    % 4.4.8
                          nn_integral(g1) - nn_integral(g3) =
                                 nn_integral(g2) - nn_integral(g4)

  integrable_add:  JUDGEMENT +(f1,f2)    HAS_TYPE integrable
  integrable_scal: JUDGEMENT *(c,f)      HAS_TYPE integrable
  integrable_opp:  JUDGEMENT -(f)        HAS_TYPE integrable
  integrable_diff: JUDGEMENT -(f1,f2)    HAS_TYPE integrable

  integrable_zero: LEMMA integrable?(lambda x: 0)

  integrals(f):set[real]
    = {c| EXISTS (g,h:nn_integrable): f = g-h AND
                                      c = nn_integral(g) - nn_integral(h)}

  nonempty_integrals:  LEMMA nonempty?[real](integrals(f))
  singleton_integrals: LEMMA singleton?[real](integrals(f))

  integral(f):real = choose[real](integrals(f))                        % 4.4.9

  nn_integrable_is_nn_integrable:
                          LEMMA (FORALL x: f(x) >= 0) => nn_integrable?(f)
  integral_nn:            LEMMA integral(g) = nn_integral(g)           % 4.4.10

  integral_zero:   LEMMA integral(lambda x: 0) = 0                     % 4.4.11
  integral_phi:    LEMMA integral(phi(F)) = mu(F)
  integral_add:    LEMMA integral(f1+f2)  = integral(f1) + integral(f2)
  integral_scal:   LEMMA integral(c*f)    = c*integral(f)
  integral_opp:    LEMMA integral(-f)     = -integral(f)
  integral_diff:   LEMMA integral(f1-f2 ) = integral(f1) - integral(f2)
  integral_nonneg: LEMMA (FORALL x: f(x) >= 0) => integral(f) >= 0

  integrable_abs:   JUDGEMENT abs(f)      HAS_TYPE integrable          % 4.4.12
  integrable_max:   JUDGEMENT max(f1,f2)  HAS_TYPE integrable          % 4.4.13
  integrable_min:   JUDGEMENT min(f1,f2)  HAS_TYPE integrable          % 4.4.13
  integrable_plus:  JUDGEMENT plus(f)     HAS_TYPE integrable          % 4.4.12
  integrable_minus: JUDGEMENT minus(f)    HAS_TYPE integrable          % 4.4.12

  integral_abs:       LEMMA abs(integral(f)) <= integral(abs(f))       % 4.4.12
  integrable_pm_def:  LEMMA integrable?(f0) <=>                        % 4.4.12
                            (integrable?(plus(f0)) AND integrable?(minus(f0)))
  integral_pm:        LEMMA integral(f) = integral(plus(f))-integral(minus(f))
  integrable_abs_def: LEMMA integrable?(abs(h)) <=> integrable?(h)     % 4.4.12

  integrable_nz_finite: LEMMA                                          % 4.4.14
                        measurable_set?({x | abs(f(x)) >= epsilon}) AND
                        mu_fin?({x | abs(f(x)) >= epsilon})

  isf_integral:   LEMMA integral(i) = isf_integral(i)                  % 4.4.15

  integral_ae_eq: LEMMA ae_eq?(f,h) =>                                 % 4.4.16
                        (integrable?(h) AND integral(f) = integral(h))

  integral_prod:  LEMMA ae_le?(abs(h),lambda x: nnc) =>                % 4.4.17
                        (integrable?(f*h) AND
                         integral(abs(f*h)) <= nnc * integral(abs(f)))

  indefinite_integrable:  LEMMA integrable?(phi(E)*f)                  % 4.4.18

  integral_ae_le:  LEMMA ae_le?(f1,f2) =>                              % 4.4.19
                         integral(f1) <= integral(f2)

  integral_ae_abs: LEMMA ae_le?(abs(h),abs(f)) =>                      % 4.4.20
                         (integrable?(h) AND
                          abs(integral(h)) <= integral(abs(f)))

  bounded_is_indefinite_integrable: LEMMA
      bounded?(phi(F)*h) =>
        (integrable?(phi(F)*h) AND
         abs(integral(phi(F)*h)) <= mu(F)*sup_norm(phi(F)*h))

  integral_abs_0:   LEMMA integral(abs(f)) = 0 => ae_0?(f)             % 4.4.21
  measurable_ae_0:  LEMMA ae_0?(h) =>
                          (integrable?(h) AND integral(h) = 0)
  integral_ae_ge_0: LEMMA ae_nonneg?(f) AND integral(f) = 0 => ae_0?(f)

  integrable_maximum:   JUDGEMENT maximum(w,n)  HAS_TYPE integrable
  integrable_minimum:   JUDGEMENT minimum(w,n)  HAS_TYPE integrable

  integrable_split: LEMMA FORALL (h:[T->real]):
    integrable?(h) <=>
           integrable?(phi(E)*h) AND integrable?(phi(complement(E))*h)

  integral_split: LEMMA
    integral(f) = integral(phi(E)*f) + integral(phi(complement(E))*f)

END integral