Quelle integral.pvs Sprache: 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

quality95%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.