Second formulation of a constructive (positive) proof of Lebesgue's

integration theorem, based on a proof by Weber.

diff --git a/matita/dama/DIMOSTRAZIONE b/matita/dama/DIMOSTRAZIONE
index afdd13e534fd36ac3b7006dfd7ad6fabebd2db92..197c3ff972b4d57de53f3a2abebf9471be3675ff 100644 (file)
--- a/matita/dama/DIMOSTRAZIONE
+++ b/matita/dama/DIMOSTRAZIONE
@@ -1,3 +1,5 @@
+############### Costruttivizzazione di Fremlin ######################
+
 Prerequisiti:
  1. definizione di exceeds
  2. definizione di <= in termini di < (sui reali)
@@ -48,3 +50,77 @@ Dimostrazione:
       (Da cui:
           liminf a_n # limsup a_n)
 Qed.
+
+############### Costruttivizzazione di Weber-Zoli ######################
+
+Prerequisiti:
+ 1. does_not_approach_zero x_n =
+     \exists delta. \exists sottosuccessione j.
+      \forall n. x_(j n) > delta
+ 2. does_not_have_sup = ??? (vedi prerequisito ????? sotto da soddisfare)
+ 3. sigma_and_esaustiva su [a,b] x_n =
+     d(a_n,x) does_not_approach_zero => a_n does_not_have_sup x
+ ????? inf x_i does_not_have_sup x => liminf x_i # x
+
+=======================================
+
+Sviluppi futuri:
+ Spezzare sigma_and_esaustiva in sigma + esaustiva o qualcosa del
+ genere. Probabilmente sigma diventa
+   d(a,a_1) ~<= \bigsum_{i=n}^\infty d(a_n,a_{n+1})  =>
+   a_n does_not_have_sup a
+ La prova del lemma 5 in versione positiva e' ancora da fare.
+ L'esaustivita' deve essere rimpiazzata da un concetto tipo located.
+
+=======================================
+
+Due carabinieri:
+ a_n <= x_n <= b_n
+ d(x_n,x) does_not_approach_zero =>
+  d(a_n,x) does_not_approach_zero \/
+  d(b_n,x) does_not_approach_zero
+Dimostrazione:
+ Per ipotesi esiste un \delta e una sottosuccessione y tale che
+   \delta <  d(y_n,x)
+          <= d(y_n,a_n) + d(a_n,x)
+          <= d(b_n,a_n) + d(a_n,x)
+          <= d(b_n,x) + 2d(a_n,x)
+ We conclude (?????? costruttivamente vero per > 0 e vero classicamente)
+  d(b_n,x) > \delta/4 \/ d(a_n,x) > \delta/4
+ and thus
+  d(a_n,x) does_not_approach_zero \/
+  d(b_n,x) does_not_approach_zero
+Qed.
+
+=======================================
+
+Lebsegue costruttivo:
+ x_n in [a,b], a_n <= x_n <= b_n per ogni n
+ d sigma_and_esaustiva su [a,b];
+ d(x_n,liminf x_n) does_not_approach_zero \/
+ d(x_n,limsup x_n) does_not_approach_zero =>
+ liminf x_n # limsup x_n   (possiamo concludere che eccede? forse no)
+Dimostrazione:
+ Fissiamo un x tale che d(x_n,x) does_not_approach_zero.
+ Per ipotesi d(x_n,x) does_not_approach_zero
+ Siano a_n := inf_{i>=n} x_i e b_n := sup_{i>=n} x_i.
+ Per i due carabinieri:
+  d(a_n,x) does_not_approach_zero \/ d(b_n,x) does_not_approach_zero
+ Per definizione di sigma_and_esaustiva su [a,b]
+  a_n does_not_have_sup x \/ b_n does_not_have_inf x
+ Quindi, per definizione di liminf e limsup e per ?????????
+  liminf x_n # x \/ limsup x_n # x
+ Facendo discharging di x concludiamo
+  \forall x t.c. d(x_n,x) does_not_approach zero,
+  liminf x_n # x \/ limsup x_n # x
+ Per ipotesi possiamo istanziare x con liminf x_n oppure con
+ limsup x_n.
+ Nel primo caso otteniamo
+  liminf x_n # liminf x_n \/ limsup x_n # liminf x_n
+ Poiche' la prima ipotesi e' falsa concludiamo
+  limsup x_n # liminf x_n
+ Nel secondo caso otteniamo
+  liminf x_n # limsup x_n \/ limsup x_n # limsup x_n \/ 
+ Poiche' la seconda ipotesi e' falsa concludiamo anche in questo caso
+  limsup x_n # liminf x_n
+Qed.