From a4058857e32cec5492821cf11696cdb25df28f4c Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Feb 2007 18:10:17 +0000
Subject: [PATCH] Second formulation of a constructive (positive) proof of
 Lebesgue's integration theorem, based on a proof by Weber.

---
 helm/software/matita/dama/DIMOSTRAZIONE | 76 +++++++++++++++++++++++++
 1 file changed, 76 insertions(+)

diff --git a/helm/software/matita/dama/DIMOSTRAZIONE b/helm/software/matita/dama/DIMOSTRAZIONE
index afdd13e53..197c3ff97 100644
--- a/helm/software/matita/dama/DIMOSTRAZIONE
+++ b/helm/software/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.
-- 
2.39.2