Commit 74a0b452 by Dennis Müller

### cleaned up

parent 3c5019fd
 namespace http://mathhub.info/MitM/smglom/buggy ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import ar http://mathhub.info/MitM/smglom/arithmetics ❚ theory buggy : base:?Logic = include ts:?AllSets ❙ include ar:?RealArithmetics ❙ possibleBug : ℝ ⟶ ℝ ⟶ ℝ ❘ = [x , y] subtraction x y ❙ possibleBug2 : ℝ ⟶ ℝ ⟶ ℝ ❘ = [x , y] x - y ❙ ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/DescriptionOperators ❚ import base http://mathhub.info/MitM/Foundation ❚ import sub http://gl.mathhub.info/MMT/LFX/Subtyping ❚ theory HilbertEpsilon : base:?Logic = Eps : {A : type} (A ⟶ bool) ⟶ A ❘# ε 2❙ epsIntro : {A : type , P : A ⟶ bool} ⊦ (∃[x : A] P x) ⟶ ⊦ P (ε P) ❙ // epsIntro2 : {A : type , P : A ⟶ bool, Q : A ⟶ bool} ⊦ (∃ [x : A ] P x) ⟶ ⊦ (∀ [x : A] P x ⟶ Q x) ⟶ ε Q ❙ epsIntro3 : {A : type , P : A ⟶ bool, Q : A ⟶ bool} ⊦ (∃[x : A] P x) ⟶ ({x : A} ⊦ P x ⟶ ⊦ Q x) ⟶ ⊦ Q (ε P) ❙ ❚ theory PeonoIota : base:?Logic = include sub:?LFSubtyped❙ include base:?Math ❙ bla : type ❘= ⟨ ℕ | [x] ⊦ x ≐ 0⟩ ❙ blu = PredOf bla ❙ ❚
 namespace http://mathhub.info/MitM/smglom/Functions ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import base http://mathhub.info/MitM/Foundation ❚ theory Functions : base:?Logic = structure FunctionRelations ts:?Relations ❙ ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/HilbertChoice ❚ import base http://mathhub.info/MitM/Foundation ❚ theory HilbertChoice : base:?Logic = Eps : {A : type} (bool ⟶ A) ⟶ A ❘# ε 2❙ ❚ \ No newline at end of file
 ... ... @@ -86,8 +86,9 @@ theory RealArithmetics : base:?Logic = theory ExtendedReals : base:?Logic = include ?RealArithmetics ❙ extended_reals : type ❘ # ℝ∞ ❙ reals_are_extended : ℝ <* ℝ∞ ❙ infty : ℝ∞ ❘ # ∞ prec 1 ❙ // extended_reals : type ❘ # ℝ∞ ❙ // reals_are_extended : ℝ <* ℝ∞ ❙ infty : ℝ ❘ # ∞ prec 1 ❙ // leq : ℝ∞ ⟶ ℝ∞ ⟶ bool ❘ # 1 ≤ 2 prec 101 ❙ // TODO neginfty : ℝ∞ ❘ = - ∞ ❘ # -∞ ❙ ❚
 namespace http://mathhub.info/MitM/smglom/FinSequences ❚ namespace http://mathhub.info/MitM/smglom ❚ import base http://mathhub.info/MitM/Foundation ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ import seq http://cds.omdoc.org/urtheories❚ import sig http://gl.mathhub.info/MMT/LFX/Sigma ❚ theory FinSequences : base:?Logic = include arith:?NaturalArithmetics ❙ below : ℕ ⟶ type ❙ toBelow : {n : ℕ} below (succ n) ❘# toB 1❙ succBelow : {n : ℕ} below n ⟶ below (succ n) ❘# succB 2❙ toBelow : {n : ℕ} below (Succ n) ❘# toB 1❙ succBelow : {n : ℕ} below n ⟶ below (Succ n) ❘# succB 2❙ belowIsSubtypeOfNat : {n : ℕ} (below n) <* ℕ ❙ belowToNat : {n : ℕ} below (succ n) ⟶ ℕ ❘# btn 1 2❙ belowToNat : {n : ℕ} below (Succ n) ⟶ ℕ ❘# btn 1 2❙ belowToNatBaseCase : {m : ℕ} ⊦ belowToNat m (toBelow m) ≐ m❙ belowToNatRecCase : {m : ℕ, b : below (succ m)} ⊦ belowToNat (succ m) (succBelow (succ m) b) ≐ belowToNat m b ❙ belowToNatRecCase : {m : ℕ, b : below (Succ m)} ⊦ belowToNat (Succ m) (succBelow (Succ m) b) ≐ belowToNat m b ❙ belowToNatExample : ⊦ btn 3 (toB 3) ≐ 3❙ belowToNatExample2 : ⊦ btn 4 (succB (toB 3)) ≐ 3 ❙ belwoToNatExample2_2 : ⊦ belowToNat (succ 3) (succBelow (succ 3) (toBelow 3)) ≐ 3❙ belowToNatExample : ⊦ btn 3 (toB 3) ≐ 3❙ belowToNatExample2 : ⊦ btn 4 (succB (toB 3)) ≐ 3 ❙ belwoToNatExample2_2 : ⊦ belowToNat (Succ 3) (succBelow (Succ 3) (toBelow 3)) ≐ 3❙ // belowToNat2 : {n : ℕ} below (Succ n) ⟶ ℕ ❘= [n, b] n ❘# btn2 %I1 ❙ // belowToNat3 : {n : ℕ, m : ℕ} below n ⟶ ⊦ m < n ⟶ ℕ ❘= [n , m , b, p ] m ❘# btn3 %I1 ❙ ... ...
 namespace http://mathhub.info/MitM/smglom/measures ❚ namespace http://mathhub.info/MitM/smglom/calculus ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import seq http://cds.omdoc.org/urtheories ❚ import supr http://mathhub.info/MitM/smglom/supremum ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ import ms http://mathhub.info/MitM/smglom/measures ❚ theory LebesgueIntegral : base:?Logic = include ?Measure ❙ include ms:?Measure ❙ include ts:?Functions ❙ include ts:?SetCollection ❙ include ?SimpleFunctions ❙ include ts:?SetSum ❙ include supr:?SupremumReal ❙ include ?LebesgueMeasurable ❙ include arith:?RealArithmetics ❙ include ts:?SupremumReal ❙ include ms:?LebesgueMeasurable ❙ // include arith:?RealArithmetics ❙ simpleLebesgueIntegral : {m : measureSpace , s : nonnegativeSimpleFunction m } ℝ ❘ = [m , s] setSum ((im (πl s) (fullset (m.universe))) : set ℝ) (theorem_nonnegativeSimpleFunctionHasFiniteValues m s) (([x] x ⋅ (m.measure.measure) (elem (m.sigma_algebra.coll) (preim (πl s) (single x)))) : ℝ ⟶ ℝ) ❙ (theorem_nonnegativeSimpleFunctionHasFiniteValues m s) (([x] x ⋅ (m.rmeasure.measure) (elem (m.sigma_algebra.coll) (preim (πl s) (single x)))) : ℝ ⟶ ℝ) ❙ upperFunction : {a : type} (a ⟶ ℝ) ⟶ a ⟶ ℝ ❘ = [a , f , x ] max (f x) 0❙ ... ... @@ -76,13 +74,4 @@ theory LebesgueIntegral : base:?Logic = ❙ ❚ theory lebesgueIntegralAlt : base:?Logic = include ?LebesgueIntegral ❙ computationalLebesgueIntegral ❙ ❚ theory LebesgueIntervalIntegral : base:?Logic = ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/measures ❚ namespace http://mathhub.info/MitM/smglom/calculus ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import lfx http://gl.mathhub.info/MMT/LFX/Sigma ❚ import exr http://mathhub.info/MitM/smglom/arithmetics ❚ import seq http://cds.omdoc.org/urtheories ❚ import desc http://mathhub.info/MitM/smglom/DescriptionOperators❚ import top http://mathhub.info/MitM/smglom/topology ❚ import ms http://mathhub.info/MitM/smglom/measures ❚ theory SimpleFunctions : base:?Logic = include ?Measure ❙ include ms:?Measure ❙ include ts:?Functions ❙ include ?PowerSigmaAlgebra ❙ include ?BorelMeasurable ❙ include ms:?PowerSigmaAlgebra ❙ include ms:?BorelMeasurable ❙ // include top:?RealTopology ❙ ... ...
 namespace http://mathhub.info/MitM/smglom/measures ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import ar http://mathhub.info/MitM/smglom/arithmetics ❚ theory NullSets : base:?Logic = include ?Measure ❙ isNullSet : {m : measureSpace} set (m.universe) ⟶ bool ❘// slow! = [m , s] (s ∈ m.sigma_algebra.coll) ∧ (((m.measure.measure) (elem (m.sigma_algebra.coll) s)) ≐ 0)❙ allNullSets : {m : measureSpace} collection (m.universe) ❘// slow!= [m] ⟪ (m.sigma_algebra.coll) | ([s] (((m.measure.measure) (elem (m.sigma_algebra.coll) s)) ≐ 0))⟫ ❙ ❚ theory AlmostEverywhere : base:?Logic = include ?NullSets ❙ almostEverywhere : {m : measureSpace} ((m.universe) ⟶ bool) ⟶ bool ❘ = [m,P] ∃ [n] n ∈ (allNullSets m) ∧ (∀[x] x ∈ (fullset (m.universe) \ n) ⇒ P x)❘# AE 1 2❙ ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/measures ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import seq http://cds.omdoc.org/urtheories ❚ import supr http://mathhub.info/MitM/smglom/supremum ❚ theory BochnerIntegral : base:?Logic = bochnerIntegrable ❙ ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/measures ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import lfx http://gl.mathhub.info/MMT/LFX/Sigma ❚ import exr http://mathhub.info/MitM/smglom/arithmetics ❚ import seq http://cds.omdoc.org/urtheories ❚ import desc http://mathhub.info/MitM/smglom/DescriptionOperators❚ import calc http://mathhub.info/MitM/smglom/calculus ❚ theory RiemannIntegrable : base:?Logic = ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/measures ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import lfx http://gl.mathhub.info/MMT/LFX/Sigma ❚ import exr http://mathhub.info/MitM/smglom/arithmetics ❚ import seq http://cds.omdoc.org/urtheories ❚ import desc http://mathhub.info/MitM/smglom/DescriptionOperators❚ theory LebesgueMeasure : base:?Logic = include ?Measure ❙ ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/measures ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import lfx http://gl.mathhub.info/MMT/LFX/Sigma ❚ import exr http://mathhub.info/MitM/smglom/arithmetics ❚ import seq http://cds.omdoc.org/urtheories ❚ import desc http://mathhub.info/MitM/smglom/DescriptionOperators❚ import calc http://mathhub.info/MitM/smglom/calculus ❚ theory OuterMeasure : base:?Logic = include ts:?SetCollection ❙ theory outerMeasure_theory : base:?Logic = measure ❙ emptyIsZero ❚ ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/measures ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import lfx http://gl.mathhub.info/MMT/LFX/Sigma ❚ import exr http://mathhub.info/MitM/smglom/arithmetics ❚ import seq http://cds.omdoc.org/urtheories ❚ import desc http://mathhub.info/MitM/smglom/DescriptionOperators❚ import calc http://mathhub.info/MitM/smglom/calculus ❚ theory RiemannIntegrable : base:?Logic = include calc:?Intervals ❙ include ?AlmostEverywhere ❙ prop_lebesgueCriterion ❙ ❚ \ No newline at end of file
 ... ... @@ -95,3 +95,17 @@ theory CountingMeasure : base:?Logic = countingMeasureSpace : type ⟶ measureSpace ❘ // slow! = [A] ['universe := A , sigma_algebra := powerSigmaAlgebra A , measure := countingMeasure A (powerSigmaAlgebra A) '] ❙ ❚ theory NullSets : base:?Logic = include ?Measure ❙ isNullSet : {m : measureSpace} set (m.universe) ⟶ bool ❘// slow! = [m , s] (s ∈ m.sigma_algebra.coll) ∧ (((m.measure.measure) (elem (m.sigma_algebra.coll) s)) ≐ 0)❙ allNullSets : {m : measureSpace} collection (m.universe) ❘// slow!= [m] ⟪ (m.sigma_algebra.coll) | ([s] (((m.measure.measure) (elem (m.sigma_algebra.coll) s)) ≐ 0))⟫ ❙ ❚ theory AlmostEverywhere : base:?Logic = include ?NullSets ❙ almostEverywhere : {m : measureSpace} ((m.universe) ⟶ bool) ⟶ bool ❘ = [m,P] ∃ [n] n ∈ (allNullSets m) ∧ (∀[x] x ∈ (fullset (m.universe) \ n) ⇒ P x)❘# AE 1 2❙ ❚
 namespace http://mathhub.info/MitM/smglom/probability ❚ import base http://mathhub.info/MitM/Foundation ❚ theory AI1 : base:?Logic = ❚
 ... ... @@ -22,13 +22,12 @@ theory ProbabilityMeasure : base:?Logic = theory ProbabilitySpaceTheorems : base:?Logic = include ?ProbabilityMeasure ❙ include measures?LebesgueIntegral ❙ include calculus?LebesgueIntegral ❙ include measures?Measurable ❙ include measures?LebesgueMeasurable ❙ theory probabilitySpaceTheorems_theory : base:?Logic > PS : probabilitySpace ❘ = include measures?LebesgueIntegral ❙ omega = (PS.universe) ❘ # Ω ❙ probability : (typeof (set (PS.universe)) (PS.sigma_algebra.coll)) ⟶ ℝ ❘ // slow! = (PS.measure.measure) ❙ events : collection (PS.universe) ❘ // sometimes slow! = (PS.sigma_algebra.coll) ❙ ... ... @@ -39,17 +38,17 @@ theory ProbabilitySpaceTheorems : base:?Logic = // variance : Ω ⟶ ℝ ❙ isRandomVariable : {A : type} ((PS.universe) ⟶ A) ⟶ sigmaAlgebra A ⟶ bool ❘ ❙ randomVariable : {A : type} Σ t : (((PS.universe) ⟶ A) × sigmaAlgebra A) . ⊦ isRandomVariable A (πl t) (πr t) ❙ randomVariable : {A : type} ⟨ t : (((PS.universe) ⟶ A) × sigmaAlgebra A) | ⊦ isRandomVariable A (πl t) (πr t) ⟩ ❙ isRealValuedRandomVariable : ((PS.universe) ⟶ ℝ) ⟶ bool ❘= [f] ❙ realValuedRandomVariable = Σ f: ((PS.universe) ⟶ ℝ) . ⊦ isRealValuedRandomVariable f ❘# ℝRv ❙ isRealValuedRandomVariable : ((PS.universe) ⟶ ℝ) ⟶ bool ❘// = [f] ❙ realValuedRandomVariable = ⟨ f: ((PS.universe) ⟶ ℝ) | ⊦ isRealValuedRandomVariable f ⟩ ❘# ℝRv ❙ // theorems ❙ lemma_probabilityLe1 : ⊦ ∀[x : set Ω] probability x ≤ 1 ❙ // lemma_probabilityLe1 : ⊦ ∀[x : set Ω] probability x ≤ 1 ❙ lemma_omegaNotEmpty : ⊦ fullset Ω ≠ ∅ ❙ lemma_probabilityGe1Eq1 : {x : set Ω} ⊦ 1 ≤ probability x ⟶ ⊦ probability x ≐ 1 ❙ // lemma_probabilityGe1Eq1 : {x : set Ω} ⊦ 1 ≤ probability x ⟶ ⊦ probability x ≐ 1 ❙ ❚ ... ... @@ -57,9 +56,5 @@ theory ProbabilitySpaceTheorems : base:?Logic = ❚ theory bla : base:?Logic = ❚
 namespace http://mathhub.info/MitM/smglom/typedsets ❚ import base http://mathhub.info/MitM/Foundation ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ theory IndicatorFunction : base:?Logic = include ?AllSets ❙ include arith:?NaturalNumbers ❙ indicatorFunction : {A : type} set A ⟶ A ⟶ ℕ ❘= [A,s,a] if (a ∈ s) then (1 : ℕ) else 0 ❘ ❙ ❚ \ No newline at end of file
 ... ... @@ -4,7 +4,8 @@ import base http://mathhub.info/MitM/Foundation ❚ import sig http://gl.mathhub.info/MMT/LFX/Sigma ❚ theory FiniteSets : sig:?LFSigma = theory FiniteSets : base:?Logic = include base:?ProductType ❙ include ?AllSets ❙ ... ...
 namespace http://mathhub.info/MitM/smglom/typedsets ❚ import base http://mathhub.info/MitM/Foundation ❚ import ar http://mathhub.info/MitM/smglom/arithmetics ❚ theory PrOSet : base:?Logic = include ?Relations ❙ ... ... @@ -81,4 +82,10 @@ theory POSet : base:?Logic = poset = Mod poset_theory ❘ role abbreviation ❙ ❚ theory SupremumReal : base:?Logic = include ?AllSets ❙ include ?LeastMost ❙ include ar:?ExtendedReals ❙ supremumReal : set ℝ ⟶ ℝ❘= [s] least ([a] ∀[x] x ∈ s ⇒ x ≤ a) ([a,b] a ≤ b) ❘# supR 1 ❙ ❚
 ... ... @@ -6,8 +6,7 @@ import sig http://gl.mathhub.info/MMT/LFX/Sigma ❚ import ar http://mathhub.info/MitM/smglom/arithmetics ❚ theory SetSum : base:?Logic = include ar:?RealArithmetics ❙ include sig:?LFSigma ❙ include ar:?RealArithmetics ❙ include ts:?FiniteSets ❙ ... ...
 namespace http://mathhub.info/MitM/smglom/typedsets ❚ import base http://mathhub.info/MitM/Foundation ❚ import sig http://gl.mathhub.info/MMT/LFX/Sigma ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ theory TypedSets : base:?Logic = include base:?Lists ❙ ... ... @@ -129,7 +129,14 @@ theory SetStructures : base:?Logic = dom : setstruct ⟶ type ❘ = [S] (S.universe) ❘ role abbreviation❙ doms : {S : setstruct}set (dom S) ❘ = [S] fullset (dom S) ❘ role abbreviation ❙ ❚ theory IndicatorFunction : base:?Logic = include ?TypedSets ❙ include arith:?NaturalNumbers ❙ include base:?DescriptionOperator ❙ indicatorFunction : {A : type} set A ⟶ A ⟶ ℕ ❘= [A,s,a] if (a ∈ s) then (1 : ℕ) else 0 ❘ ❙ ❚ theory AllSets : base:?Logic = include ?FiniteCardinality ❙ ... ... @@ -160,7 +167,7 @@ theory SetCollection : base:?Logic = theory TaggedSetCollection : base:?Logic = include ?SetCollection ❙ include sig:?LFSigma ❙ include base:?ProductType ❙ taggedCollection : type ⟶ type ❘= [G] set (G × set G) ❙ ... ...
 namespace http://mathhub.info/MitM/smglom/supremum❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import ar http://mathhub.info/MitM/smglom/arithmetics ❚ theory SupremumReal : base:?Logic = include ts:?AllSets ❙ include ts:?LeastMost ❙ include ar:?ExtendedReals ❙ supremumReal : set ℝ ⟶ ℝ ❘= [s] least ([a] ∀[x] x ∈ s ⇒ x ≤ a) ([a,b] a ≤ b) ❘# supR 1 ❙ ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/topology ❚ import base http://mathhub.info/MitM/Foundation ❚ import calc http://mathhub.info/MitM/smglom/calculus ❚ theory RealTopology : base:?Logic = include calc:?RealMetricSpace❙ include calc:?MetricSpaceAsTopology ❙ include ?OpenSetTopology ❙ realTopology = metricAsTopology realmetricspace ❘ : topology ℝ❙ realTopologicalSpace = [' universe := ℝ , topology := realTopology '] ❘: topologicalSpace ❙ ❚ \ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!