Defs

📁 Source: Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean

Statistics

Metric	Count
Definitions MultiseriesExpansion, Multiseries, cons, corec, destruct, head, instInhabited, instMembershipProdReal, map, nil, recOn, tail, toSeq, instInhabited, mk, ofReal, recOn, replaceFun, seq, toFun, toReal	21
Theorems Pairwise_cons_nil, Pairwise_nil, cons_eq_cons, cons_ne_nil, corec_cons, corec_nil, destruct_cons, destruct_eq_cons, destruct_eq_none, destruct_nil, eq_of_bisim, eq_of_bisim_strong, head_cons, head_nil, map_comp, map_cons, map_id, map_nil, mem_cons_iff, nil_ne_cons, notMem_nil, tail_cons, tail_nil, const_toFun, eq_mk, ext_iff, mk_eq_mk_iff, mk_eq_mk_iff_iff, mk_replaceFun, mk_seq, mk_toFun, ms_eq_mk_iff, replaceFun_seq, replaceFun_toFun	34
Total	55

ComputeAsymptotics

Definitions

Name	Category	Theorems
MultiseriesExpansion 📖	CompOp	9 math math: MultiseriesExpansion.Multiseries.destruct_cons, MultiseriesExpansion.Multiseries.mem_cons_iff, MultiseriesExpansion.Multiseries.head_nil, MultiseriesExpansion.Multiseries.Pairwise_nil, MultiseriesExpansion.Multiseries.map_comp, MultiseriesExpansion.Multiseries.destruct_nil, MultiseriesExpansion.Multiseries.Pairwise_cons_nil, MultiseriesExpansion.Multiseries.notMem_nil, MultiseriesExpansion.Multiseries.head_cons

ComputeAsymptotics.MultiseriesExpansion

Definitions

Name	Category	Theorems
Multiseries 📖	CompOp	4 math math: Multiseries.destruct_cons, Multiseries.mem_cons_iff, Multiseries.destruct_nil, Multiseries.notMem_nil
instInhabited 📖	CompOp	—
mk 📖	CompOp	—
ofReal 📖	CompOp	—
recOn 📖	CompOp	—
replaceFun 📖	CompOp	3 math math: replaceFun_seq, replaceFun_toFun, mk_replaceFun
seq 📖	CompOp	6 math math: mk_seq, eq_mk, replaceFun_seq, ext_iff, ms_eq_mk_iff, mk_eq_mk_iff_iff
toFun 📖	CompOp	7 math math: eq_mk, replaceFun_toFun, ext_iff, ms_eq_mk_iff, mk_eq_mk_iff_iff, mk_toFun, const_toFun
toReal 📖	CompOp	1 math math: const_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_toFun 📖	mathematical	—	toFun toReal	—	—
eq_mk 📖	mathematical	—	seq toFun	—	—
ext_iff 📖	mathematical	—	seq toFun	—	—
mk_eq_mk_iff 📖	—	—	—	—	—
mk_eq_mk_iff_iff 📖	mathematical	—	seq toFun	—	ms_eq_mk_iff
mk_replaceFun 📖	mathematical	—	replaceFun	—	—
mk_seq 📖	mathematical	—	seq	—	—
mk_toFun 📖	mathematical	—	toFun	—	—
ms_eq_mk_iff 📖	mathematical	—	seq toFun	—	mk_eq_mk_iff
replaceFun_seq 📖	mathematical	—	seq replaceFun	—	—
replaceFun_toFun 📖	mathematical	—	toFun replaceFun	—	—

ComputeAsymptotics.MultiseriesExpansion.Multiseries

Definitions

Name	Category	Theorems
cons 📖	CompOp	9 math math: destruct_cons, mem_cons_iff, map_cons, cons_eq_cons, destruct_eq_cons, Pairwise_cons_nil, corec_cons, tail_cons, head_cons
corec 📖	CompOp	—
destruct 📖	CompOp	2 math math: destruct_cons, destruct_nil
head 📖	CompOp	2 math math: head_nil, head_cons
instInhabited 📖	CompOp	—
instMembershipProdReal 📖	CompOp	2 math math: mem_cons_iff, notMem_nil
map 📖	CompOp	4 math math: map_cons, map_comp, map_nil, map_id
nil 📖	CompOp	9 math math: tail_nil, head_nil, Pairwise_nil, destruct_nil, corec_nil, Pairwise_cons_nil, map_nil, destruct_eq_none, notMem_nil
recOn 📖	CompOp	—
tail 📖	CompOp	2 math math: tail_nil, tail_cons
toSeq 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Pairwise_cons_nil 📖	mathematical	—	Stream'.Seq.Pairwise Real ComputeAsymptotics.MultiseriesExpansion cons nil	—	—
Pairwise_nil 📖	mathematical	—	Stream'.Seq.Pairwise Real ComputeAsymptotics.MultiseriesExpansion nil	—	—
cons_eq_cons 📖	mathematical	—	cons	—	cons.eq_1 Stream'.Seq.cons_eq_cons
cons_ne_nil 📖	—	—	—	—	Stream'.Seq.cons_ne_nil
corec_cons 📖	mathematical	Real ComputeAsymptotics.MultiseriesExpansion	cons	—	Stream'.Seq.corec_cons
corec_nil 📖	mathematical	Real ComputeAsymptotics.MultiseriesExpansion	nil	—	Stream'.Seq.corec_nil
destruct_cons 📖	mathematical	—	destruct cons Real ComputeAsymptotics.MultiseriesExpansion ComputeAsymptotics.MultiseriesExpansion.Multiseries	—	Stream'.Seq.destruct_cons
destruct_eq_cons 📖	mathematical	destruct Real ComputeAsymptotics.MultiseriesExpansion ComputeAsymptotics.MultiseriesExpansion.Multiseries	cons	—	Stream'.Seq.destruct_eq_cons
destruct_eq_none 📖	mathematical	destruct Real ComputeAsymptotics.MultiseriesExpansion ComputeAsymptotics.MultiseriesExpansion.Multiseries	nil	—	Stream'.Seq.destruct_eq_none
destruct_nil 📖	mathematical	—	destruct nil Real ComputeAsymptotics.MultiseriesExpansion ComputeAsymptotics.MultiseriesExpansion.Multiseries	—	—
eq_of_bisim 📖	—	nil Real ComputeAsymptotics.MultiseriesExpansion ComputeAsymptotics.MultiseriesExpansion.Multiseries cons	—	—	Stream'.Seq.eq_of_bisim'
eq_of_bisim_strong 📖	—	Real ComputeAsymptotics.MultiseriesExpansion ComputeAsymptotics.MultiseriesExpansion.Multiseries cons	—	—	Stream'.Seq.eq_of_bisim_strong
head_cons 📖	mathematical	—	head cons Real ComputeAsymptotics.MultiseriesExpansion	—	Stream'.Seq.head_cons
head_nil 📖	mathematical	—	head nil Real ComputeAsymptotics.MultiseriesExpansion	—	—
map_comp 📖	mathematical	—	map Real ComputeAsymptotics.MultiseriesExpansion	—	—
map_cons 📖	mathematical	—	map cons	—	Stream'.Seq.map_cons
map_id 📖	mathematical	—	map	—	Stream'.Seq.map_id
map_nil 📖	mathematical	—	map nil	—	—
mem_cons_iff 📖	mathematical	—	Real ComputeAsymptotics.MultiseriesExpansion ComputeAsymptotics.MultiseriesExpansion.Multiseries instMembershipProdReal cons	—	Stream'.Seq.mem_cons_iff
nil_ne_cons 📖	—	—	—	—	cons_ne_nil
notMem_nil 📖	mathematical	—	Real ComputeAsymptotics.MultiseriesExpansion ComputeAsymptotics.MultiseriesExpansion.Multiseries instMembershipProdReal nil	—	Stream'.Seq.notMem_nil
tail_cons 📖	mathematical	—	tail cons	—	—
tail_nil 📖	mathematical	—	tail nil	—	—

---

← Back to Index