RadiusLiminf

📁 Source: Mathlib/Analysis/Analytic/RadiusLiminf.lean

Statistics

Metric	Count
Definitions	0
Theorems radius_eq_liminf, radius_inv_eq_limsup	2
Total	2

FormalMultilinearSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
radius_eq_liminf 📖	mathematical	—	radius Filter.liminf ENNReal ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder DivInvMonoid.toDiv ENNReal.instDivInvMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal ENNReal.ofNNReal NNReal Real NNReal.instPowReal NNNorm.nnnorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype Real.instDivInvMonoid Real.instOne Real.instNatCast Filter.atTop Nat.instPreorder	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial one_div ENNReal.le_inv_iff_mul_le ENNReal.coe_mul ENNReal.coe_le_one_iff NNReal.rpow_one mul_inv_cancel₀ LT.lt.ne' NNReal.rpow_mul NNReal.mul_rpow NNReal.one_rpow NNReal.rpow_le_rpow_iff inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_comm NNReal.rpow_natCast le_antisymm ENNReal.le_of_forall_nnreal_lt List.TFAE.out TFAE_exists_lt_isLittleO_pow isLittleO_of_lt_radius Filter.le_liminf_of_le Filter.isCobounded_ge_of_top Filter.eventually_map Filter.Eventually.mp Filter.Eventually.mono Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder NNReal.coe_le_coe LE.le.trans le_abs_self pow_le_one₀ IsOrderedRing.toPosMulMono LT.lt.le le_radius_of_isBigO Asymptotics.IsBigO.of_norm_eventuallyLE Filter.mp_mem Filter.eventually_lt_of_lt_liminf Filter.isBounded_ge_of_bot Filter.univ_mem' norm_mul NormedDivisionRing.toNormMulClass norm_norm norm_pow NormedDivisionRing.to_normOneClass NNReal.abs_eq
radius_inv_eq_limsup 📖	mathematical	—	ENNReal ENNReal.instInv radius Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder ENNReal.ofNNReal NNReal Real NNReal.instPowReal NNNorm.nnnorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast Filter.atTop Nat.instPreorder	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul one_div ENNReal.inv_liminf inv_inv radius_eq_liminf

---

← Back to Index