Commit 20b587b3 authored by Dennis Müller's avatar Dennis Müller

removed old files

parent 4dd3a031
namespace http://mathhub.info/MitM/smglom/Lists ❚
import fnd http://mathhub.info/MitM/Foundation ❚
import top http://mathhub.info/MitM/interfaces ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
import sets http://mathhub.info/MitM/smglom/sets ❚
theory Lists : fnd:?Lists =
include fnd:?OptionType ❙
// include top:/Logic?SortedFull ❙
include sets:?relations ❙
include arith:?natarith ❙
include sets:?set ❙
include http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma ❙
nonempty_list : type → type ❘ = [A:type] ⟨ list A | ([x] ⊦ (x ≠ nil A))⟩  # nonempty_list 1 ❙
head: {A} list A → A ❘ # head 2 ❙
tail: {A} nonempty_list A → list A ❘ # tail 2 ❙
concat: {A} list A → list A → list A ❘ # concat 2 3 ❙
reverse: {A} list A → list A ❘ # reverse 2 ❙
length: {A} list A → ℕ ❘ # length 2 ❙
member: {A} A → list A → bool ❘ # member 2 3 ❙
nth: {A} list A → ℕ → A ❘ # nth 2 3 ❙
// remove an element from a list ❙
remove: {A} A → list A → list A ❘ # remove 2 3 ❙
// return the last element of a list; return a default value if the list is empty ❙
last: {A} list A → A → A ❘ # last 2 3 ❙
// remove the last element of a list; does not change an empty list ❙
remove_last: {A} list A → list A ❘ # remove_last 2 ❙
// count the occurrences of an element in a list ❙
count: {A} list A → A → ℕ ❘ # count 2 3 ❙
// concatenate a list of lists ❙
concat_list: {A} list (list A) → list A ❘ # concat_list 2 ❙
// apply a function to each element of a list and concatenate the output ❙
flat_map: {A,B} (A → (list B)) → list A → list B ❘ # flat_map 3 4 ❙
// the set of sequences of elts of y indexed by elts of x, sorted in lexicographic order;
as a set it is the same as the power set ❙
list_power: {A,B} list A → list B → list (list A × B) ❘ # list_power 3 4 ❙
// check whether there is an element of a list satisfying the boolean function ❙
exists: {A} (A → bool) → list A → bool ❘ # exists 2 3 ❙
// check whether all elements of list satisfy the boolean function ❙
forall: {A} (A → bool) → list A → bool ❘ # forall 2 3 ❙
// check whether all elements of two lists are pairwise related according to a relation ❙
forall2: {A,B} relation A B → list A → list B → bool ❘ # forall2 2 3 4 ❙
// check whether all possible ordered pairs of a list are related according to a relation ❙
forall_pairs: {A} relation A A → list A → bool ❘ # forall_pairs 2 3 ❙
// check whether the ordered pairs which have the frontal elements as the first components
of a list are related according to a relation ❙
forall_ordpairs: {A} relation A A → list A → bool ❘ # forall_ordpairs 2 3 ❙
// check whether certain element satisfying the boolean function exists in a list ❙
find: {A} (A → bool) → list A → Option A ❘ # find 2 3 ❙
// the list of elements satisfying the boolean function is the first component ❙
partition: {A} (A → bool) → list A → list A × list A ❘ # partition 2 3 ❙
// split a list of doubletons into a doubleton of lists ❙
split: {A,B} list (A × B) → list A × list B ❘ # split 3 ❙
// combine two lists into one ❙
combine: {A,B} list A → list B → list (A × B) ❘ # combine 3 4 ❙
// return a list of all possible pairs ❙
list_prod: {A,B} list A → list B → list (A × B) ❘ # list_prod 3 4 ❙
// use length as an order on lists ❙
shorter_than: {A} list A → list A → bool ❘ # shorter_than 2 3 ❙
// set inclusion on lists ❙
in: {A} list A → list A → bool ❘ # 2 in 3 ❙
// first n elements ❙
firstn: {A} ℕ → list A → list A ❘ # firstn 2 3 ❙
// complement of first_n ❙
skipn: {A} ℕ → list A → list A ❘ # skipn 2 3 ❙
// check whether there are duplicates in a list ❙
no_duplicates: {A} list A → bool ❘ # no_dup 2 ❙
// remove duplicates of existing elements ❙
remove_duplicates: {A} list A → list A ❘ # remove_dup 2 ❙
// generate a natural number sequence given a starting point (2) and length (3) ❙
nat_sequence: {A:type} ℕ → ℕ → list ℕ ❘ # nat_seq 2 3 ❙
list_comprehension: {A:type} (A → bool) → list A ❘ # list_comprehension 2 ❙
filter: {A:type} (A → bool) → list A → list A ❘ # filter 2 3 ❙
fold_right: {A:type,B:type} (A → B → B) → B → list A → B ❘ # fold_right 3 4 5 ❙
fold_left: {A:type,B:type} (A → B → B) → B → list A → B ❘ # fold_left 3 4 5 ❙
map: {A,B} (A → B) → list A → list B ❘ # map 3 4 ❙
//Weirdly, doesn't typecheck
//concat_def: {A} ⊦ ∀ [l:list A] ∀ [m:list A] (concat l m) ≐ (fold_left cons m l) ❙
filter_def: ⊦ {A} ∀ [l:list A] ∀ [p:A → bool] (filter p l) ≐ (list_comprehension ([a:A] ((p a) ∧ (member a l)))) ❙
fold_left_def: ⊦ {A:type,B:type} ∀ [f:A → B → B] ∀ [b:B] ∀ [l:list A] fold_left f b l ≐ fold_right f b (reverse l) ❙
map_def: ⊦ {A:type,B:type} ∀ [f:A → B] ∀ [l:list A] map f l ≐ (list_comprehension ([b:B] (forall ([a:A] f a ≐ b) l))) ❙
//The next line doesn't typecheck, looks like a bug in the definition of nil (getting same issue after replacing l with nil in concat_def)
map_def2: ⊦ {A:type,B:type} ∀ [f:A → B] ∀ [l:list A] map f l ≐ fold_left ([a:A,m:list B] ((f a) , m)) nil l ❙
exists_axiom: ⊦ {A} ∀ [l:list A] ∀ [p:A → bool] exists p l ≐ ¬ forall ([a:A] ¬ p a) l ❙
forall_axiom: ⊦ {A} ∀ [l:list A] ∀ [p:A → bool] forall p l ≐ ¬ exists ([a:A] ¬ p a) l ❙
theory finite_sequences : fnd:?Logic =
include sets:?relations ❙
include arith:?natarith ❙
include sets:?set ❙
//include top:?TypingJudgments ❙
first_nats: {n:ℕ} ⟨set ℕ | ([s] ⊦ ∀ [x:ℕ] inset ℕ x s ≐ lessthan x n)⟩ ❘ # upto 1 ❙
fin_seq: type → type ❘ # fseq 1 ❙
fseq_nil: type → type ❘ # fseq_nil 1 ❙
single: {A} A → fseq A ❘ # single 2 ❙
concat: {A} fseq A → fseq A → fseq A ❘ # fseq_concat 2 3 ❙
fseq_cons: {A} A → fseq A → fseq A ❘ = [A:type,a:A,seq:fseq A] fseq_concat (single a) seq ❘ # fseq_cons 2 3 ❙
term: {A} A → fseq A → bool ❘ # term 2 3 ❙
length: {A} fseq A → ℕ ❘ # fseq_length 2 ❙
take: {A} ℕ → fseq A → fseq A ❘ # take 2 3 ❙
indexset: {A} fseq A → set ℕ  = [A,s] upto (fseq_length s) ❘ # indexset 2 ❙
finite_set_sequence: {A} (set A) → fseq A ❘ # fset_seq 2 ❙
//index: {A:type,s:fseq A} ⟨ℕ | ([x] ⊦ inset ℕ x (upto (length s)))⟩ → A ❘ # index 2 3 ❙
head: {A} fseq A → A ❘ # head 2 ❙
tail: {A} fseq A → fseq A ❘ # tail 2 ❙
reverse: {A} fseq A → fseq A ❘ # reverse 2 ❙
filter: {A} (A → bool) → fseq A → fseq A ❘ # filter 2 3 ❙
fseq_fold_right: {A:type,B:type} (A → B → B) → B → fseq A → B ❘ # fseq_fold_right 3 4 5 ❙
fseq_fold_left: {A:type,B:type} (A → B → B) → B → fseq A → B ❘ # fseq_fold_left 3 4 5 ❙
map: {A,B} (A → B) → fseq A → fseq B ❘ # map 3 4 ❙
any: {A} fseq A → (A → bool) → bool ❘ # any 2 3 ❙
some: {A} fseq A → (A → bool) → bool ❘ # some 2 3 ❙
//This doen't work as we are making a claim about a type, thus the typechecker actually needs a proof
//of the statement, which wasn't given in a definition, thus can't be infered
//Therefore, typechecking fails. Only possible fix is in adapting the definition of fseq to some weird subtype
//Leaving this for documentation purpose
//
////For now, this should be removed as soon as the Functions_are_Relations lemma is in place
////This is not referenced to in alignments, but used in Lists/finite_sequences
//restriction_fct: {A,B} function A B → {C} function C B ❘ # 3 restrict_fct 4 ❙
//fin_seq_def: ⊦ {A:type} ∀ [seq:fseq A] ∃ [f:ℕ → A] seq ≐ f | ⟨ ℕ | ([x] ⊦ x in (upto (length seq)))⟩ ❙
theory lists_as_sequences : fnd:?Logic =
include ?Lists ❙
include ?finite_sequences ❙
//list_to_sequence: {A} list A → fseq A ❘ = [A,l] fold_left ([a,b] fseq_cons (single a) b) fseq_nil l ❘ # list_to_sequence 2 ❙
namespace http://cds.omdoc.org/examples 
import base http://cds.omdoc.org/urtheories
theory Tannakian(R: CommutativeRing) : base:?LF =
/T A BellRow is a sequence of elements that starts with one 
theory BellRow =
apply: ℕ → R
preserve_one : ⊦ apply 0 = R.one
linearlyRecursive : bool = sf"$apply$ is given by a linear recurrence relation"

/T A BellTable is a prime-indexed set of BellRows.
theory BellTable =
rows: prime → BellRow
/T It induces a multiplicative function by factoring the argument into prime powers multiplying the entries of the bell table.
apply: ℕ⁺ → R = [n] sf"factor $n$ into prime powers $p^e$ and multiply all values $rows(p)(e)$"
rational : bool = {p} ⊦ rows(p).linearlyRecursive

/T A multiplicative function is a monoid homomorphism from (N,⋅,1) except that multiplication is only preserved for coprime factors.
theory MultiplicativeFunction =
apply: ℕ⁺ → R
preserve_one: ⊦ apply 1 = R.one
preserve_times: ⊦ coprime p q → ⊦ apply (p⋅q) = (apply p) R.times (apply q)
/T A multiplicative function is uniquely determined by its values on prime powers, which are stored in its BellTable
bellTable = {' BellTable ; rows = [p] BellRow {apply = [e] apply (p ^ e) '}
rational : bool = bellTable.rational

/T Bell rows form a commutative ring
view BellRowRing : CommutativeRing =
universe = BellRow
plus = sf"Cauchy product"
zero = sf"the function that returns $0$ everywhere except for the unit"
minus = sf"Cauchy inverse"
product = sf"tensor product"
one = sf"the constant function $1$"

/T Tannakian symbols are finitely-supported maps $R → ℤ$, but it's more convenient to represent them as lists of pairs
theory TannakianSymbol =
pairs: List R * ℤ
apply: R → ℤ = [r] sum (pairs filter [p] p.1 = r)
normal: bool  = [x] sf"no ring elements occurs twice in $pairs$"
upstairs = sf"the multiset of all ring elements that occur with positive multiplicity"
downstairs = sf"the multiset of all ring elements that occur with negative multiplicity"
trace : R  = pairs map [p] p.1 R.times R.embed(p.2)

/T up to a straightforward normalization, Tannakian symbols form a commutative ring
theory TannakianSymbolRing =
normalize : TannakianSymbol → TannakianSymbol = [x] sf"merge all pairs for the same ring element by summing the multiplicities"
universe = TannakianSymbol
zero = List()
zero_apply: {r} ⊦ zero(r) = 0
plus = concat # 1 ⊕ 2
plus_apply: {x,y,r} (x⊕y)(r) = x(r)+y(r)-
minus = [x] x map [p] (p.1, -p.2) # ⊖ 1
minus_apply: {x,r} (⊖x)(r) = -x(r)
times = [x,y] x flatMap [p] p map [q] (p.1 R.times q.1 , p.2 ⋅ q.2) # 1 ⊗ 2
times_apply: {x,y,r} (x⊗y)(r) = sf"sum of $x(a)⋅y(b)$ for all $a R.times b = r$
one = List((R.one,1))
one_apply: {r} one(r) = if (r = R.one) 1 else 0
/T actually, the axioms only hold up to normalization
realize CommutativeRing
embed : ℤ → TannakianSymbol = [z] = List((M.one, z))
/T flipping upstairs and downstairs
flip: TannakianSymbol → TannakianSymbol  = [x] x map [p] (R.minus p.1, p.2)
/T additionaly unary operations that could be defined now: λ^k, ψ^k, σ^k
lambda : ℕ → TannakianSymbol → TannakianSymbol  # λ 1 2

/T Tannakian symbols are isomorphic to rational Bell rows; this is a homomorphism of (at least) commutative rings 
correspondingBellRow : TannakianSymbol → BellRow
= [x] BellRow {
apply: [e] trace (λ k (flip(⊖ x)))
}
/T alternatively, we could compute the BellRow from its generating function, which is obtained as the product of $product x.pairs map [p] (1-p.1⋅T)^(-p.2)$

\ No newline at end of file
namespace http://mathhub.info/MitM/smglom/algebra ❚
import base http://mathhub.info/MitM/Foundation ❚
import sets http://mathhub.info/MitM/smglom/sets ❚
import type http://mathhub.info/MitM/interfaces/TypeConstructors ❚
theory category : base:?Logic =
theory category_theory : base:?Logic =
include sets:?setstruct/setstruct_theory ❙
hom : U → U → type ❘ # hom 1 2 ❙
comp : {a,b,c:U} hom a b → hom b c → hom a c ❘ # 4 ∘ 5 ❙
id: {a:U} hom a a ❘ # id %I1 ❙
Axiom_assoc : {a,b,c,d:U} ⊦ ∀[f:hom a b] ∀[g:hom b c] ∀[h:hom c d] f ∘ (g ∘ h) ≐ (f ∘ g) ∘ h ❙
Axiom_id_r : {x:U,a:U} ⊦ ∀[f:hom a x] f ∘ id ≐ f ❙
Axiom_id_l : {x:U,a:U} ⊦ ∀[f:hom x a] id ∘ f ≐ f ❙
include sets:?setstruct ❙
category = ModelsOf category_theory ❙
objects : category → type ❘ = [𝒞] dom 𝒞 ❘ # | 1 | ❙
morphisms : {𝒞:category} |𝒞| → |𝒞| → type ❘ = [𝒞,a,b] (𝒞.hom) a b ❘ # Hom 2 3 ❙
composition : {𝒞:category,a,b,c:|𝒞|} Hom a b → Hom b c → Hom a c ❘ = [𝒞,a,b,c,f,g] (𝒞.comp) a b c f g ❘ # 6 ∘ 5 ❙
id: {𝒞:category,a:|𝒞|} Hom a a ❘ # id 2 ❙
theory functor : base:?Logic =
include ?category ❙
functor : category → category → type❘ # 1 ⟹ 2 ❙
object : {𝒞,𝒟:category} 𝒞 ⟹ 𝒟 → |𝒞| → |𝒟| ❘ # 3 of 4 ❙
morph : {𝒞,𝒟:category} {F:𝒞 ⟹ 𝒟} {a: |𝒞|, b: |𝒞|} Hom a b → Hom (F of a) (F of b)  # 3 mf 6 ❙
func_id : {𝒞:category} {F:𝒞 ⟹ 𝒞} {a: |𝒞|} ⊦ (F mf (id a)) ≐ (id (F of a)) ❙
func_comp : {𝒞, 𝒟:category} {F:𝒞 ⟹ 𝒟} {a , b, c: |𝒞|, f: Hom a b, g: Hom b c} ⊦ F mf (g ∘ f) ≐ (F mf g) ∘ (F mf f) ❙
functor_composition: {𝒞1, 𝒞2, 𝒞3:category} 𝒞1 ⟹ 𝒞2 → 𝒞2 ⟹ 𝒞3 → 𝒞1 ⟹ 𝒞3 ❘ # 4 ∘ 5 ❙
identity_functor: {𝒞} 𝒞 ⟹ 𝒞 ❘ # id 1 ❙
namespace http://mathhub.info/MitM/smglom/combinatorics ❚
import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
theory binomial : base:?Logic =
include arith:?naturalnumbers ❙
binomial_coefficient: ℕ → ℕ → ℕ ❘ # 1 choose 2 ❙
namespace http://mathhub.info/MitM/smglom/misc ❚
import fnd http://mathhub.info/MitM/Foundation ❚
theory comparison : fnd:?Logic =
comparison : type ❘ # comparison ❙
greater_than : comparison ❘ # gt ❙
equal : comparison ❘ # eq ❙
less_than : comparison ❘ # lt ❙
opposite : comparison → comparison ❘ # opposite 1 ❙
theory option : fnd:?Logic =
option : type → type ❘ # option 1 ❙
some : {A} A → option A ❘ # some 2 ❙
none : {A} option A ❘ # none ❙
// none A is mapped to none B; some A a is mapped to some B (f a) ❙
option_map : {A,B} (A → B) → option A → option B ❘ # option_map 3 4 ❙
theory disjoint_sum : fnd:?Logic =
disjoint_sum : type → type → type ❘ # 1 + 2 ❙
inj1 : {A,B} A → A + B ❘ # inj1 3 ❙
inj2 : {A,B} B → A + B ❘ # inj2 3 ❙
// a sample interface for product type; feel free to remove or edit this ❚
theory product : fnd:?Logic =
include fnd:?NatLiterals ❙
product : type → type → type ❘ # 1 × 2 ❙
proj1 : {A,B} A × B → A ❘ # proj1 3 ❙
proj2 : {A,B} A × B → B ❘ # proj2 3 ❙
prod_curry : {A,B,C : type} (A → B → C) → (A × B) → C ❘ # curry 4 5 ❙
prod_uncurry : {A,B,C : type} (A × B → C) → A → B → C ❘ # uncurry 4 5 6 ❙
power : ℕ → type → type ❘ # 2 ^ 1 ❙
namespace http://mathhub.info/MitM/smglom/probability ❚
import base http://mathhub.info/MitM/Foundation ❚
// import sub http://gl.mathhub.info/MMT/LFX/Subtyping ❚
theory ProbabilityMeasure : base:?Logic =
include measures?Measure ❙
theory probabilityMeasure_theory : base:?Logic > X : type , A : sigmaAlgebra X ❘ =
include measures?Measure/measure_theory (X,A) ❙
axiom_fullsetisone : ⊦ μ (elem (A.coll) (fullset X)) ≐ 1 ❙
probabilityMeasure = [X : type, A : sigmaAlgebra X] Mod `?ProbabilityMeasure/probabilityMeasure_theory , X , A ❙
probabilitySpace = {'
universe : type ,
sigma_algebra : sigmaAlgebra universe ,
measure : probabilityMeasure universe sigma_algebra
'} ❙
theory ProbabilitySpaceTheorems : base:?Logic =
include ?ProbabilityMeasure ❙
include calculus?LebesgueIntegral ❙
include measures?Measurable ❙
include measures?LebesgueMeasurable ❙
theory probabilitySpaceTheorems_theory : base:?Logic > PS : probabilitySpace ❘ =
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) ❙
// eventsSigmaAlgebra = (PS.sigma_algebra) ❙
// probabilityMeasure : measure Ω (eventsSigmaAlgebra) ❙
// expectation : Ω ⟶ ⊦ quasiIntegrable ⟶ ℝ ❙
// 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) ⟩ ❙
isRealValuedRandomVariable : ((PS.universe) ⟶ ℝ) ⟶ bool ❘// = [f] ❙
realValuedRandomVariable = ⟨ f: ((PS.universe) ⟶ ℝ) | ⊦ isRealValuedRandomVariable f ⟩ ❘# ℝRv ❙
// theorems ❙
// lemma_probabilityLe1 : ⊦ ∀[x : set Ω] probability x ≤ 1 ❙
lemma_omegaNotEmpty : ⊦ fullset Ω ≠ ∅ ❙
// lemma_probabilityGe1Eq1 : {x : set Ω} ⊦ 1 ≤ probability x ⟶ ⊦ probability x ≐ 1 ❙
namespace http://mathhub.info/MitM/smglom/probability ❚
import base http://mathhub.info/MitM/Foundation ❚
import sets http://mathhub.info/MitM/smglom/typedsets ❚
import calc http://mathhub.info/MitM/smglom/calculus ❚ // for seqeuences and intervals ❚
import mes http://mathhub.info/MitM/smglom/measures ❚
// theory Vitali : base:?Logic =
include sets:?AllSets ❙
include seqs:?Sequences ❙
vitaliSet : set ℕ❙
namespace http://mathhub.info/MitM/smglom/probability ❚
import base http://mathhub.info/MitM/Foundation ❚
import sets http://mathhub.info/MitM/smglom/typedsets ❚
import calc http://mathhub.info/MitM/smglom/calculus ❚ // for seqeuences and intervals ❚
import mes http://mathhub.info/MitM/smglom/measures ❚
theory VitaliCoinToss : base:?Logic =
// a version of the vitali theorem from Hans-Otto Georgii's "Stochastik" ❙
include sets:?AllSets ❙
include calc:?Sequences ❙
include base:?DescriptionOperator ❙
include calc:?Intervals ❙
include mes:?SigmaAdditive ❙
vitaliSet : set (sequence ℕ) ❘= ⟪ (fullset (ℕ ⟶ ℕ)) | ([f] ∀[i] f i ≐ 0 ∨ f i ≐ 1) ⟫ ❙
vitaliPowerSet : collection (sequence ℕ) ❘= ℘ vitaliSet ❙
flipOneZero : ℕ ⟶ ℕ ❘= [n] (if (n ≐ 1) then 0 else (if (n ≐ 0) then (1 : ℕ) else n))❙
flipAt : ℕ ⟶ (sequence ℕ) ⟶ (sequence ℕ) ❘= [n , oldSeq] [i : ℕ] (if (i ≐ n) then (flipOneZero (oldSeq i)) else (oldSeq i)) ❙
vitaliPowerSetType : type ❘= setastype (vitaliPowerSet)❙
invariancy : (vitaliPowerSetType ⟶ ℝ) ⟶ bool ❘ = [P] ∀[A ] ∀[n : ℕ] A ⊑ vitaliSet ⇒
P (elem vitaliPowerSet A) ≐ P (elem vitaliPowerSet (im (flipAt n) A))❙
vitaliTheorem :
⊦ (¬ (∃[P : vitaliPowerSetType ⟶ ℝ]
(∀[x : vitaliPowerSetType] P x ≤ 1 ∧ 0 ≤ P x) ∧ P (vitaliSet) ≐ 1 ∧ prop_sigmaAdditive vitaliPowerSet P) ∧ invariancy P) ❙
\ No newline at end of file
namespace http://mathhub.info/MitM/smglom ❚
import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
import alg http://mathhub.info/MitM/smglom/algebra ❚
theory MultiplicativeFunctions : base:?Logic =
include arith:?NaturalArithmetics ❙
include alg:?Ring ❙ // Commutative! ❙
// TODO ❙ gcd : ℕ ⟶ ℕ ⟶ ℕ ❙
// TODO ❙ coprime : ℕ ⟶ ℕ ⟶ bool ❘ = [m,n] gcd m n ≐ 1 ❙
isMultiplicative : {R : ring} (ℕ+ ⟶ (R.universe)) ⟶ bool ❘// = [R, f] (f 1 ≐ (R.one)) ∧
∀ [m : ℕ+] ∀ [n : ℕ+] (coprime m n) ⇒ (f (m ⋅ n) ≐ (R.times) (f m) (f n) ) ❙
multiplicativeFunctions : ring ⟶ type ❘ = [R : ring] ⟨ (ℕ+ ⟶ (R.universe)) | ([f] ⊦ isMultiplicative R f) ⟩ ❘ # Mult 1 ❙
bellRow : {R : ring} type ❘ = [R] ⟨ (ℕ ⟶ (R.universe)) | ([f] ⊦ f 0 ≐ (R.one)) ⟩ ❙
bellRowMap : {R : ring} Mult R ⟶ primes ⟶ bellRow R ❘
// = [R,f,p] ([n] f (p ^ n)) ❘ # bellRowM 2 3 ❙
// A sequence b_i is linearly recursive if ∃ [k,N,c_1,...,c_k] ∀ [n] n > N ⇒ b_n= c_1 b_n-1...c_k b_n-k,
the c_i may be from a larger ring than R ❙
// in certain cases this is equivalent to the generating function of b being rational over R❙
linearRecursive : {R : ring} bellRow R ⟶ bool ❘ # linRec 2 ❙
rationalMultiplicative : {R : ring} Mult R ⟶ bool ❘
= [R,f] ∀ [p : primes] linRec (bellRowM f p) ❙
theory TannakianSymbols : base:?Logic =
include alg:?Monoid ❙ // abelian ❙
include arith:?IntegerArithmetics ❙
isTannakianSymbol : {M : monoid} ((M.universe) ⟶ ℤ) ⟶ bool ❙ // = f is zero almost everywhere ❙
tannakianSymbols : {M : monoid} type ❘ = [M] ⟨ ((M.universe) ⟶ ℤ) | ([f] ⊦ isTannakianSymbol M f) ⟩ ❘ # TS 1 ❙
include base:?ProductType ❙
include base:?Lists ❙
tSasList : {M : monoid} TS M ⟶ list ((M.universe) × ℤ) ❘ # ls 2 ❙
plusTS : {M : monoid} TS M ⟶ TS M ⟶ TS M ❘ // = [M] [f,g] [a] (f a) + (g a) ❘ # 2 ⊕ 3 ❙
timesTS : {M : monoid} TS M ⟶ TS M ⟶ TS M ❘ // = [M] [f,g] [a] sum_{xy=a} (f x) ⋅ (g y) ❘ # 2 ⊗ 3 ❙
psiTS : {M : monoid} ℕ+ ⟶ TS M ⟶ TS M ❘ // = [M] [k,X] ([n] sum_{a| a^k=n} X a) ❘ # ψ 2 3 ❙
lambdaTS : {M : monoid} ℕ+ ⟶ TS M ⟶ TS M ❘ // = ??? ❘ # λ 2 3 ❙
gammaTS : {M : monoid} ℕ+ ⟶ TS M ⟶ TS M ❘ // = ??? ❘ # γ 2 3 ❙
sigmaTS : {M : monoid} ℕ+ ⟶ TS M ⟶ TS M ❘ // = ??? ❘ # σ 2 3 ❙
epsilonTS : {M : monoid} TS M ⟶ TS M ❘ // = ??? ❘ # ε 2 ❙
include ?MultiplicativeFunctions ❙
tannakianSymbolsRing : {R : ring} type ❘ = [R] tannakianSymbols (multiplicative_monoid R) ❘ # TSr 1 ❙
trace : {R : ring} TSr R ⟶ (R.universe) ❘ // = [R,X] sum_{r : support of X} X(r) ⋅ r ❘ # tr 2 ❙
tsConstructor : {M : monoid} list (M.universe) ⟶ list (M.universe) ⟶ TS M ❘ # 2 ts 3 ❙
tsDestructorU : {M : monoid} TS M ⟶ list (M.universe) ❘ # up 2 ❙
tsDestructorD : {M : monoid} TS M ⟶ list (M.universe) ❘ # down 2 ❙
// TODO make Ring -> Monoid implicit or smth ❙
correspondingSequence : {R : ring} TSr R ⟶ bellRow R ❘
= [R,X] [k] lambdaTS (multiplicative_monoid R) k (plusTS (multiplicative_monoid R) X (tsConstructor (multiplicative_monoid R) (nil (R.universe)) (cons (R.universe) ((R.minus) (R.one)) (nil (R.universe))) ) )❙
\ 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