Commit c8b9cf7e authored by Sven Wille's avatar Sven Wille

new nat type , redid the finsequences

parent 3dde8c35
<errors>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: could not prove ⊦(succB toB 3)&lt;(([n]succ_nat_lit n) 4)" 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.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>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: could not prove ⊦(succB toB 3)&lt;(([n]succ_nat_lit n) (([n]succ_nat_lit n) 3))" 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.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/arithmetics/naturals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#0.0.0:3754.88.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/arithmetics"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#108.4.0:128.4.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#409.15.0:433.15.24"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#0.0.0:5504.158.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/arithmetics"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#108.4.0:128.4.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#409.15.0:433.15.24"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?InductiveNaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?InductiveNaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#3825.92.0:3855.92.30"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?INatArith]" target="http://mathhub.info/MitM/smglom/arithmetics?INatArith"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#4134.108.0:4149.108.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?Between]" target="http://mathhub.info/MitM/smglom/arithmetics?Between"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#4743.137.0:4756.137.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NatConversions]" target="http://mathhub.info/MitM/smglom/arithmetics?NatConversions"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#5236.149.0:5256.149.20"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/calculus/FinSequences.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/FinSequences.mmt#0.0.0:1723.41.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"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/smglom/arithmetics"/><mref name="[http://mathhub.info/MitM/smglom?FinSequences]" target="http://mathhub.info/MitM/smglom?FinSequences"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/FinSequences.mmt#157.6.0:175.6.18"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/calculus/FinSequences.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/FinSequences.mmt#0.0.0:1045.29.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"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/smglom/arithmetics"/><mref name="[http://mathhub.info/MitM/smglom?FinSequences]" target="http://mathhub.info/MitM/smglom?FinSequences"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/FinSequences.mmt#158.7.0:176.7.18"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom?FinSeqProps]" target="http://mathhub.info/MitM/smglom?FinSeqProps"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/FinSequences.mmt#363.19.0:380.19.17"/></metadata></mref></omdoc>
\ No newline at end of file
document http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?InductiveNaturalNumbers
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?INatArith
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?Between
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?NatConversions
document http://mathhub.info/MitM/smglom/calculus/FinSequences.omdoc
Declares http://mathhub.info/MitM/smglom/calculus/FinSequences.omdoc http://mathhub.info/MitM/smglom?FinSequences
Declares http://mathhub.info/MitM/smglom/calculus/FinSequences.omdoc http://mathhub.info/MitM/smglom?FinSeqProps
......@@ -42,28 +42,36 @@ theory ProbabilityTheoryDefinitions : base:?Logic =
theory RandomVariables : base:?Logic > PS : probabilitySpace ❘ =
include ?ProbabilityTheoryDefinitions/BasicDefinitions (PS) ❙
include ts:?CountablyInfinite ❙
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 ❙
isDiscreteRandomVariable : {ms : measurableSpace} randomVariable ms ⟶ prop ❘ = [ms, X] (im X (fullset (PS.universe) )) finite ∨ is_countablyInfinite (im X (fullset (PS.universe) ))❙
discreteRandomVariable : measurableSpace ⟶ type ❘ = [ms] ⟨ X : randomVariable ms | ⊦ isDiscreteRandomVariable ms X ⟩❙
theory RealValuedRandomVariable : base:?Logic > PS : probabilitySpace ❘ =
theory RealValuedRandomVariables : base:?Logic > PS : probabilitySpace ❘ =
include ?ProbabilityTheoryDefinitions/RandomVariables (PS) ❙
include measures?RealBorelMeasurableSpace ❙
isRealValuedRandomVariable : ((PS.universe) ⟶ ℝ) ⟶ prop ❘ = [f] isRandomVariable realBorelMeasurableSpace f❙
realValuedRandomVariable = randomVariable realBorelMeasurableSpace ❙
// isDiscreteRealValuedRandomVariable ❙
isDiscreteRealValuedRandomVariable : realValuedRandomVariable ⟶ bool ❘ = [X] isDiscreteRandomVariable realBorelMeasurableSpace X❙
discreteRealValuedRandomVariable = discreteRandomVariable realBorelMeasurableSpace❙
// 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
random variable. I left it in (the constraint that X has to be a realValuedRandomVariable) since it makes it more clear what the expectation is ❙
// expectation : { X : realValuedRandomVariable } {XisLmes : ⊦ lebesgueMeasurableLeq (PS.sigma_algebra) X} ⊦ quasiIntegrable PS X XisLmes ⟶ ℝ ❘= [X,h,h0]lebesgueIntegral PS X h h0❙
// variance : ❙
// theorems ❙
theory Expectaion : base:?Logic > PS : probabilitySpace ❘ =
include ?ProbabilityTheoryDefinitions/RealValuedRandomVariables (PS) ❙
expectation : { X : realValuedRandomVariable } {XisLmes : ⊦ lebesgueMeasurableLeq (PS.sigma_algebra) X} ⊦ quasiIntegrable PS X XisLmes ⟶ ℝ ❘= [X,h,h0]lebesgueIntegral PS X h h0❙
finiteDiscreteExpectation ❙
discreteExpectation ❙
theory Variance : base:?Logic > PS : probabilitySpace ❘ =
// lemma_probabilityLe1 : ⊦ ∀[x : set Ω] probability x ≤ 1 ❙
// lemma_omegaNotEmpty : ⊦ fullset Ω ≠ ∅ ❙
// lemma_probabilityGe1Eq1 : {x : set Ω} ⊦ 1 ≤ probability x ⟶ ⊦ probability x ≐ 1 ❙
......
......@@ -92,23 +92,69 @@ theory NaturalArithmetics : base:?Logic =
theory InductiveNaturalNumbers : base:?InductiveTypes =
induct Nats ()❘ =
Nat : type ❙
Zero : Nat ❙
Suc : Nat ⟶ Nat ❙
INat : type ❙
Zero : INat ❙
Suc : INat ⟶ INat ❙
def naturalcases (A : type , a : A , F : (INat ⟶ A)) ❘ =
ncases : INat ⟶ INat ❙
Zero = Zero ❙
Suc = [m : INat] F m❙
theory INatArith : base:?InductiveTypes =
include ?InductiveNaturalNumbers ❙
def additionNat (n : INat) ❘ =
add : INat ⟶ INat ❘ # 1 + 2 ❙
Zero = n ❙
Suc = [m] add m ❙
def subtractionNat () ❘ =
sub : INat ⟶ INat ⟶ INat ❘ # 1 - 2 prec 15❙
Zero = Zero ❙
Suc = [n][m] ncases INat (Suc n) ([v] sub n v) m ❙
def leNat () ❘ =
leN : INat ⟶ INat ⟶ prop ❘# 1 ≤ 2❙
Zero = [v : INat] true ❙
Suc = [m][n] ncases prop false ([v] leN m v) n❙
ltN : INat ⟶ INat ⟶ prop ❘ = [n][m] Suc n ≤ m ❘ # 1 < 2 ❙
theory Between : base:?InductiveTypes =
include ?INatArith❙
include base:?Subtyping ❙
// added by sw ❙
// this one is needed to create a possibly empty subset of the natural numbers (this way we can create empty finite sequences)❙
/T finite subset of the natural numbers ❙
between : INat ⟶ INat ⟶ type ❘= [f,t] ⟨ x : INat | ⊦ f ≤ x ∧ x ≤ t⟩ ❙
// convenience function for between ❙
betweenOneAnd : INat ⟶ type ❘= [t] ⟨ x : INat | ⊦ Suc Zero ≤ x ∧ x ≤ t⟩ ❙
theory NatConversions : base:?InductiveTypes =
include ?InductiveNaturalNumbers❙
include ?NaturalArithmetics ❙
natlitToNat : ℕ ⟶ Nat❙
natlitToNat : ℕ ⟶ INat❙
def NatToNatlit () ❘ =
recFn : Nat ⟶ ℕ ❙
recFn : INat ⟶ ℕ ❙
Zero = 0 ❙
Suc = [m : Nat] 1 + (recFn m)❙
Suc = [m : INat] 1 + (recFn m)❙
......@@ -3,70 +3,34 @@ namespace http://mathhub.info/MitM/smglom ❚
import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
import lfxwt http://gl.mathhub.info/MMT/LFX/WTypes ❚
import lfx http://gl.mathhub.info/MMT/LFX/Sigma ❚
import top http://gl.mathhub.info/MMT/LFX ❚
theory FinSequences : base:?Logic =
include arith:?NaturalArithmetics ❙
// below : ℕ ⟶ type ❘ = [n] ⟨ x : ℕ | ⊦ x < n⟩ ❙
theory FinSequences : base:?InductiveTypes =
include arith:?INatArith ❙
/T finite sequences ❙
finiteSequence : ℕ ⟶ type ⟶ type ❘= [n , A] betweenOneAnd n ⟶ A ❘# finSeq 1 2 ❙
finiteSequence : INat ⟶ type ⟶ type ❘= [n : INat , A] {x : INat} ⊦ leN (Suc Zero) x ⟶ ⊦ (leN x n) ⟶ A ❘# finSeq 1 2 ❙
// disjointFinSeq_prop : {n : ℕ, A : type} finSeq n A ⟶ bool ❘= [n,A,fs] ∀[x] ∀[y] ∀ [h : ⊦ x < n] ∀ [h0 : ⊦ y < n] y ≐ x ∨ fs x h ≠ fs y h0❙
theory blaaa : lfxwt:?Inductive =
induct Nats ()❘ =
Nat : type ❘ # ℕ ❙
Zero : ℕ ❘ # O ❙
Succ : ℕ ⟶ ℕ ❘ # S 1 ❙
bla : ℕ ❘ = 1 ❙
theory FinSeqProps : base:?Logic =
theory FinSeqProps : base:?InductiveTypes =
include arith:?RealArithmetics ❙
include ?FinSequences ❙
/T A disjoint ❙
prop_disjointFinSeq : {n : ℕ, A : type} finSeq n A ⟶ bool ❘= [n,A,fs] ∀[x] ∀[y] y ≐ x ∨ fs x ≠ fs y ❘# disjoint 3❙
asceindingLoop
prop_disjointFinSeq : {n : INat, A : type} finSeq n A ⟶ bool ❘= [n,A,fs] ∀[x] ∀[y] ∀[hx1] ∀[hx2] ∀[hy1] ∀[hy2] y ≐ x ∨ fs x hx1 hx2 ≠ fs y hy1 hy2
// ascendingfn : {n : ℕ} finSeq n ℝ ⟶ bool ❘ = [n,sq] ascending ❘# ascending 2 ❙
prop_ascendingfn : {n : INat} finSeq n ℝ ⟶ bool ❘ = [n,fsq] ∀[x] ∀[y] ∀[hx1] ∀[hx2] ∀[hy1 ] ∀[hy2] leN x y ⇒ arith?RealArithmetics?leq (fsq x hx1 hx2) (fsq y hy1 hy2) ❘# ascending 2 ❙
prop_strictly_ascendingfn : {n : INat} finSeq n ℝ ⟶ bool ❘ = [n,fsq] ∀[x] ∀[y] ∀[hx1] ∀[hx2] ∀[hy1 ] ∀[hy2] leN x y ⇒ arith?RealArithmetics?lessthan (fsq x hx1 hx2) (fsq y hy1 hy2) ❘# strictly_ascending 2 ❙
def strictly_ascending_rec () ❘ =
strictly_asc_rec : {m : INat}{n : INat} finSeq n ℝ ⟶ bool ❘ # strictAscRec 1 3 ❙
theory FinSeqSum : base:?Logic =
include ?FinSequences ❙
include arith:?RealArithmetics ❙
include arith:?NaturalArithmetics ❙
// sw: old version of finSeqSumRec. I leave it here in case I need it in the future ❙
// this one does the actual recusive summation and is called by finSeqSum ❙
// finSeqSumRec : {n : ℕ} {m : ℕ } ⊦ `arith:?NaturalArithmetics?lessthan m n ⟶ finSeq n ℝ ⟶ ℝ ❘# finSeqSumR 2 3 4❙
// finSeqSumRecB : {n : ℕ} {sq : finSeq n ℝ} {h : ⊦ `arith:?NaturalArithmetics?lessthan 0 n} ⊦ finSeqSumRec n 0 h sq ≐ 0 ❙
// finSeqSumRecS : {n : ℕ} {m : ℕ} {sq : finSeq n ℝ} {h : ⊦ `arith:?NaturalNumbers?succ m < n}
⊦ finSeqSumR ( `arith:?NaturalNumbers?succ m) h sq ≐
sq (`arith:?NaturalNumbers?succ m) h + finSeqSumR m (lt_pred_lt h) sq❙
finSeqSumRec : {n : ℕ} betweenOneAnd n ⟶ finSeq n ℝ ⟶ ℝ ❘# finSeqSumR 1 2 3❙
finSeqSumRecB : {n : ℕ} {sq : finSeq n ℝ} ⊦ finSeqSumRec n 1 sq ≐ sq 1 ❙
finSeqSumRecS : {n : ℕ} {m : betweenOneAnd n} {sq : finSeq n ℝ}
⊦ finSeqSumR n ( `arith:?NaturalNumbers?succ m) sq ≐
sq (`arith:?NaturalNumbers?succ m) + finSeqSumR n m sq❙
finSeqSum : {n : ℕ} finSeq n ℝ ⟶ ℝ❙
// the function implementation currently doesn't type check (between n < Nat) ❙
// finSeqSumZero : {sq} ⊦ finSeqSum 0 sq ≐ 0 ❙
// finSeqSumFn : {n : ℕ} {sq : finSeq n ℝ} ⊦ finSeqSum n sq ≐ finSeqSumRec n n sq❙
\ No newline at end of file
......@@ -5,6 +5,8 @@ import base http://mathhub.info/MitM/Foundation ❚
import meta http://cds.omdoc.org/mmt ❚
// author: Theresa Pollinger ❚
......@@ -35,7 +37,9 @@ theory Intervals : base:?Logic =
leftPred := ([x,y] x ≤ y),
rightPred := ([x,y] x ≤ y)
'] ❘ # [ 1 ; 2 ] ❙
type_closedInterval : ℝ ⟶ ℝ ⟶ type ❘= [l,r] ⟨ iv : interval | ⊦ iv ≐ closedInterval l r⟩ ❘ # cInterval 1 2❙
theory OneCuboid : base:?Logic =
......@@ -88,4 +92,12 @@ theory GeneralDomains : base:?Logic =
DomainPred = interval_pred ❙
BoundaryPred = boundary_pred ❙
// vec_pred_as_sub = pred_as_sub ❙
theory IntervalPartition : base:?Logic =
include ?Intervals ❙
include top:?FinSeqProps ❙
// intervalPartition : interval ⟶ type ❘ = [i] ❙
prop_is_closedinterval_partittion : {l : ℝ } {r : ℝ} {n : INat} cInterval l r ⟶ finSeq n ℝ ⟶ prop ❘ = [l,r,n, ci, fs] strictly_ascending fs ❙
......@@ -10,7 +10,7 @@ import exr http://mathhub.info/MitM/smglom/arithmetics ❚
theory IntervalPartition : base:?Logic =
include ?Intervals ❙
partitionOfInterval : interval ⟶ type ❘ = [i] ❙
intervalPartition : interval ⟶ type ❘ = [i] ❙
......
namespace http://mathhub.info/MitM/smglom/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚
import natt http://mathhub.info/MitM/smglom/arithmetics ❚
theory Countable : base:?InductiveTypes =
include ?Injective ❙
include ?AllSets ❙
include natt:?InductiveNaturalNumbers ❙
prop_countableSet : {A : type} set A ⟶ prop ❘= [A,S] ∃ [f : setastype S ⟶ Nat] is_injective f ❘# is_countable 2 ❙
lemma_finiteSetIsCountable : {A : type} {s : set A} ⊦ s finite ⟶ ⊦ is_countable s ❙
theory CountablyInfinite : base:?InductiveTypes =
include ?Countable ❙
include ?Bijective ❙
prop_countablyInfiniteSet : {A : type} set A ⟶ prop ❘= [A,S] ∃ [f : setastype S ⟶ Nat] is_bijective f ❘# is_countablyInfinite 2 ❙
lemma_countablyInfiniteSetsAreCountable : {A : type} {s : set A} ⊦ is_countablyInfinite s ⟶ ⊦ is_countable s ❙
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