From 2a56316adcc4d32870d704fa86fda83fbde6df15 Mon Sep 17 00:00:00 2001
From: Enrico Zoli <??>
Date: Wed, 17 Jan 2007 17:59:59 +0000
Subject: [PATCH] This is the roadmap of the constructive proof of Lebesgue's
 dominated convergence theorem in the order theoretic setting. I.e. we speak
 of convergence (in terms of liminf and limsup) and not of norms/measures.

The formulation should be fully constructive:
 1. the exceeds relation is used in place of the derived negative notion
    <= for partial orders
 2. strong sup and infs are used in place of the weaker sup and infs
 3. the statement of Lebesgue's dominated converge theorem is just
    extensionality of the functional
      \lambda f. liminf f a_n
    with respect to the apartness relation # over real numbers and the
    exceeds/apartness relation over partial orders.

Interesting points to be noticed:
 a) one lemma used in the proof is Fatou. This lemma can be given in the
    usual negative formulation (i.e. on <=)
 b) another lemma used in the proof is that the liminf is less or equal to
    the limsup. This lemm can be given in the usual negative formulation
    (i.e. on <=). Moreover, we feel that if <= is not defined as
    ~< it is actually impossible to constructively prove it.
---
 helm/software/matita/dama/DIMOSTRAZIONE | 50 +++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 helm/software/matita/dama/DIMOSTRAZIONE

diff --git a/helm/software/matita/dama/DIMOSTRAZIONE b/helm/software/matita/dama/DIMOSTRAZIONE
new file mode 100644
index 000000000..afdd13e53
--- /dev/null
+++ b/helm/software/matita/dama/DIMOSTRAZIONE
@@ -0,0 +1,50 @@
+Prerequisiti:
+ 1. definizione di exceeds
+ 2. definizione di <= in termini di < (sui reali)
+ 2. definizione di sup forte (sui reali)
+
+========================================
+
+Lemma: liminf f a_n <= limsup f a_n
+Per definizione di <= dobbiamo dimostrare:
+  ~(limsup f a_n < liminf f a_n)
+Supponiamo limsup f a_n < liminf f a_n.
+Ovvero inf_n sup_{k>n} f a_k < sup_m inf_{h>m} f a_h
+? Quindi esiste un l tale che
+       inf_n sup_{k>n} f a_k + l/2 = sup_m inf_{h>m} f a_h - l/2
+? Per definizione di inf forte abbiamo
+       esiste un n' tale che
+         sup_{k>n'} f a_k < inf_n sup_{k>n} + l
+	                  = sup_m inf_{h>m} f a_h - l/2
+? Per definizione di sup forte abbiamo
+       esiste un n'' tale che
+         sup_{k>n'} f a_k < sup_m inf_{h>m} f a_h - l/2 < inf_{h>n''} f a_k
+  Sia N il max tra n' e n''. Allora:
+    sup_{k>N} f a_k < sup_{k>n'} f a_k < inf_{h>n''} f a_k < inf_{h>N} f a_k
+  Assurdo per lemma precedente.
+Qed.
+
+=======================================
+
+Lebesgue costruttivo:
+  a_n bounded da b ovvero \forall n, a_n < b
+  f strongly monotone ovvero f x < f y => y -<= x
+  liminf f a_n # limsup f a_n => liminf a_n < (o #) limsup a_n
+Dimostrazione:
+  per ipotesi
+   liminf f a_n # limsup f a_n
+  quindi
+   liminf f a_n > limsup f a_n \/ liminf f a_n < limsup f a_n.
+  per casi:
+    Caso 1:
+      Usiamo il lemma liminf f a_n <= limsup f a_n => assurdo
+    Caso 2:
+      Usiamo Fatou e Fatou rovesciato:
+        f (liminf a_n) <= liminf (f a_n)  (per fatou)
+	               <  limsup (f a_n)  (per ipotesi)
+		       <= f (limsup a_n)  (per fatou rovesciato)
+      Per monotonia forte della f otteniamo:
+          limsup a_n -<= liminf a_n
+      (Da cui:
+          liminf a_n # limsup a_n)
+Qed.
-- 
2.39.2