namespace http://mathhub.info/MitM/core/calculus ❚

import base http://mathhub.info/MitM/Foundation ❚
import sets http://mathhub.info/MitM/core/typedsets ❚

theory Sequences : base:?Logic =
   include ?MetricSpace ❙
   include ☞sets:?AllSets ❙
   // MiKo: should G here not be a metric space? ❙
   sequence : {G: type}type ❘ = [G] ℕ ⟶ G ❘ # 1 ^ω prec 1 ❙
   structseq : {G : setstruct}type ❘ = [G] (G.universe)^ω ❘ # 1 ^ω❙
   
   // prop_isSupremum : {G: metricSpace} G^ω ⟶ G.universe ⟶ prop  ❘
   		= [G,a,l] ∀[ε : ℝ+] (∀[n : ℕ] a n < l + ε) ∧ (∃[n : ℕ] a n > l - ε) ❙
   // prop_isInfimum : {G: metricSpace} G^ω ⟶ G.universe ⟶ prop  ❘
   		= [G,a,l] ∀[ε : ℝ+] (∀[n : ℕ] a n > l - ε) ∧ (∃[n : ℕ] a n < l + ε) ❙
   // prop_hasSupremum : {G: metricSpace} G^ω ⟶ prop  ❘
   		= [G,a] ∃![g] prop_isSupremum G a g   ❙
   // prop_hasInfimum : {G: metricSpace} G^ω ⟶ prop  ❘
   		= [G,a] ∃![g] prop_isInfimum G a g    ❙
   // supremum : {G : metricSpace, a : G^ω, p : ⊦ prop_hasSupremum G a} dom G ❘
   		= [G, a, p] that (dom G) ([g] prop_isSupremum G a g) p ❘
   		# sup 2 %I3 ❙
   // infimum : {G : metricSpace, a : G^ω, p : ⊦ prop_hasInfimum G a} dom G ❘
   		= [G, a, p] that (dom G) ([g] prop_isInfimum G a g) p ❘
   		# inf 2 %I3 ❙
   	// All of this stuff is only applicable to the real numbers, due to the usage of orders, addition etc. directly on elements of the
   		domain. Possibly can be generalized ❙
❚

theory SequenceConvergence : base:?Logic =
	include ?Sequences ❙

	prop_converges : {G: metricSpace} G^ω ⟶ G.universe ⟶ prop  ❘
		= [G,a,l] ∀[ε : ℝ+]∃[n : ℕ] ∀[m : ℕ] (m ≥ n) ⇒ (d (a m) l) < ε ❙
	prop_convergent : {G: metricSpace} G^ω ⟶ prop  ❘
		= [G,a] ∃![g] prop_converges G a g   ❙
            
	// isLimitSupremum : {G: metricSpace} G^ω ⟶ G.universe ⟶ prop  ❘
		// = [G,a,l] ∀[ε : ℝ+] (∀[N : ℕ] ∃[n : ℕ] (n ≥ N) ∧ (a n > l - ε)) ∧ (∃[N : ℕ] ∀[n : ℕ] (n ≥ N) ⇒ (a n < l + ε)) ❙
	// isLimitInfimum : {G: metricSpace} G^ω ⟶ G.universe ⟶ prop  ❘
		//  = [G,a,l] ∀[ε : ℝ+] (∀[N : ℕ] ∃[n : ℕ] (n ≥ N) ∧ (a n < l + ε)) ∧ (∃[N : ℕ] ∀[n : ℕ] (n ≥ N) ⇒ (a n > l - ε)) ❙
	// hasLimitSupremum : {G: metricSpace} G^ω ⟶ prop  ❘
		// = [G,a] ∃![g] isLimitSupremum G a g   ❙
	// hasLimitInfimum : {G: metricSpace} G^ω ⟶ prop  ❘
		// = [G,a] ∃![g] isLimitInfimum G a g    ❙
	// limitSupremum : {G : metricSpace, a : G^ω, p : ⊦ hasLimitSupremum G a} dom G ❘
		//   = [G, a, p] that (dom G) ([g] isLimitSupremum G a g) p ❘
		// # limsup 2 %I3 ❙
	// limitInfimum : {G : metricSpace, a : G^ω, p : ⊦ hasLimitInfimum G a} dom G ❘
		//  = [G, a, p] that (dom G) ([g] isLimitInfimum G a g) p ❘
		// # liminf 2 %I3 ❙
         
	prop_isLimit : {G: metricSpace} G^ω ⟶ G.universe ⟶ prop  ❘
		= [G,a,l] ∀[ε : ℝ+] ∀[N : ℕ] ∃[n : ℕ] (n ≥ N) ∧ ((d (a n) l) < ε) ❙
	prop_hasLimit : {G: metricSpace} G^ω ⟶ prop  ❘
		= [G,a] ∃![g] prop_isLimit G a g    ❙
	limit : {G : metricSpace, a : G^ω, p : ⊦ prop_convergent G a} G.universe ❘
		= [G, a, p] that (G.universe) ([g : G.universe] prop_converges G a g) p ❘
		# lim 2 %I3 ❙
❚
    	      
theory FunctionLimit : base:?Logic = 
   include ?MetricSpace ❙
   /T p is the limit of f at "point" a, where A is the larger space and is restricted by cond ❙
   /T *_c-variants: only on pred_as_subs, all the others on ℝ ❙
   prop_isLimit_c : {A : metricSpace,B: metricSpace, cond : A.universe ⟶ prop} ({x : A.universe,p:⊦ cond x}B.universe) ⟶ A.universe ⟶ B.universe ⟶ prop ❘
   		= [A,B,cond][f][a,l] ∀[ε:ℝ+] ε > 0 ⇒ ∃[δ : ℝ] δ > 0 ∧ ∀[x : A.universe] ∀[p : ⊦ cond x] (d x a) < δ ⇒ (d (f x p) l) < ε ❙
   prop_hasLimit_c : {A : metricSpace,B: metricSpace, cond : A.universe ⟶ prop} ({x : A.universe,p:⊦ cond x}B.universe) ⟶ A.universe ⟶ prop ❘
   		= [A,B,cond,f,a] ∃![l : B.universe] prop_isLimit_c A B cond f a l ❙
   prop_isLimit : {A : metricSpace,B: metricSpace} (A.universe ⟶ B.universe) ⟶ A.universe ⟶ B.universe ⟶ prop ❘
   		= [A,B,f,a,l] prop_isLimit_c A B ([x]true) ([x,p] f x) a l ❙
   prop_hasLimit : {A : metricSpace,B: metricSpace} (A.universe ⟶ B.universe) ⟶ A.universe ⟶ prop ❘
   		= [A,B,f,a] ∃![l : B.universe] prop_isLimit A B f a l❙
   limit_c : {A : metricSpace, B: metricSpace, cond : A.universe ⟶ prop, f : {x : A.universe,p:⊦ cond x}B.universe, a : A.universe, p : ⊦ prop_hasLimit_c A B cond f a} B.universe ❘
   		= [A,B,cond,f,a,p] that (B.universe) ([b:B.universe] prop_isLimit_c A B cond f a b) p ❙
   limit : {A : metricSpace, B: metricSpace, f : A.universe ⟶ B.universe, a : A.universe, p : ⊦ prop_hasLimit A B f a} B.universe ❘
   		= [A,B,f,a,p] that (B.universe) ([b] prop_isLimit A B f a b) p ❙
❚

theory Completeness : base:?Logic = 
   include ?MetricSpace ❙
   include ?SequenceConvergence ❙
   // d(x_k , x_l ) → 0 for k, l → ∞ ❙
   cauchy : {M: metricSpace} (ℕ ⟶ M.universe) ⟶ prop ❘ 
     = [M, seq] ∀[ε : ℝ+] ∀[N : ℕ] ∃[k : ℕ] ∃[l : ℕ] (k ≥ N) ∧ (l > k) ∧ ((d (seq k) (seq l)) < ε) ❘
     # cauchy 2 ❙
   // every Cauchy sequence in M converges ❙
   complete : {M: metricSpace} prop ❘
     = [M] ∀[seq] cauchy seq ⇒ prop_convergent M seq ❘ # complete 1 ❙
❚

// MiKo: maybe we should refactor the iterated operation construction into $?monoid$ with the axioms ❚
theory Series : base:?Logic =
  include ?SequenceConvergence ❙
  include ?MetricMonoid ❙
  
  partialSum : {G : metricMonoid} G^ω ⟶ ℕ ⟶ (G.universe) ❘ # parSum 2 3 ❙
  axiom_partialSumBase : {G : metricMonoid} ⊦ ∀[S : G^ω] parSum S 0 ≐ (G.unit) ❙
  axiom_partialSumStep : {G : metricMonoid} ⊦ ∀[S : G^ω] ∀[n] parSum S (succ_nat_lit n) ≐ (G.op) (parSum S n) (S (succ_nat_lit n)) ❙
  prop_convergent : {G : metricMonoid} G^ω ⟶ prop ❘ = [G][S] prop_convergent G ([n] parSum S n) ❙
  series : {G : metricMonoid, S: G^ω} dom G ❘ = [G,S] lim (partialSum G S) ❘ # SUM 2 ❙ 
❚