]> matita.cs.unibo.it Git - helm.git/blob - matita/dama/DIMOSTRAZIONE
fix dependences for matita
[helm.git] / matita / dama / 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.