Corecursion

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

Statistics

Metric	Count
Definitions FriendlyOperation, FriendlyOperationClass, gcorec, instMetricSpaceSeq, instMetricSpaceStream'	5
Theorems comp, const, dist_le, exists_fixed_point, id, ite, comp, friend, dist_le_one, dist_cons_cons, dist_cons_cons_eq_one, dist_cons_nil, dist_eq_half_of_head, dist_eq_one_of_head, dist_eq_two_inv_pow, dist_le_one, dist_nil_cons, exists_fixed_point_of_contractible, gcorec_nil, gcorec_some, instBoundedSpaceSeq, instBoundedSpaceStream', instCompleteSpaceSeq, instCompleteSpaceStream'	24
Total	29

Tactic.ComputeAsymptotics.Seq

Definitions

Name	Category	Theorems
FriendlyOperation 📖	MathDef	3 math math: FriendlyOperation.const, FriendlyOperation.id, FriendlyOperationClass.friend
FriendlyOperationClass 📖	CompData	1 math math: FriendlyOperationClass.comp
gcorec 📖	CompOp	—
instMetricSpaceSeq 📖	CompOp	11 math math: dist_cons_nil, instBoundedSpaceSeq, dist_cons_cons_eq_one, dist_eq_one_of_head, dist_cons_cons, dist_eq_two_inv_pow, dist_nil_cons, instCompleteSpaceSeq, FriendlyOperation.dist_le, dist_eq_half_of_head, dist_le_one
instMetricSpaceStream' 📖	CompOp	3 math math: Stream'.dist_le_one, instCompleteSpaceStream', instBoundedSpaceStream'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_cons_cons 📖	mathematical	—	Dist.dist Stream'.Seq PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpaceSeq Stream'.Seq.cons Real Real.instMul Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat dist_self MulZeroClass.mul_zero Subtype.dist_eq PiNat.dist_eq_of_ne Subtype.coe_ne_coe one_div PiNat.firstDiff_def Mathlib.Tactic.Contrapose.contrapose₂ Subtype.val_injective Nat.find_comp_succ
dist_cons_cons_eq_one 📖	mathematical	—	Dist.dist Stream'.Seq PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpaceSeq Stream'.Seq.cons Real Real.instOne	—	dist_eq_one_of_head Stream'.Seq.head_cons
dist_cons_nil 📖	mathematical	—	Dist.dist Stream'.Seq PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpaceSeq Stream'.Seq.cons Stream'.Seq.nil Real Real.instOne	—	dist_eq_one_of_head Stream'.Seq.head_cons
dist_eq_half_of_head 📖	mathematical	Stream'.Seq.head	Dist.dist Stream'.Seq PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpaceSeq Real Real.instMul Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Stream'.Seq.tail	—	Nat.instAtLeastTwoHAddOfNat dist_self MulZeroClass.mul_zero Stream'.Seq.head_cons dist_cons_cons
dist_eq_one_of_head 📖	mathematical	—	Dist.dist Stream'.Seq PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpaceSeq Real Real.instOne	—	Subtype.dist_eq Nat.instAtLeastTwoHAddOfNat PiNat.dist_eq_of_ne Subtype.coe_ne_coe Mathlib.Tactic.Contrapose.contrapose₄ PiNat.firstDiff_def pow_zero
dist_eq_two_inv_pow 📖	mathematical	—	Dist.dist Stream'.Seq PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpaceSeq Real Monoid.toNatPow Real.instMonoid Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Subtype.dist_eq PiNat.dist_eq_of_ne Subtype.coe_ne_coe one_div inv_pow IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Real.instIsOrderedRing Real.instNontrivial IsStrictOrderedRing.toCharZero
dist_le_one 📖	mathematical	—	Real Real.instLE Dist.dist Stream'.Seq PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpaceSeq Real.instOne	—	PiNat.dist_le_one
dist_nil_cons 📖	mathematical	—	Dist.dist Stream'.Seq PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpaceSeq Stream'.Seq.nil Stream'.Seq.cons Real Real.instOne	—	dist_comm dist_cons_nil
exists_fixed_point_of_contractible 📖	mathematical	LipschitzWith UniformFun Stream'.Seq UniformFun.instPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace instMetricSpaceSeq NNReal NNReal.instInv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Nat.instAtLeastTwoHAddOfNat	Function.IsFixedPt	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.isNNRat_lt_true NNReal.instIsStrictOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one instBoundedSpaceSeq instNonemptyUniformFun UniformFun.instCompleteSpace instCompleteSpaceSeq ContractingWith.fixedPoint_isFixedPt
gcorec_nil 📖	mathematical	—	Stream'.Seq.nil	—	FriendlyOperation.exists_fixed_point
gcorec_some 📖	mathematical	—	Stream'.Seq.cons	—	FriendlyOperation.exists_fixed_point
instBoundedSpaceSeq 📖	mathematical	—	BoundedSpace Stream'.Seq PseudoMetricSpace.toBornology MetricSpace.toPseudoMetricSpace instMetricSpaceSeq	—	instBoundedSpaceSubtype instBoundedSpaceStream'
instBoundedSpaceStream' 📖	mathematical	—	BoundedSpace Stream' PseudoMetricSpace.toBornology MetricSpace.toPseudoMetricSpace instMetricSpaceStream'	—	PiNat.boundedSpace discreteTopology_bot
instCompleteSpaceSeq 📖	mathematical	—	CompleteSpace Stream'.Seq PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpaceSeq	—	isClosed_iff_clusterPt Nat.instAtLeastTwoHAddOfNat clusterPt_principal_iff Metric.ball_mem_nhds pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo PiNat.apply_eq_of_dist_lt le_refl IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd IsClosed.completeSpace_coe instCompleteSpaceStream'
instCompleteSpaceStream' 📖	mathematical	—	CompleteSpace Stream' PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpaceStream'	—	PiNat.completeSpace discreteTopology_bot

Tactic.ComputeAsymptotics.Seq.FriendlyOperation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	Tactic.ComputeAsymptotics.Seq.FriendlyOperation	Stream'.Seq	—	eq_1 mul_one LipschitzWith.comp
const 📖	mathematical	—	Tactic.ComputeAsymptotics.Seq.FriendlyOperation	—	dist_self one_mul
dist_le 📖	mathematical	Tactic.ComputeAsymptotics.Seq.FriendlyOperation	Real Real.instLE Dist.dist Stream'.Seq PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Tactic.ComputeAsymptotics.Seq.instMetricSpaceSeq	—	one_mul lipschitzWith_iff_dist_le_mul eq_1
exists_fixed_point 📖	mathematical	—	Stream'.Seq Stream'.Seq.nil Stream'.Seq.cons	—	Nat.instAtLeastTwoHAddOfNat Tactic.ComputeAsymptotics.Seq.instBoundedSpaceSeq lipschitzWith_iff_dist_le_mul UniformFun.dist_le mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt Mathlib.Meta.Positivity.nnreal_coe_pos inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat NNReal.instIsOrderedRing Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo dist_nonneg dist_self IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instNontrivial Tactic.ComputeAsymptotics.Seq.dist_cons_cons Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass.friend one_mul eq_1 le_ciSup Metric.boundedSpace_iff Tactic.ComputeAsymptotics.Seq.exists_fixed_point_of_contractible
id 📖	mathematical	—	Tactic.ComputeAsymptotics.Seq.FriendlyOperation Stream'.Seq	—	LipschitzWith.id
ite 📖	mathematical	Tactic.ComputeAsymptotics.Seq.FriendlyOperation	Stream'.Seq Stream'.Seq.head	—	eq_1 lipschitzWith_iff_dist_le_mul NNReal.coe_one Tactic.ComputeAsymptotics.Seq.dist_eq_one_of_head mul_one

Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass	—	—
friend 📖	mathematical	—	Tactic.ComputeAsymptotics.Seq.FriendlyOperation	—	—

Tactic.ComputeAsymptotics.Seq.Stream'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_le_one 📖	mathematical	—	Real Real.instLE Dist.dist Stream' PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Tactic.ComputeAsymptotics.Seq.instMetricSpaceStream' Real.instOne	—	dist_self Real.instZeroLEOneClass Nat.instAtLeastTwoHAddOfNat PiNat.dist_eq_of_ne pow_le_one₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing zero_le_one zero_le_two IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_le_one_of_le₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Mathlib.Meta.NormNum.isNat_le_true Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo

---

← Back to Index