helm/software/matita/dama/DIMOSTRAZIONE

   1 Prerequisiti:
   2  1. definizione di exceeds
   3  2. definizione di <= in termini di < (sui reali)
   4  2. definizione di sup forte (sui reali)
   5
   6 ========================================
   7
   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
  16        esiste un n' tale che
  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.
  25 Qed.
  26
  27 =======================================
  28
  29 Lebesgue costruttivo:
  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
  33 Dimostrazione:
  34   per ipotesi
  35    liminf f a_n # limsup f a_n
  36   quindi
  37    liminf f a_n > limsup f a_n \/ liminf f a_n < limsup f a_n.
  38   per casi:
  39     Caso 1:
  40       Usiamo il lemma liminf f a_n <= limsup f a_n => assurdo
  41     Caso 2:
  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
  48       (Da cui:
  49           liminf a_n # limsup a_n)
  50 Qed.