Contracting

📁 Source: Mathlib/Topology/MetricSpace/Contracting.lean

Statistics

Metric	Count
Definitions ContractingWith, efixedPoint, efixedPoint', fixedPoint	4
Theorems aposteriori_dist_iterate_fixedPoint_le, apriori_dist_iterate_fixedPoint_le, apriori_edist_iterate_efixedPoint_le, apriori_edist_iterate_efixedPoint_le', dist_fixedPoint_fixedPoint_of_dist_le', dist_fixedPoint_le, dist_inequality, dist_le_mul, dist_le_of_fixedPoint, edist_efixedPoint_le, edist_efixedPoint_le', edist_efixedPoint_lt_top, edist_efixedPoint_lt_top', edist_inequality, edist_le_of_fixedPoint, efixedPoint_eq_of_edist_lt_top, efixedPoint_eq_of_edist_lt_top', efixedPoint_isFixedPt, efixedPoint_isFixedPt', efixedPoint_mem', eq_or_edist_eq_top_of_fixedPoints, exists_fixedPoint, exists_fixedPoint', fixedPoint_isFixedPt, fixedPoint_lipschitz_in_map, fixedPoint_unique, fixedPoint_unique', isFixedPt_fixedPoint_iterate, one_sub_K_ne_top, one_sub_K_ne_zero, one_sub_K_pos, one_sub_K_pos', restrict, tendsto_iterate_efixedPoint, tendsto_iterate_efixedPoint', tendsto_iterate_fixedPoint, toLipschitzWith	37
Total	41

ContractingWith

Definitions

Name	Category	Theorems
efixedPoint 📖	CompOp	6 math math: efixedPoint_eq_of_edist_lt_top, tendsto_iterate_efixedPoint, edist_efixedPoint_lt_top, efixedPoint_isFixedPt, apriori_edist_iterate_efixedPoint_le, edist_efixedPoint_le
efixedPoint' 📖	CompOp	7 math math: apriori_edist_iterate_efixedPoint_le', efixedPoint_eq_of_edist_lt_top', edist_efixedPoint_lt_top', edist_efixedPoint_le', efixedPoint_mem', efixedPoint_isFixedPt', tendsto_iterate_efixedPoint'
fixedPoint 📖	CompOp	8 math math: dist_fixedPoint_le, aposteriori_dist_iterate_fixedPoint_le, apriori_dist_iterate_fixedPoint_le, tendsto_iterate_fixedPoint, fixedPoint_unique, fixedPoint_lipschitz_in_map, fixedPoint_isFixedPt, isFixedPt_fixedPoint_iterate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aposteriori_dist_iterate_fixedPoint_le 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace	Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Nat.iterate fixedPoint DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instOne NNReal.toReal	—	Function.iterate_succ' dist_fixedPoint_le
apriori_dist_iterate_fixedPoint_le 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace	Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Nat.iterate fixedPoint DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Monoid.toNatPow Real.instMonoid NNReal.toReal Real.instSub Real.instOne	—	aposteriori_dist_iterate_fixedPoint_le div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing LipschitzWith.dist_iterate_succ_le_geometric toLipschitzWith LT.lt.le one_sub_K_pos
apriori_edist_iterate_efixedPoint_le 📖	mathematical	ContractingWith	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace Nat.iterate efixedPoint DivInvMonoid.toDiv ENNReal.instDivInvMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ENNReal.ofNNReal ENNReal.instSub AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	exists_fixedPoint
apriori_edist_iterate_efixedPoint_le' 📖	mathematical	IsComplete PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace Set.MapsTo ContractingWith Set.Elem instEMetricSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist Nat.iterate efixedPoint' DivInvMonoid.toDiv ENNReal.instDivInvMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ENNReal.ofNNReal ENNReal.instSub AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	exists_fixedPoint'
dist_fixedPoint_fixedPoint_of_dist_le' 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace Function.IsFixedPt Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instOne NNReal.toReal	—	dist_comm dist_le_of_fixedPoint Function.IsFixedPt.eq div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing one_sub_K_pos
dist_fixedPoint_le 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace	Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace fixedPoint DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instOne NNReal.toReal	—	dist_le_of_fixedPoint fixedPoint_isFixedPt
dist_inequality 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace	Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd Real.instSub Real.instOne NNReal.toReal	—	dist_triangle4_right le_imp_le_of_le_of_le add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid dist_le_mul le_refl le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing one_sub_K_pos mul_comm sub_mul one_mul sub_le_iff_le_add covariant_swap_add_of_covariant_add
dist_le_mul 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace	Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Real.instMul NNReal.toReal	—	LipschitzWith.dist_le_mul toLipschitzWith
dist_le_of_fixedPoint 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace Function.IsFixedPt	Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instOne NNReal.toReal	—	Function.IsFixedPt.eq dist_self add_zero dist_inequality
edist_efixedPoint_le 📖	mathematical	ContractingWith	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace efixedPoint DivInvMonoid.toDiv ENNReal.instDivInvMonoid ENNReal.instSub AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal ENNReal.ofNNReal	—	pow_zero mul_one apriori_edist_iterate_efixedPoint_le
edist_efixedPoint_le' 📖	mathematical	IsComplete PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace Set.MapsTo ContractingWith Set.Elem instEMetricSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist efixedPoint' DivInvMonoid.toDiv ENNReal.instDivInvMonoid ENNReal.instSub AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal ENNReal.ofNNReal	—	pow_zero mul_one apriori_edist_iterate_efixedPoint_le'
edist_efixedPoint_lt_top 📖	mathematical	ContractingWith	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace efixedPoint Top.top instTopENNReal	—	LE.le.trans_lt edist_efixedPoint_le Ne.lt_top ENNReal.mul_ne_top ENNReal.inv_ne_top one_sub_K_ne_zero
edist_efixedPoint_lt_top' 📖	mathematical	IsComplete PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace Set.MapsTo ContractingWith Set.Elem instEMetricSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist efixedPoint' Top.top instTopENNReal	—	LE.le.trans_lt edist_efixedPoint_le' Ne.lt_top ENNReal.mul_ne_top ENNReal.inv_ne_top one_sub_K_ne_zero
edist_inequality 📖	mathematical	ContractingWith	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace DivInvMonoid.toDiv ENNReal.instDivInvMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instSub AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal ENNReal.ofNNReal	—	edist_triangle4 PseudoEMetricSpace.edist_comm add_right_comm add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_rfl ENNReal.le_div_iff_mul_le one_sub_K_ne_zero one_sub_K_ne_top mul_comm ENNReal.sub_mul one_mul tsub_le_iff_right ENNReal.instOrderedSub
edist_le_of_fixedPoint 📖	mathematical	ContractingWith Function.IsFixedPt	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace DivInvMonoid.toDiv ENNReal.instDivInvMonoid ENNReal.instSub AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal ENNReal.ofNNReal	—	Function.IsFixedPt.eq PseudoEMetricSpace.edist_self add_zero edist_inequality
efixedPoint_eq_of_edist_lt_top 📖	mathematical	ContractingWith	efixedPoint	—	eq_or_edist_eq_top_of_fixedPoints efixedPoint_isFixedPt ne_of_lt Setoid.trans' Setoid.symm' edist_efixedPoint_lt_top lt_top_iff_ne_top
efixedPoint_eq_of_edist_lt_top' 📖	mathematical	ContractingWith IsComplete PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace Set.MapsTo Set.Elem instEMetricSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	efixedPoint'	—	eq_or_edist_eq_top_of_fixedPoints efixedPoint_isFixedPt' ne_of_lt Setoid.trans' Setoid.symm' edist_efixedPoint_lt_top' lt_top_iff_ne_top
efixedPoint_isFixedPt 📖	mathematical	ContractingWith	Function.IsFixedPt efixedPoint	—	exists_fixedPoint
efixedPoint_isFixedPt' 📖	mathematical	IsComplete PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace Set.MapsTo ContractingWith Set.Elem instEMetricSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	Function.IsFixedPt efixedPoint'	—	exists_fixedPoint'
efixedPoint_mem' 📖	mathematical	IsComplete PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace Set.MapsTo ContractingWith Set.Elem instEMetricSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	efixedPoint'	—	exists_fixedPoint'
eq_or_edist_eq_top_of_fixedPoints 📖	mathematical	ContractingWith Function.IsFixedPt	EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace Top.top ENNReal instTopENNReal	—	edist_le_zero Function.IsFixedPt.eq PseudoEMetricSpace.edist_self ENNReal.zero_div edist_le_of_fixedPoint
exists_fixedPoint 📖	mathematical	ContractingWith	Function.IsFixedPt Filter.Tendsto Nat.iterate Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist DivInvMonoid.toDiv ENNReal.instDivInvMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ENNReal.ofNNReal ENNReal.instSub AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	cauchySeq_of_edist_le_geometric ENNReal.coe_lt_one_iff LipschitzWith.edist_iterate_succ_le_geometric toLipschitzWith cauchySeq_tendsto_of_complete isFixedPt_of_tendsto_iterate TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Continuous.continuousAt LipschitzWith.continuous edist_le_of_edist_le_geometric_of_tendsto
exists_fixedPoint' 📖	mathematical	IsComplete PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace Set.MapsTo ContractingWith Set.Elem instEMetricSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	Function.IsFixedPt Filter.Tendsto Nat.iterate Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist DivInvMonoid.toDiv ENNReal.instDivInvMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ENNReal.ofNNReal ENNReal.instSub AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	exists_fixedPoint IsComplete.completeSpace_coe Set.MapsTo.iterate Set.MapsTo.iterate_restrict Filter.Tendsto.comp Continuous.tendsto continuous_subtype_val
fixedPoint_isFixedPt 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace	Function.IsFixedPt fixedPoint	—	efixedPoint_isFixedPt
fixedPoint_lipschitz_in_map 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	fixedPoint DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instOne NNReal.toReal	—	dist_fixedPoint_fixedPoint_of_dist_le' fixedPoint_isFixedPt
fixedPoint_unique 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace Function.IsFixedPt	fixedPoint	—	fixedPoint_unique' fixedPoint_isFixedPt
fixedPoint_unique' 📖	—	ContractingWith MetricSpace.toEMetricSpace Function.IsFixedPt	—	—	eq_or_edist_eq_top_of_fixedPoints edist_ne_top
isFixedPt_fixedPoint_iterate 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace Nat.iterate	Function.IsFixedPt fixedPoint	—	fixedPoint_isFixedPt LipschitzWith.dist_le_mul toLipschitzWith Mathlib.Tactic.Contrapose.contrapose₁ one_mul mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing NNReal.coe_lt_one dist_pos Function.iterate_succ_apply' Function.iterate_succ_apply
one_sub_K_ne_top 📖	—	—	—	—	Nat.cast_one ENNReal.coe_ne_top
one_sub_K_ne_zero 📖	—	ContractingWith	—	—	ne_of_gt one_sub_K_pos'
one_sub_K_pos 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace	Real Real.instLT Real.instZero Real.instSub Real.instOne NNReal.toReal	—	sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
one_sub_K_pos' 📖	mathematical	ContractingWith	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal ENNReal.instSub AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal ENNReal.ofNNReal	—	ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub
restrict 📖	mathematical	ContractingWith Set.MapsTo	Set.Elem instEMetricSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	—	—
tendsto_iterate_efixedPoint 📖	mathematical	ContractingWith	Filter.Tendsto Nat.iterate Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace efixedPoint	—	exists_fixedPoint
tendsto_iterate_efixedPoint' 📖	mathematical	IsComplete PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace Set.MapsTo ContractingWith Set.Elem instEMetricSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	Filter.Tendsto Nat.iterate Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace efixedPoint'	—	exists_fixedPoint'
tendsto_iterate_fixedPoint 📖	mathematical	ContractingWith MetricSpace.toEMetricSpace	Filter.Tendsto Nat.iterate Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace fixedPoint	—	edist_ne_top fixedPoint_unique efixedPoint_isFixedPt tendsto_iterate_efixedPoint
toLipschitzWith 📖	mathematical	ContractingWith	LipschitzWith EMetricSpace.toPseudoEMetricSpace	—	—

(root)

Definitions

Name	Category	Theorems
ContractingWith 📖	MathDef	1 math math: ODE.FunSpace.exists_contractingWith_iterate_next

---

← Back to Index