matita/contribs/dama/dama/doc/DIMOSTRAZIONE

   1 ############### Costruttivizzazione di Fremlin ######################
   2
   3 Prerequisiti:
   4  1. definizione di exceeds
   5  2. definizione di <= in termini di < (sui reali)
   6  2. definizione di sup forte (sui reali)
   7
   8 ========================================
   9
  10 Lemma: liminf f a_n <= limsup f a_n
  11 Per definizione di <= dobbiamo dimostrare:
  12   ~(limsup f a_n < liminf f a_n)
  13 Supponiamo limsup f a_n < liminf f a_n.
  14 Ovvero inf_n sup_{k>n} f a_k < sup_m inf_{h>m} f a_h
  15 ? Quindi esiste un l tale che
  16        inf_n sup_{k>n} f a_k + l/2 = sup_m inf_{h>m} f a_h - l/2
  17 ? Per definizione di inf forte abbiamo
  18        esiste un n' tale che
  19          sup_{k>n'} f a_k < inf_n sup_{k>n} + l
  20                           = sup_m inf_{h>m} f a_h - l/2
  21 ? Per definizione di sup forte abbiamo
  22        esiste un n'' tale che
  23          sup_{k>n'} f a_k < sup_m inf_{h>m} f a_h - l/2 < inf_{h>n''} f a_k
  24   Sia N il max tra n' e n''. Allora:
  25     sup_{k>N} f a_k < sup_{k>n'} f a_k < inf_{h>n''} f a_k < inf_{h>N} f a_k
  26   Assurdo per lemma precedente.
  27 Qed.
  28
  29 =======================================
  30
  31 Lebesgue costruttivo:
  32   a_n bounded da b ovvero \forall n, a_n < b
  33   f strongly monotone ovvero f x < f y => y -<= x
  34   liminf f a_n # limsup f a_n => liminf a_n < (o #) limsup a_n
  35 Dimostrazione:
  36   per ipotesi
  37    liminf f a_n # limsup f a_n
  38   quindi
  39    liminf f a_n > limsup f a_n \/ liminf f a_n < limsup f a_n.
  40   per casi:
  41     Caso 1:
  42       Usiamo il lemma liminf f a_n <= limsup f a_n => assurdo
  43     Caso 2:
  44       Usiamo Fatou e Fatou rovesciato:
  45         f (liminf a_n) <= liminf (f a_n)  (per fatou)
  46                        <  limsup (f a_n)  (per ipotesi)
  47                        <= f (limsup a_n)  (per fatou rovesciato)
  48       Per monotonia forte della f otteniamo:
  49           limsup a_n -<= liminf a_n
  50       (Da cui:
  51           liminf a_n # limsup a_n)
  52 Qed.
  53
  54 ############### Costruttivizzazione di Weber-Zoli ######################
  55
  56 Prerequisiti:
  57  1. does_not_approach_zero x_n =
  58      \exists delta. \exists sottosuccessione j.
  59       \forall n. x_(j n) > delta
  60  2. does_not_have_sup = ??? (vedi prerequisito ????? sotto da soddisfare)
  61  3. sigma_and_esaustiva su [a,b] x_n =
  62      d(a_n,x) does_not_approach_zero => a_n does_not_have_sup x
  63  ????? inf x_i does_not_have_sup x => liminf x_i # x
  64
  65 =======================================
  66
  67 Sviluppi futuri:
  68  Spezzare sigma_and_esaustiva in sigma + esaustiva o qualcosa del
  69  genere. Probabilmente sigma diventa
  70    d(a,a_1) ~<= \bigsum_{i=n}^\infty d(a_n,a_{n+1})  =>
  71    a_n does_not_have_sup a
  72  La prova del lemma 5 in versione positiva e' ancora da fare.
  73  L'esaustivita' deve essere rimpiazzata da un concetto tipo located.
  74
  75 =======================================
  76
  77 Due carabinieri:
  78  a_n <= x_n <= b_n
  79  d(x_n,x) does_not_approach_zero =>
  80   d(a_n,x) does_not_approach_zero \/
  81   d(b_n,x) does_not_approach_zero
  82 Dimostrazione:
  83  Per ipotesi esiste un \delta e una sottosuccessione y tale che
  84    \delta <  d(y_n,x)
  85           <= d(y_n,a_n) + d(a_n,x)
  86           <= d(b_n,a_n) + d(a_n,x)
  87           <= d(b_n,x) + 2d(a_n,x)
  88  We conclude (?????? costruttivamente vero per > 0 e vero classicamente)
  89   d(b_n,x) > \delta/4 \/ d(a_n,x) > \delta/4
  90  and thus
  91   d(a_n,x) does_not_approach_zero \/
  92   d(b_n,x) does_not_approach_zero
  93 Qed.
  94
  95 =======================================
  96
  97 Lebsegue costruttivo:
  98  x_n in [a,b], a_n <= x_n <= b_n per ogni n
  99  d sigma_and_esaustiva su [a,b];
 100  d(x_n,liminf x_n) does_not_approach_zero \/
 101  d(x_n,limsup x_n) does_not_approach_zero =>
 102  liminf x_n # limsup x_n   (possiamo concludere che eccede? forse no)
 103 Dimostrazione:
 104  Fissiamo un x tale che d(x_n,x) does_not_approach_zero.
 105  Per ipotesi d(x_n,x) does_not_approach_zero
 106  Siano a_n := inf_{i>=n} x_i e b_n := sup_{i>=n} x_i.
 107  Per i due carabinieri:
 108   d(a_n,x) does_not_approach_zero \/ d(b_n,x) does_not_approach_zero
 109  Per definizione di sigma_and_esaustiva su [a,b]
 110   a_n does_not_have_sup x \/ b_n does_not_have_inf x
 111  Quindi, per definizione di liminf e limsup e per ?????????
 112   liminf x_n # x \/ limsup x_n # x
 113  Facendo discharging di x concludiamo
 114   \forall x t.c. d(x_n,x) does_not_approach zero,
 115   liminf x_n # x \/ limsup x_n # x
 116  Per ipotesi possiamo istanziare x con liminf x_n oppure con
 117  limsup x_n.
 118  Nel primo caso otteniamo
 119   liminf x_n # liminf x_n \/ limsup x_n # liminf x_n
 120  Poiche' la prima ipotesi e' falsa concludiamo
 121   limsup x_n # liminf x_n
 122  Nel secondo caso otteniamo
 123   liminf x_n # limsup x_n \/ limsup x_n # limsup x_n \/
 124  Poiche' la seconda ipotesi e' falsa concludiamo anche in questo caso
 125   limsup x_n # liminf x_n
 126 Qed.