Commit 3dde8c35 authored by Sven Wille's avatar Sven Wille

probability and finsequences and inductively defined natural numbers

parent 745c560c
<errors>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦∅∈A.coll" level="1">
<stacktrace>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12(RuleBasedChecker.scala:88)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12$adapted(RuleBasedChecker.scala:85)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:85)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:218)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13(MMTStructureChecker.scala:226)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13$adapted(MMTStructureChecker.scala:223)</element>
<element>scala.Option.foreach(Option.scala:257)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:223)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:69)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:88)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:99)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:493)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:664)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:471)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:744)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:744)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:565)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:471)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:744)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:744)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:410)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:189)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:189)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:179)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:94)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:157)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
</error>
</errors>
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/measures/measures.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#0.0.0:5126.110.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/measures"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import ts http://mathhub.info/MitM/smglom/typedsets"/><instruction text="import lfx http://gl.mathhub.info/MMT/LFX/Sigma"/><instruction text="import exr http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import seq http://cds.omdoc.org/urtheories"/><instruction text="import desc http://mathhub.info/MitM/smglom/DescriptionOperators"/><mref name="[http://mathhub.info/MitM/smglom/measures?Additive]" target="http://mathhub.info/MitM/smglom/measures?Additive"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#377.9.0:391.9.14"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?SigmaAdditive]" target="http://mathhub.info/MitM/smglom/measures?SigmaAdditive"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#722.18.0:741.18.19"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?Measure]" target="http://mathhub.info/MitM/smglom/measures?Measure"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#1224.29.0:1237.29.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?PowerSigmaAlgebra]" target="http://mathhub.info/MitM/smglom/measures?PowerSigmaAlgebra"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#2345.56.0:2368.56.23"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?CountingMeasure]" target="http://mathhub.info/MitM/smglom/measures?CountingMeasure"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#3285.76.0:3306.76.21"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?NullSets]" target="http://mathhub.info/MitM/smglom/measures?NullSets"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#4501.97.0:4515.97.14"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?AlmostEverywhere]" target="http://mathhub.info/MitM/smglom/measures?AlmostEverywhere"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#4900.105.0:4922.105.22"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/measures/measures.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#0.0.0:5570.123.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/measures"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import ts http://mathhub.info/MitM/smglom/typedsets"/><instruction text="import lfx http://gl.mathhub.info/MMT/LFX/Sigma"/><instruction text="import exr http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import seq http://cds.omdoc.org/urtheories"/><instruction text="import desc http://mathhub.info/MitM/smglom/DescriptionOperators"/><mref name="[http://mathhub.info/MitM/smglom/measures?Additive]" target="http://mathhub.info/MitM/smglom/measures?Additive"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#377.9.0:391.9.14"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?SigmaAdditive]" target="http://mathhub.info/MitM/smglom/measures?SigmaAdditive"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#722.18.0:741.18.19"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?Measure]" target="http://mathhub.info/MitM/smglom/measures?Measure"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#1224.29.0:1237.29.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?PowerSigmaAlgebra]" target="http://mathhub.info/MitM/smglom/measures?PowerSigmaAlgebra"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#2344.56.0:2367.56.23"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?CountingMeasure]" target="http://mathhub.info/MitM/smglom/measures?CountingMeasure"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#3284.76.0:3305.76.21"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?NullSets]" target="http://mathhub.info/MitM/smglom/measures?NullSets"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#4500.97.0:4514.97.14"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?AlmostEverywhere]" target="http://mathhub.info/MitM/smglom/measures?AlmostEverywhere"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#4899.105.0:4921.105.22"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?BorelMeasurableSpace]" target="http://mathhub.info/MitM/smglom/measures?BorelMeasurableSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#5129.113.0:5155.113.26"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?RealBorelMeasurableSpace]" target="http://mathhub.info/MitM/smglom/measures?RealBorelMeasurableSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#5368.119.1:5398.119.31"/></metadata></mref></omdoc>
\ No newline at end of file
......@@ -96,9 +96,9 @@ DependsOn http://mathhub.info/MitM/smglom/measures?Measure/measure_theory?axiom_
DependsOn http://mathhub.info/MitM/smglom/measures?Measure/measure_theory?axiom_emptyiszero?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/MitM/smglom/measures?Measure/measure_theory?axiom_emptyiszero?type http://mathhub.info/MitM/Foundation?Logic?eq?type
DependsOn http://mathhub.info/MitM/smglom/measures?Measure/measure_theory?axiom_emptyiszero?type http://mathhub.info/MitM/smglom/measures?SigmaAlgebra?sigmaAlgebra?definition
DependsOn http://mathhub.info/MitM/smglom/measures?Measure/measure_theory?axiom_emptyiszero?type http://mathhub.info/MitM/Foundation?InformalProofs?trivial?type
DependsOn http://mathhub.info/MitM/smglom/measures?Measure/measure_theory?axiom_emptyiszero?type http://mathhub.info/MitM/smglom/typedsets?SetCollection?collection?definition
DependsOn http://mathhub.info/MitM/smglom/measures?Measure/measure_theory?axiom_emptyiszero?type http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/MitM/smglom/measures?Measure/measure_theory?axiom_emptyiszero?type http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type
DependsOn http://mathhub.info/MitM/smglom/measures?Measure/measure_theory?axiom_emptyiszero?type http://mathhub.info/MitM/smglom/typedsets?TypedSets?inSet?definition
DependsOn http://mathhub.info/MitM/smglom/measures?Measure/measure_theory?axiom_emptyiszero?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/measures?Measure/measure_theory?axiom_emptyiszero?type http://mathhub.info/MitM/smglom/typedsets?EmptySet?emptySet?type
......
......@@ -6,3 +6,5 @@ Declares http://mathhub.info/MitM/smglom/measures/measures.omdoc http://mathhub.
Declares http://mathhub.info/MitM/smglom/measures/measures.omdoc http://mathhub.info/MitM/smglom/measures?CountingMeasure
Declares http://mathhub.info/MitM/smglom/measures/measures.omdoc http://mathhub.info/MitM/smglom/measures?NullSets
Declares http://mathhub.info/MitM/smglom/measures/measures.omdoc http://mathhub.info/MitM/smglom/measures?AlmostEverywhere
Declares http://mathhub.info/MitM/smglom/measures/measures.omdoc http://mathhub.info/MitM/smglom/measures?BorelMeasurableSpace
Declares http://mathhub.info/MitM/smglom/measures/measures.omdoc http://mathhub.info/MitM/smglom/measures?RealBorelMeasurableSpace
namespace http://mathhub.info/MitM/smglom/Probability ❚
import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/smglom/typedsets ❚
import meas http://mathhub.info/MitM/smglom/measures ❚
// import sub http://gl.mathhub.info/MMT/LFX/Subtyping ❚
theory ProbabilityMeasure : base:?Logic =
......@@ -43,17 +44,18 @@ theory ProbabilityTheoryDefinitions : base:?Logic =
include ?ProbabilityTheoryDefinitions/BasicDefinitions (PS) ❙
isRandomVariable : {ms : measurableSpace} ((PS.universe) ⟶ (ms.universe)) ⟶ bool ❘= [ms,X] measurable eventsSigmaAlgebra (ms.sigma_algebra) X ❙
randomVariable : measurableSpace ⟶ type ❘= [MS] ⟨ t : ((PS.universe) ⟶ (MS.universe)) | ⊦ isRandomVariable MS t ⟩ ❙
bla : {A : type} set A ⟶ prop ❙
isDiscreteRandomVariable : {ms : measurableSpace} randomVariable ms ⟶ prop ❘ = [ms, X] (im X (fullset (PS.universe) )) finite ❙
discreteRandomVariable : measurableSpace ⟶ type ❘ = [ms] ⟨ X : randomVariable ms | ⊦ isDiscreteRandomVariable ms X ⟩❙
theory RealValuedRandomVariable : base:?Logic > PS : probabilitySpace ❘ =
include ?ProbabilityTheoryDefinitions/RandomVariables (PS) ❙
include measures?RealBorelMeasurableSpace ❙
// isRealValuedRandomVariable : ((PS.universe) ⟶ ℝ) ⟶ prop ❘ = [f] realBorelMeasurable (PS.universe) eventsSigmaAlgebra f❙
// realValuedRandomVariable = ⟨ f: ((PS.universe) ⟶ ℝ) | ⊦ isRealValuedRandomVariable f ⟩ ❘# ℝRv ❙
// bla : {A : type} randomVarixable A ⟶ set A❘ = [A,X] im X (fullset (PS.universe))❙
// isDiscreteRandomVariable : {A : type} randomVariable A ⟶ bool ❘ = [X] finite (image X (fullset (PS.universe))) ❙
// discreteRandomVariable ❙
isRealValuedRandomVariable : ((PS.universe) ⟶ ℝ) ⟶ prop ❘ = [f] isRandomVariable realBorelMeasurableSpace f❙
realValuedRandomVariable = randomVariable realBorelMeasurableSpace ❙
// isDiscreteRealValuedRandomVariable ❙
// sw: this one has redundancy in it since the proof that X is quasiitegrable over PS and the borel measure space of ℝ covers that it is a realvalued
......
namespace http://mathhub.info/MitM/smglom/arithmetics ❚
import base http://mathhub.info/MitM/Foundation ❚
import lfxwt http://gl.mathhub.info/MMT/LFX/WTypes ❚
theory NaturalNumbers : base:?Logic =
include base:?NatLiterals ❙
......@@ -91,26 +90,25 @@ theory NaturalArithmetics : base:?Logic =
theory InductiveNaturalNumbers : lfxwt:?Inductive =
theory InductiveNaturalNumbers : base:?InductiveTypes =
induct Nats ()❘ =
Natt : type ❙
Zero : Natt
Succ : Natt ⟶ Natt ❙
Nat : type ❙
Zero : Nat ❙
Suc : Nat ⟶ Nat ❙
def Natid () ❘ =
recc : Natt ⟶ Natt ❙
Zero = Zero ❙
Succ = [m : Natt] Succ (recc m)❙
theory NatConversions : lfxwt:?Inductive =
// include ?InductiveNaturalNumbers❙
// include ?NaturalNumbers ❙
// natlitToNat : ℕ ⟶ Nat❙
bla = prop ❙
theory NatConversions : base:?InductiveTypes =
include ?InductiveNaturalNumbers❙
include ?NaturalArithmetics ❙
natlitToNat : ℕ ⟶ Nat❙
def NatToNatlit () ❘ =
recFn : Nat ⟶ ℕ ❙
Zero = 0 ❙
Suc = [m : Nat] 1 + (recFn m)❙
......@@ -109,3 +109,16 @@ theory AlmostEverywhere : base:?Logic =
almostEverywhere : {m : measureSpace} ((m.universe) ⟶ bool) ⟶ bool ❘
= [m,P] ∃ [n] n ∈ (allNullSets m) ∧ (∀[x] x ∈ (fullset (m.universe) \ n) ⇒ P x)❘# AE 1 2❙
theory BorelMeasurableSpace : base:?Logic =
include ?Measure ❙
include ?BorelMeasurable ❙
borelMeasurableSpace : {t : topologicalSpace} measurableSpace ❘ = [t] [' universe := (t.universe) , sigma_algebra := borelSigma t']❙
theory RealBorelMeasurableSpace : base:?Logic =
include ?Measure ❙
include ?BorelMeasurableSpace ❙
realBorelMeasurableSpace : measurableSpace ❘ = borelMeasurableSpace realTopologicalSpace ❙
\ 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!
Please register or to comment