Documentation Verification Report

RpowTendsto

📁 Source: Mathlib/Analysis/SpecialFunctions/Log/RpowTendsto.lean

Statistics

Metric	Count
Definitions	0
Theorems `norm_inv_mul_rpow_sub_one_sub_log_le`, `tendstoLocallyUniformlyOn_rpow_sub_one_log`, `tendsto_rpow_sub_one_log`	3
Total	3

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_inv_mul_rpow_sub_one_sub_log_le` 📖	mathematical	`Real` `instLT` `instZero` `instLE` `Norm.norm` `norm` `instMul` `log` `instOne`	`instSub` `instInv` `instPow` `Monoid.toNatPow` `instMonoid`	—	`norm_mul` `NormedDivisionRing.toNormMulClass` `norm_of_nonneg` `mul_comm` `exp_mul` `exp_log` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `norm_exp_sub_one_sub_id_le` `le_of_lt` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing`
`tendstoLocallyUniformlyOn_rpow_sub_one_log` 📖	mathematical	—	`TendstoLocallyUniformlyOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instMul` `instInv` `instSub` `instPow` `instOne` `log` `nhdsWithin` `instZero` `Set.Ioi` `instPreorder`	—	`tendstoLocallyUniformlyOn_iff_forall_isCompact` `locallyCompact_of_proper` `instProperSpaceReal` `isOpen_Ioi` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `Filter.HasBasis.tendstoUniformlyOn_iff_of_uniformity` `Metric.uniformity_basis_dist_le` `sSup_nonneg` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Mathlib.Meta.Positivity.pos_of_isNat` `instIsOrderedRing` `instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Filter.HasBasis.mem_of_mem` `nhdsGT_basis` `instOrderTopologyReal` `instNoMaxOrderOfNontrivial` `Filter.Eventually.filter_mono` `nhdsWithin_le_nhds` `eventually_le_nhds` `instClosedIciTopology` `ContinuousOn.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousOn.norm` `ContinuousOn.log` `continuousOn_id'` `Filter.mp_mem` `Filter.univ_mem'` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `norm_nonneg` `div_le_div₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `le_of_lt` `le_refl` `add_le_add_left` `le_csSup` `div_le_one₀` `dist_eq_norm'` `norm_inv_mul_rpow_sub_one_sub_log_le` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `mul_le_mul`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_rpow_sub_one_log` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter.Tendsto` `Real.instMul` `Real.instInv` `Real.instSub` `Real.instPow` `Real.instOne` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.Ioi` `Real.instPreorder` `nhds` `Real.log`	—	`TendstoLocallyUniformlyOn.tendsto_at` `Real.tendstoLocallyUniformlyOn_rpow_sub_one_log`

---

← Back to Index