Order

📁 Source: Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Order.lean

Statistics

Metric	Count
Definitions	0
Theorems log_le_log, log_monotoneOn, tendsto_cfc_rpow_sub_one_log	3
Total	3

CFC

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
log_le_log 📖	mathematical	Preorder.toLE PartialOrder.toPreorder IsStrictlyPositive MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	log CStarAlgebra.toStarRing NormedAlgebra.complexToReal NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra IsSelfAdjoint.instContinuousFunctionalCalculus UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedAlgebra.toAlgebra Complex Complex.instNormedField IsStarNormal.instContinuousFunctionalCalculus	—	log_monotoneOn IsStrictlyPositive.of_le
log_monotoneOn 📖	mathematical	—	MonotoneOn PartialOrder.toPreorder log CStarAlgebra.toNormedRing CStarAlgebra.toStarRing NormedAlgebra.complexToReal NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra IsSelfAdjoint.instContinuousFunctionalCalculus UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedAlgebra.toAlgebra Complex Complex.instNormedField IsStarNormal.instContinuousFunctionalCalculus setOf IsStrictlyPositive Preorder.toLE MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsSelfAdjoint.instContinuousFunctionalCalculus IsStarNormal.instContinuousFunctionalCalculus MonotoneOn.congr IsClosed.mem_of_tendsto nhdsGT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial isClosed_monotoneOn CStarAlgebra.instOrderClosedTopology tendsto_pi_nhds Filter.Tendsto.congr tendsto_cfc_rpow_sub_one_log T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Filter.HasBasis.mem_of_mem nhdsGT_basis zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.mp_mem Filter.univ_mem' CStarAlgebra.instNonnegSpectrumClass' cfc_smul UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsScalarTower.left Pi.isScalarTower IsScalarTower.right ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Continuous.continuousOn Real.continuous_rpow_const instIsPreorder_mathlib instOrderedRingOfIsStrictOrderedRing instLawfulOrderLT_mathlib continuousOn_const cfc_sub cfc_const_one IsSelfAdjoint.of_nonneg IsStrictlyPositive.nonneg rpow_eq_cfc_real NonUnitalSeminormedRing.toIsTopologicalRing TopologicalSpace.t2Space_of_metrizableSpace smul_le_smul_of_nonneg_left IsOrderedModule.toPosSMulMono instIsOrderedModule Real.instStarOrderedRing StarModule.complexToReal CStarAlgebra.toStarModule Algebra.to_smulCommClass sub_le_sub_right covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid rpow_le_rpow le_of_lt inv_pos_of_pos
tendsto_cfc_rpow_sub_one_log 📖	mathematical	IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Filter.Tendsto Real cfc IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid CStarAlgebra.toStarRing Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedAlgebra.toAlgebra Real.normedField NormedAlgebra.complexToReal CStarAlgebra.toNormedAlgebra IsSelfAdjoint.instContinuousFunctionalCalculus Complex Complex.instNormedField IsStarNormal.instContinuousFunctionalCalculus Real.instMul Real.instInv Real.instSub Real.instPow Real.instOne nhdsWithin Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds log	—	tendsto_cfc_fun IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsSelfAdjoint.instContinuousFunctionalCalculus IsStarNormal.instContinuousFunctionalCalculus Real.tendstoLocallyUniformlyOn_rpow_sub_one_log tendstoLocallyUniformlyOn_iff_forall_isCompact locallyCompact_of_proper instProperSpaceReal isOpen_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.Eventually.of_forall ContinuousOn.fun_mul IsTopologicalSemiring.toContinuousMul continuousOn_const ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal ContDiffOn.continuousOn_zero ContDiffOn.rpow_const_of_ne contDiffOn_fun_id IsStrictlyPositive.spectrum_pos CStarAlgebra.instNonnegSpectrumClass' instLawfulOrderLT_mathlib instIsPreorder_mathlib instOrderedRingOfIsStrictOrderedRing Real.instIsStrictOrderedRing

---

← Back to Index