2 1. definizione di exceeds
3 2. definizione di <= in termini di < (sui reali)
4 2. definizione di sup forte (sui reali)
6 ========================================
8 Lemma: liminf f a_n <= limsup f a_n
9 Per definizione di <= dobbiamo dimostrare:
10 ~(limsup f a_n < liminf f a_n)
11 Supponiamo limsup f a_n < liminf f a_n.
12 Ovvero inf_n sup_{k>n} f a_k < sup_m inf_{h>m} f a_h
13 ? Quindi esiste un l tale che
14 inf_n sup_{k>n} f a_k + l/2 = sup_m inf_{h>m} f a_h - l/2
15 ? Per definizione di inf forte abbiamo
17 sup_{k>n'} f a_k < inf_n sup_{k>n} + l
18 = sup_m inf_{h>m} f a_h - l/2
19 ? Per definizione di sup forte abbiamo
20 esiste un n'' tale che
21 sup_{k>n'} f a_k < sup_m inf_{h>m} f a_h - l/2 < inf_{h>n''} f a_k
22 Sia N il max tra n' e n''. Allora:
23 sup_{k>N} f a_k < sup_{k>n'} f a_k < inf_{h>n''} f a_k < inf_{h>N} f a_k
24 Assurdo per lemma precedente.
27 =======================================
30 a_n bounded da b ovvero \forall n, a_n < b
31 f strongly monotone ovvero f x < f y => y -<= x
32 liminf f a_n # limsup f a_n => liminf a_n < (o #) limsup a_n
35 liminf f a_n # limsup f a_n
37 liminf f a_n > limsup f a_n \/ liminf f a_n < limsup f a_n.
40 Usiamo il lemma liminf f a_n <= limsup f a_n => assurdo
42 Usiamo Fatou e Fatou rovesciato:
43 f (liminf a_n) <= liminf (f a_n) (per fatou)
44 < limsup (f a_n) (per ipotesi)
45 <= f (limsup a_n) (per fatou rovesciato)
46 Per monotonia forte della f otteniamo:
47 limsup a_n -<= liminf a_n
49 liminf a_n # limsup a_n)