|
riesz_representation[a:real,b: {bb:real | a < bb}]: THEORY
%------------------------------------------------------------------------------
% The Riesz Representation Theorem
% [This is a fundamental theorem in functional analysis. It says that every
% bounded linear functional on the Banach space C[a,b] of continuous functions
% on [a,b] is given by integration (Riemann-Stieltjes) with respect to some
% integrator of bounded variation]
%------------------------------------------------------------------------------
BEGIN
IMPORTING riesz_interval_funs[a,b],rs_integral_cont[INTab], riesz_hahn_banach[a,b], bounded_variation[INTab], reals@sign
h: VAR [INTab -> real]
x: VAR INTab
M: VAR nnreal
r1,r2,r3: VAR INTab
% x :VAR INTab
LC : VAR C_Bounded_Linear_Operator
LB : VAR B_Bounded_Linear_Operator
g : VAR (bounded_variation?(a,b))
f : VAR Continuous_Function[a,b]
integral_norm_bounded: LEMMA integrable?(a,b,g,f) AND
abs(integral(a,b,g,f)) <= total_variation(a,b,g)(b)*fun_norm(f)
fun_to_op(g): C_Bounded_Linear_Operator = (LAMBDA (f):
integral(a,b,g,f))
fun_to_op_bound: LEMMA abs(fun_to_op(g)(f)) <= total_variation(a,b,g)(b)*fun_norm(f)
char_fun(r1,r2)(x): nnreal = IF r1<=x AND x<r2 AND r2<b THEN 1 ELSIF r1<=x AND x<=r2 AND r2=b THEN 1 ELSE 0 ENDIF
char_fun_minus: LEMMA r1<=r2 AND (r2<r3 OR (r2<=r3 AND r3<b)) IMPLIES char_fun(r1,r3)-char_fun(r1,r2) = char_fun(r2,r3)
% ----- Approximating a continuous f by a step function -------- %
step_approx(P:partition(a,b),xis:xis?(a,b,P))(fr:(bounded_on_int?[a,b])): (bounded_on_int?[a,b]) =
(LAMBDA (x:INTab): sigma[below(P`length-1)](0,P`length-2,LAMBDA (n:below(P`length-1)):
fr(xis`seq(n))*char_fun(P`seq(n),P`seq(n+1))(x)))
step_approx_def: LEMMA FORALL (eps:posreal): EXISTS (delta:posreal): FORALL (P:partition(a,b),xis:xis?(a,b,P)):
strictly_increasing?(P) AND width(a,b,P)<delta IMPLIES (FORALL (x:INTab): abs(f(x)-step_approx(P,xis)(f)(x)) < eps)
IMPORTING riesz_bounded_functionals[a,b,Continuous_Function[a,b]],riesz_bounded_functionals[a,b,Bounded_Function[a,b]]
riesz_representation: LEMMA EXISTS g:
op_norm[a,b,Continuous_Function[a,b]](LC) = total_variation(a,b,g)(b) AND
LC = fun_to_op(g)
END riesz_representation
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
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.
|
