Top File of PVS complex_integration Library

 
%------------------------------------------------------------------------------
% Top file for Functional Analysis
%
%     Author: David Lester, Manchester University
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
%     Version 1.0            12/3/10   Initial Version
%------------------------------------------------------------------------------

top: THEORY

BEGIN

  IMPORTING
    complex_topology,       % complex_topology
    complex_measurable,     % measurable functions [T->complex]
    complex_measure_theory, % ae properties and cal_N
    complex_integral,       % integrable functions [T->complex]
    p_integrable_def,       % cal_L^p and norm defs
    young,                  % Young's inequality
    holder_scaf,            % Holder's inequality
    minkowski_scaf,         % Minkowski's inequality
    p_integrable,           % cal_L^p and norm properties
    essentially_bounded,    % essential bounds
    essential_bound_complete_scaf,
                            % completeness of essential bounds
    cal_L_inf,              % L^\infty
    complex_finite_measures,% class structure for finite measures
    cal_L_complex,          % complex integral classes
    cal_L_real              % real integral classes

END top

The tag identifies links that are outside the NASA domain