|
riesz_interval_funs[a:real,b: {bb:real | a < bb}]: THEORY
%------------------------------------------------------------------------------
% Real valued functions on a closed interval
%------------------------------------------------------------------------------
BEGIN
IMPORTING real_metric_space,real_fun_on_compact_sets,
metric_space_real_fun
c: VAR real
M: VAR nnreal
Intab : set[real] = closed_intv(a,b)
INTab : TYPE = (closed_intv(a,b))
h,f,g: VAR [INTab -> real]
x :VAR INTab
IMPORTING metric_space_real_fun[INTab,real_dist]
bounded_on_int?(h): bool = EXISTS (M:nnreal): FORALL (x): abs(h(x))<=M
bounded_on_int_sum_closed: LEMMA bounded_on_int?(f) AND bounded_on_int?(h) IMPLIES bounded_on_int?(f+h)
bounded_on_int_const_closed: LEMMA bounded_on_int?(f) IMPLIES bounded_on_int?(c*f)
fun_norm(f: (bounded_on_int?)): {M:nnreal | (FORALL (x): abs(f(x))<=M) AND (FORALL (M1:real): M1 < M IMPLIES
EXISTS (x): abs(f(x)) > M1)}
fun_norm_dist(f,g:(bounded_on_int?)): {k:nnreal|k=0 IFF f=g} = fun_norm(f-g)
fun_norm_bound: LEMMA FORALL (f:(bounded_on_int?),x): abs(f(x)) <= fun_norm(f)
fun_norm_zero: LEMMA bounded_on_int?(f) IMPLIES (fun_norm(f) = 0 IFF f = (LAMBDA (y:INTab): 0))
fun_norm_scal: LEMMA FORALL (f:(bounded_on_int?),c): fun_norm(c*f) = abs(c)*fun_norm(f)
fun_norm_triangle: LEMMA FORALL (f,g:(bounded_on_int?)): fun_norm(f+g) <= fun_norm(f)+fun_norm(g)
bounded_funs_metric_space: LEMMA metric_space?[(bounded_on_int?),fun_norm_dist](bounded_on_int?)
int_compact: LEMMA compact?(Intab)
Bounded_Function : TYPE = (bounded_on_int?)
continuous_on_int?(h): bool = continuous?(h,Intab)
Continuous_Function: TYPE = (continuous_on_int?)
fc,gc : VAR Continuous_Function
fb,gb: VAR Bounded_Function
continuous_implies_bounded: LEMMA FORALL (h:Continuous_Function): bounded_on_int?(h)
continuous_function_bounded: JUDGEMENT Continuous_Function Subtype_of Bounded_Function
END riesz_interval_funs
[ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
]
|
