SumTransform

📁 Source: Mathlib/Computability/AkraBazzi/SumTransform.lean

Statistics

Metric	Count
Definitions AkraBazziRecurrence, asympBound, max_bi, min_bi, n₀, p, smoothingFn, sumTransform	8
Theorems T_gt_zero', T_nonneg, T_pos, a_pos, asympBound_def, asympBound_def', asympBound_pos, b_lt_one, b_pos, bi_min_div_two_lt_one, bi_min_div_two_pos, continuous_sumCoeffsExp, deriv_smoothingFn, differentiableAt_one_add_smoothingFn, differentiableAt_one_sub_smoothingFn, differentiableAt_smoothingFn, differentiableOn_one_add_smoothingFn, differentiableOn_one_sub_smoothingFn, dist_r_b, dist_r_b', eventually_asympBound_pos, eventually_asympBound_r_pos, eventually_atTop_sumTransform_ge, eventually_atTop_sumTransform_le, eventually_b_le_r, eventually_bi_mul_le_r, eventually_deriv_one_add_smoothingFn, eventually_deriv_one_sub_smoothingFn, eventually_log_b_mul_pos, eventually_one_add_smoothingFn_nonneg, eventually_one_add_smoothingFn_pos, eventually_one_add_smoothingFn_r_pos, eventually_one_sub_smoothingFn_gt_const, eventually_one_sub_smoothingFn_gt_const_real, eventually_one_sub_smoothingFn_nonneg, eventually_one_sub_smoothingFn_pos, eventually_one_sub_smoothingFn_pos_real, eventually_one_sub_smoothingFn_r_pos, eventually_r_ge, eventually_r_le_b, eventually_r_lt_n, eventually_r_pos, exists_eventually_const_mul_le_r, exists_eventually_r_le_const_mul, g_grows_poly, g_nonneg, growsPolynomially_one_add_smoothingFn, growsPolynomially_one_sub_smoothingFn, h_rec, injective_sumCoeffsExp, isEquivalent_one_add_smoothingFn_one, isEquivalent_one_sub_smoothingFn_one, isEquivalent_smoothingFn_sub_self, isLittleO_deriv_one_add_smoothingFn, isLittleO_deriv_one_sub_smoothingFn, isLittleO_deriv_smoothingFn, isLittleO_self_div_log_id, isLittleO_smoothingFn_one, isTheta_smoothingFn_sub_self, max_bi_le, min_bi_le, n₀_gt_zero, one_add_smoothingFn_le_two, one_mem_range_sumCoeffsExp, p_def, r_lt_n, strictAntiOn_one_add_smoothingFn, strictAntiOn_smoothingFn, strictAnti_sumCoeffsExp, strictMonoOn_one_sub_smoothingFn, sumCoeffsExp_p_eq_one, sumTransform_def, tendsto_atTop_r, tendsto_atTop_r_real, tendsto_atTop_sumCoeffsExp, tendsto_zero_sumCoeffsExp	76
Total	84

AkraBazziRecurrence

Definitions

Name	Category	Theorems
asympBound 📖	CompOp	9 math math: T_isBigO_smoothingFn_mul_asympBound, isBigO_symm_asympBound, eventually_asympBound_pos, asympBound_def, asympBound_def', isBigO_asympBound, isTheta_asympBound, smoothingFn_mul_asympBound_isBigO_T, asympBound_pos
max_bi 📖	CompOp	1 math math: max_bi_le
min_bi 📖	CompOp	3 math math: min_bi_le, bi_min_div_two_pos, bi_min_div_two_lt_one
n₀ 📖	CompOp	1 math math: n₀_gt_zero
p 📖	CompOp	4 math math: asympBound_def, p_def, asympBound_def', sumCoeffsExp_p_eq_one
smoothingFn 📖	CompOp	39 math math: T_isBigO_smoothingFn_mul_asympBound, isLittleO_deriv_one_add_smoothingFn, differentiableAt_one_add_smoothingFn, isTheta_deriv_rpow_p_mul_one_sub_smoothingFn, eventually_one_sub_smoothingFn_gt_const, eventually_one_sub_smoothingFn_gt_const_real, eventually_deriv_one_add_smoothingFn, strictMonoOn_one_sub_smoothingFn, one_add_smoothingFn_le_two, isTheta_smoothingFn_sub_self, differentiableAt_one_sub_smoothingFn, eventually_deriv_rpow_p_mul_one_sub_smoothingFn, eventually_one_sub_smoothingFn_pos, eventually_deriv_rpow_p_mul_one_add_smoothingFn, isTheta_deriv_rpow_p_mul_one_add_smoothingFn, differentiableOn_one_add_smoothingFn, strictAntiOn_one_add_smoothingFn, eventually_one_sub_smoothingFn_pos_real, isEquivalent_one_sub_smoothingFn_one, eventually_one_sub_smoothingFn_nonneg, growsPolynomially_one_add_smoothingFn, eventually_deriv_one_sub_smoothingFn, isEquivalent_smoothingFn_sub_self, differentiableOn_one_sub_smoothingFn, deriv_smoothingFn, isLittleO_smoothingFn_one, isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn, isEquivalent_one_add_smoothingFn_one, differentiableAt_smoothingFn, isLittleO_deriv_one_sub_smoothingFn, growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn, isLittleO_deriv_smoothingFn, growsPolynomially_one_sub_smoothingFn, growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn, isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn, smoothingFn_mul_asympBound_isBigO_T, eventually_one_add_smoothingFn_nonneg, eventually_one_add_smoothingFn_pos, strictAntiOn_smoothingFn
sumTransform 📖	CompOp	2 math math: sumTransform_def, asympBound_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
T_gt_zero' 📖	mathematical	n₀	Real Real.instLT Real.instZero	—	—
T_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero	—	le_of_lt T_pos
T_pos 📖	mathematical	—	Real Real.instLT Real.instZero	—	lt_or_ge T_gt_zero' g_nonneg add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Finset.sum_pos Real.instIsOrderedCancelAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing a_pos r_lt_n Finset.univ_nonempty Real.instIsOrderedRing
a_pos 📖	mathematical	—	Real Real.instLT Real.instZero	—	—
asympBound_def 📖	mathematical	—	asympBound Real Real.instAdd Real.instPow Real.instNatCast p sumTransform	—	—
asympBound_def' 📖	mathematical	—	asympBound Real Real.instMul Real.instPow Real.instNatCast p Real.instAdd Real.instOne Finset.sum Real.instAddCommMonoid Finset.range DivInvMonoid.toDiv Real.instDivInvMonoid	—	Finset.sum_congr Nat.Ico_zero_eq_range mul_add Distrib.leftDistribClass mul_one
asympBound_pos 📖	mathematical	—	Real Real.instLT Real.instZero asympBound	—	add_zero mul_one Real.rpow_pos_of_pos Real.instIsOrderedRing Real.instNontrivial asympBound_def' mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid g_nonneg Finset.sum_nonneg div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.rpow_nonneg le_of_lt Nat.cast_pos' Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
b_lt_one 📖	mathematical	—	Real Real.instLT Real.instOne	—	—
b_pos 📖	mathematical	—	Real Real.instLT Real.instZero	—	—
bi_min_div_two_lt_one 📖	mathematical	—	Real Real.instLT DivInvMonoid.toDiv Real.instDivInvMonoid min_bi Finite.of_fintype instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instOne	—	Finite.of_fintype b_pos Nat.instAtLeastTwoHAddOfNat PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing b_lt_one
bi_min_div_two_pos 📖	mathematical	—	Real Real.instLT Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid min_bi Finite.of_fintype instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Finite.of_fintype Nat.instAtLeastTwoHAddOfNat b_pos Real.instIsOrderedRing Real.instNontrivial
continuous_sumCoeffsExp 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Finset.sum Real.instAddCommMonoid Finset.univ Real.instMul Real.instPow	—	continuous_finset_sum IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Continuous.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring continuous_const Continuous.rpow continuous_id ne_of_gt b_pos
deriv_smoothingFn 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace smoothingFn DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.instInv Monoid.toPow Real.instMonoid Real.log	—	one_div Real.deriv_inv_log
differentiableAt_one_add_smoothingFn 📖	mathematical	Real Real.instLT Real.instOne	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAdd Real.instOne smoothingFn	—	DifferentiableAt.add differentiableAt_const differentiableAt_smoothingFn
differentiableAt_one_sub_smoothingFn 📖	mathematical	Real Real.instLT Real.instOne	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instSub Real.instOne smoothingFn	—	DifferentiableAt.sub differentiableAt_const differentiableAt_smoothingFn
differentiableAt_smoothingFn 📖	mathematical	Real Real.instLT Real.instOne	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace smoothingFn	—	Real.log_ne_zero_of_pos_of_ne_one lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one ne_of_gt one_div DifferentiableAt.inv Real.differentiableAt_log
differentiableOn_one_add_smoothingFn 📖	mathematical	—	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAdd Real.instOne smoothingFn Set.Ioi Real.instPreorder	—	DifferentiableAt.differentiableWithinAt differentiableAt_one_add_smoothingFn
differentiableOn_one_sub_smoothingFn 📖	mathematical	—	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instSub Real.instOne smoothingFn Set.Ioi Real.instPreorder	—	DifferentiableAt.differentiableWithinAt differentiableAt_one_sub_smoothingFn
dist_r_b 📖	mathematical	—	Asymptotics.IsLittleO Real Real.norm Filter.atTop Nat.instPreorder Real.instSub Real.instNatCast Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toPow Real.instMonoid Real.log	—	—
dist_r_b' 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	Filter.eventually_all Finite.of_fintype instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat norm_div RCLike.norm_natCast norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass sq_abs Asymptotics.IsLittleO.eventuallyLE dist_r_b
eventually_asympBound_pos 📖	mathematical	—	Filter.Eventually Real Real.instLT Real.instZero asympBound Filter.atTop Nat.instPreorder	—	Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder Filter.univ_mem' asympBound_pos
eventually_asympBound_r_pos 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	Filter.eventually_all Finite.of_fintype Filter.Tendsto.eventually tendsto_atTop_r eventually_asympBound_pos
eventually_atTop_sumTransform_ge 📖	mathematical	—	Real Real.instLT Real.instZero Filter.Eventually Filter.atTop Nat.instPreorder	—	exists_eventually_const_mul_le_r GrowsPolynomially.eventually_atTop_ge_nat g_grows_poly exists_eventually_r_le_const_mul lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le lt_min mul_pos IsStrictOrderedRing.toPosMulStrictMono div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Real.rpow_pos_of_pos Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder eventually_r_lt_n eventually_r_pos Filter.univ_mem' g_nonneg le_of_lt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike le_or_gt mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Finset.sum_le_sum div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Finset.mem_Ico Set.mem_Icc Real.rpow_nonneg Nat.cast_nonneg' div_le_div₀ mul_nonneg le_refl Real.rpow_le_rpow Nat.mono_cast Finset.card_nsmul_le_sum nsmul_eq_mul mul_assoc Nat.card_Ico Nat.cast_sub mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono sub_le_sub_left covariant_swap_add_of_covariant_add Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_one Real.rpow_add_one ne_of_gt div_self mul_one min_le_left Real.rpow_le_rpow_of_nonpos Finset.Nonempty.card_pos Finset.Aesop.nonempty_Ico_of_lt Real.mul_rpow one_mul min_le_right
eventually_atTop_sumTransform_le 📖	mathematical	—	Real Real.instLT Real.instZero Filter.Eventually Filter.atTop Nat.instPreorder	—	exists_eventually_const_mul_le_r GrowsPolynomially.eventually_atTop_le_nat g_grows_poly lt_max_of_lt_left Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder eventually_r_lt_n eventually_r_pos Filter.univ_mem' g_nonneg le_of_lt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike le_or_gt mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing Finset.sum_le_sum div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Finset.mem_Ico Set.mem_Icc Real.rpow_nonneg Nat.cast_nonneg' Real.rpow_pos_of_pos div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_nonneg le_refl Real.rpow_le_rpow Nat.mono_cast Finset.sum_le_card_nsmul nsmul_eq_mul mul_assoc Nat.card_Ico Nat.cast_sub mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos mul_pos Real.rpow_add_one ne_of_gt Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw mul_comm Real.mul_rpow div_self mul_one le_max_right Real.rpow_le_rpow_of_nonpos le_max_left
eventually_b_le_r 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	Filter.mp_mem dist_r_b' Filter.univ_mem' le_of_lt b_pos sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_comm norm_mul NormedDivisionRing.toNormMulClass Real.norm_of_nonneg RCLike.norm_natCast norm_sub_norm_le norm_sub_rev
eventually_bi_mul_le_r 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	Finite.of_fintype b_pos isLittleO_self_div_log_id Nat.instAtLeastTwoHAddOfNat Asymptotics.isLittleO_iff div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Filter.mp_mem eventually_b_le_r Filter.univ_mem' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_zero_add sub_le_sub_left IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Real.norm_of_nonneg Nat.cast_nonneg' Real.instZeroLEOneClass sub_le_sub_right mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono min_bi_le div_nonneg Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul
eventually_deriv_one_add_smoothingFn 📖	mathematical	—	Filter.EventuallyEq Real Filter.atTop Real.instPreorder deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAdd Real.instOne smoothingFn DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.instInv Monoid.toPow Real.instMonoid Real.log	—	Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' deriv_fun_add differentiableAt_smoothingFn deriv_const' zero_add deriv_smoothingFn
eventually_deriv_one_sub_smoothingFn 📖	mathematical	—	Filter.EventuallyEq Real Filter.atTop Real.instPreorder deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instSub Real.instOne smoothingFn DivInvMonoid.toDiv Real.instDivInvMonoid Real.instInv Monoid.toPow Real.instMonoid Real.log	—	Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' deriv_fun_sub differentiableAt_smoothingFn deriv_const' zero_sub deriv_smoothingFn neg_div neg_neg
eventually_log_b_mul_pos 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	Filter.eventually_all Finite.of_fintype Filter.Tendsto.comp Real.tendsto_log_atTop Filter.Tendsto.const_mul_atTop Real.instIsStrictOrderedRing b_pos tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean Filter.Tendsto.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instNontrivial
eventually_one_add_smoothingFn_nonneg 📖	mathematical	—	Filter.Eventually Real Real.instLE Real.instZero Real.instAdd Real.instOne smoothingFn Real.instNatCast Filter.atTop Nat.instPreorder	—	Filter.mp_mem eventually_one_add_smoothingFn_pos Filter.univ_mem' le_of_lt
eventually_one_add_smoothingFn_pos 📖	mathematical	—	Filter.Eventually Real Real.instLT Real.instZero Real.instAdd Real.instOne smoothingFn Real.instNatCast Filter.atTop Nat.instPreorder	—	isLittleO_smoothingFn_one Filter.Eventually.natCast_atTop Real.instIsOrderedRing Real.instArchimedean Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instNontrivial Nat.instAtLeastTwoHAddOfNat Asymptotics.isLittleO_iff one_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Filter.univ_mem' Real.log_pos add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one div_pos
eventually_one_add_smoothingFn_r_pos 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	Filter.eventually_all Finite.of_fintype Filter.Tendsto.eventually tendsto_atTop_r eventually_one_add_smoothingFn_pos
eventually_one_sub_smoothingFn_gt_const 📖	mathematical	Real Real.instLT Real.instOne	Filter.Eventually Real Real.instLT Real.instSub Real.instOne smoothingFn Real.instNatCast Filter.atTop Nat.instPreorder	—	Filter.Eventually.natCast_atTop Real.instIsOrderedRing Real.instArchimedean eventually_one_sub_smoothingFn_gt_const_real
eventually_one_sub_smoothingFn_gt_const_real 📖	mathematical	Real Real.instLT Real.instOne	Filter.Eventually Real Real.instLT Real.instSub Real.instOne smoothingFn Filter.atTop Real.instPreorder	—	Asymptotics.isEquivalent_const_iff_tendsto one_ne_zero NeZero.charZero_one RCLike.charZero_rclike isEquivalent_one_sub_smoothingFn_one tendsto_order instOrderTopologyReal
eventually_one_sub_smoothingFn_nonneg 📖	mathematical	—	Filter.Eventually Real Real.instLE Real.instZero Real.instSub Real.instOne smoothingFn Real.instNatCast Filter.atTop Nat.instPreorder	—	Filter.mp_mem eventually_one_sub_smoothingFn_pos Filter.univ_mem' le_of_lt
eventually_one_sub_smoothingFn_pos 📖	mathematical	—	Filter.Eventually Real Real.instLT Real.instZero Real.instSub Real.instOne smoothingFn Real.instNatCast Filter.atTop Nat.instPreorder	—	Filter.Eventually.natCast_atTop Real.instIsOrderedRing Real.instArchimedean eventually_one_sub_smoothingFn_pos_real
eventually_one_sub_smoothingFn_pos_real 📖	mathematical	—	Filter.Eventually Real Real.instLT Real.instZero Real.instSub Real.instOne smoothingFn Filter.atTop Real.instPreorder	—	eventually_one_sub_smoothingFn_gt_const_real zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
eventually_one_sub_smoothingFn_r_pos 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	Filter.eventually_all Finite.of_fintype Filter.Tendsto.eventually tendsto_atTop_r_real eventually_one_sub_smoothingFn_pos_real
eventually_r_ge 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	exists_eventually_const_mul_le_r Filter.mp_mem Real.instIsStrictOrderedRing Filter.eventually_ge_atTop Filter.univ_mem' mul_div_assoc mul_div_cancel_left₀ GroupWithZero.toMulDivCancelClass ne_of_gt mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass
eventually_r_le_b 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	Filter.mp_mem dist_r_b' Filter.univ_mem' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.le_norm_self
eventually_r_lt_n 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	Filter.mp_mem Filter.eventually_ge_atTop Filter.univ_mem' r_lt_n
eventually_r_pos 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	Filter.eventually_all Finite.of_fintype Filter.Tendsto.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder tendsto_atTop_r
exists_eventually_const_mul_le_r 📖	mathematical	—	Real Set Set.instMembership Set.Ioo Real.instPreorder Real.instZero Real.instOne Filter.Eventually Filter.atTop Nat.instPreorder	—	Finite.of_fintype b_pos Nat.instAtLeastTwoHAddOfNat div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo bi_min_div_two_lt_one eventually_bi_mul_le_r
exists_eventually_r_le_const_mul 📖	mathematical	—	Real Set Set.instMembership Set.Ioo Real.instPreorder Real.instZero Real.instOne Filter.Eventually Filter.atTop Nat.instPreorder	—	Finite.of_fintype Nat.instAtLeastTwoHAddOfNat b_pos b_lt_one lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.mul_congr add_lt_add_left IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_div isLittleO_self_div_log_id Asymptotics.isLittleO_iff Filter.mp_mem eventually_r_le_b Filter.univ_mem' add_le_add_right Real.norm_of_nonneg Nat.cast_nonneg' Real.instZeroLEOneClass div_nonneg Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono add_le_add_left max_bi_le
g_grows_poly 📖	mathematical	—	GrowsPolynomially	—	—
g_nonneg 📖	mathematical	Real Real.instLE Real.instZero	Real Real.instLE Real.instZero	—	—
growsPolynomially_one_add_smoothingFn 📖	mathematical	—	GrowsPolynomially Real Real.instAdd Real.instOne smoothingFn	—	GrowsPolynomially.of_isEquivalent_const isEquivalent_one_add_smoothingFn_one
growsPolynomially_one_sub_smoothingFn 📖	mathematical	—	GrowsPolynomially Real Real.instSub Real.instOne smoothingFn	—	GrowsPolynomially.of_isEquivalent_const isEquivalent_one_sub_smoothingFn_one
h_rec 📖	mathematical	n₀	Real Real.instAdd Finset.sum Real.instAddCommMonoid Finset.univ Real.instMul Real.instNatCast	—	—
injective_sumCoeffsExp 📖	mathematical	—	Real Finset.sum Real.instAddCommMonoid Finset.univ Real.instMul Real.instPow	—	StrictAnti.injective strictAnti_sumCoeffsExp
isEquivalent_one_add_smoothingFn_one 📖	mathematical	—	Asymptotics.IsEquivalent Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.atTop Real.instPreorder Real.instAdd Real.instOne smoothingFn	—	Asymptotics.IsEquivalent.add_isLittleO Asymptotics.IsEquivalent.refl isLittleO_smoothingFn_one
isEquivalent_one_sub_smoothingFn_one 📖	mathematical	—	Asymptotics.IsEquivalent Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.atTop Real.instPreorder Real.instSub Real.instOne smoothingFn	—	Asymptotics.IsEquivalent.sub_isLittleO Asymptotics.IsEquivalent.refl isLittleO_smoothingFn_one
isEquivalent_smoothingFn_sub_self 📖	mathematical	—	Asymptotics.IsEquivalent Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.atTop Nat.instPreorder Real.instSub smoothingFn Real.instMul Real.instNatCast DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.log Monoid.toPow Real.instMonoid	—	Filter.mp_mem eventually_log_b_mul_pos Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder Filter.univ_mem' Real.log_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike one_div inv_sub_inv ne_of_gt Nat.instCanonicallyOrderedAdd Real.log_neg_eq_log Real.log_one Filter.eventually_ne_atTop b_pos Real.log_mul sub_add_eq_sub_sub Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_congr Asymptotics.IsEquivalent.div Asymptotics.IsEquivalent.refl Asymptotics.IsEquivalent.mul add_comm Asymptotics.IsEquivalent.add_isLittleO Asymptotics.IsLittleO.natCast_atTop Real.instIsStrictOrderedRing Real.instArchimedean Real.isLittleO_const_log_atTop pow_two
isLittleO_deriv_one_add_smoothingFn 📖	mathematical	—	Asymptotics.IsLittleO Real Real.norm Filter.atTop Real.instPreorder deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAdd Real.instOne smoothingFn Real.instInv	—	Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' deriv_fun_add differentiableAt_smoothingFn deriv_const' zero_add isLittleO_deriv_smoothingFn
isLittleO_deriv_one_sub_smoothingFn 📖	mathematical	—	Asymptotics.IsLittleO Real Real.norm Filter.atTop Real.instPreorder deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instSub Real.instOne smoothingFn Real.instInv	—	Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' deriv_fun_sub differentiableAt_smoothingFn deriv_const' zero_sub Asymptotics.isLittleO_neg_left isLittleO_deriv_smoothingFn
isLittleO_deriv_smoothingFn 📖	mathematical	—	Asymptotics.IsLittleO Real Real.norm Filter.atTop Real.instPreorder deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace smoothingFn Real.instInv	—	Filter.univ_mem' deriv_smoothingFn neg_div div_eq_mul_inv neg_inv neg_mul Asymptotics.IsLittleO.inv_rev Asymptotics.IsBigO.mul_isLittleO NormedDivisionRing.toNormMulClass Asymptotics.isBigO_neg_right Asymptotics.isBigO_refl Asymptotics.isLittleO_one_left_iff NormedDivisionRing.to_normOneClass Filter.Tendsto.comp tendsto_norm_atTop_atTop Filter.tendsto_pow_atTop Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_eq_false Nat.instCharZero Mathlib.Meta.NormNum.isNat_ofNat Real.tendsto_log_atTop Filter.Eventually.of_forall mul_one neg_zero Real.log_zero zero_pow Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero
isLittleO_self_div_log_id 📖	mathematical	—	Asymptotics.IsLittleO Real Real.norm Filter.atTop Nat.instPreorder DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Monoid.toPow Real.instMonoid Real.log	—	div_eq_mul_inv Asymptotics.IsBigO.mul_isLittleO NormedDivisionRing.toNormMulClass Asymptotics.isBigO_refl Asymptotics.IsLittleO.inv_rev one_pow Asymptotics.IsLittleO.pow Asymptotics.IsLittleO.natCast_atTop Real.instIsStrictOrderedRing Real.instArchimedean Real.isLittleO_const_log_atTop Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instCharZero Mathlib.Meta.NormNum.isNat_ofNat NeZero.charZero_one RCLike.charZero_rclike isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors Nat.instAtLeastTwoHAddOfNat instIsEmptyFalse instIsDirectedOrder instArchimedeanNat inv_one mul_one
isLittleO_smoothingFn_one 📖	mathematical	—	Asymptotics.IsLittleO Real Real.norm Filter.atTop Real.instPreorder smoothingFn Real.instOne	—	Asymptotics.isLittleO_of_tendsto one_ne_zero NeZero.charZero_one RCLike.charZero_rclike one_div div_one Filter.Tendsto.inv_tendsto_atTop Real.instIsStrictOrderedRing instOrderTopologyReal Real.tendsto_log_atTop
isTheta_smoothingFn_sub_self 📖	mathematical	—	Asymptotics.IsTheta Real Real.norm Filter.atTop Nat.instPreorder Real.instSub smoothingFn Real.instMul Real.instNatCast DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Monoid.toPow Real.instMonoid Real.log	—	Asymptotics.IsEquivalent.isTheta isEquivalent_smoothingFn_sub_self mul_one neg_ne_zero Real.log_ne_zero_of_pos_of_ne_one b_pos ne_of_lt b_lt_one Asymptotics.isTheta_const_mul_right Asymptotics.isTheta_refl
max_bi_le 📖	mathematical	—	Real Real.instLE max_bi	—	Finite.exists_max
min_bi_le 📖	mathematical	—	Real Real.instLE min_bi	—	Finite.exists_min
n₀_gt_zero 📖	mathematical	—	n₀	—	—
one_add_smoothingFn_le_two 📖	mathematical	Real Real.instLE Real.exp Real.instOne	Real Real.instLE Real.instAdd Real.instOne smoothingFn instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.exp_zero Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike div_le_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.log_pos Real.log_exp Real.log_le_log Real.exp_pos
one_mem_range_sumCoeffsExp 📖	mathematical	—	Real Set Set.instMembership Set.range Finset.sum Real.instAddCommMonoid Finset.univ Real.instMul Real.instPow Real.instOne	—	mem_range_of_exists_le_of_exists_ge HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ConnectedSpace.toPreconnectedSpace PathConnectedSpace.connectedSpace Real.instPathConnectedSpace continuous_sumCoeffsExp Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean Filter.Tendsto.eventually_le_const instClosedIciTopology zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike tendsto_zero_sumCoeffsExp Filter.atBot_neBot instIsCodirectedOrder Filter.Tendsto.eventually_ge_atTop tendsto_atTop_sumCoeffsExp
p_def 📖	mathematical	—	p Function.invFun Real Real.instInhabited Finset.sum Real.instAddCommMonoid Finset.univ Real.instMul Real.instPow Real.instOne	—	—
r_lt_n 📖	—	n₀	—	—	—
strictAntiOn_one_add_smoothingFn 📖	mathematical	—	StrictAntiOn Real Real.instPreorder Real.instAdd Real.instOne smoothingFn Set.Ioi	—	StrictAntiOn.const_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid strictAntiOn_smoothingFn
strictAntiOn_smoothingFn 📖	mathematical	—	StrictAntiOn Real Real.instPreorder smoothingFn Set.Ioi Real.instOne	—	one_div StrictAntiOn.comp_strictMonoOn inv_strictAntiOn PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing StrictMonoOn.mono Real.strictMonoOn_log Set.Ioi_subset_Ioi zero_le_one Real.instZeroLEOneClass Real.log_pos
strictAnti_sumCoeffsExp 📖	mathematical	—	StrictAnti Real Real.instPreorder Finset.sum Real.instAddCommMonoid Finset.univ Real.instMul Real.instPow	—	Finset.sum_fn Finset.sum_induction_nonempty StrictAnti.add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add Finset.univ_nonempty StrictAnti.const_mul IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.strictAnti_rpow_of_base_lt_one b_pos b_lt_one a_pos
strictMonoOn_one_sub_smoothingFn 📖	mathematical	—	StrictMonoOn Real Real.instPreorder Real.instSub Real.instOne smoothingFn Set.Ioi	—	sub_eq_add_neg StrictMonoOn.const_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid StrictAntiOn.neg IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add strictAntiOn_smoothingFn
sumCoeffsExp_p_eq_one 📖	mathematical	—	Finset.sum Real Real.instAddCommMonoid Finset.univ Real.instMul Real.instPow p Real.instOne	—	Finset.sum_congr p_def Function.invFun_eq Set.mem_range one_mem_range_sumCoeffsExp
sumTransform_def 📖	mathematical	—	sumTransform Real Real.instMul Real.instPow Real.instNatCast Finset.sum Real.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd Real.instOne	—	—
tendsto_atTop_r 📖	mathematical	—	Filter.Tendsto Filter.atTop Nat.instPreorder	—	Filter.tendsto_atTop eventually_r_ge IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Filter.eventually_all Finite.of_fintype
tendsto_atTop_r_real 📖	mathematical	—	Filter.Tendsto Real Real.instNatCast Filter.atTop Nat.instPreorder Real.instPreorder	—	Filter.Tendsto.comp tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean tendsto_atTop_r
tendsto_atTop_sumCoeffsExp 📖	mathematical	—	Filter.Tendsto Real Finset.sum Real.instAddCommMonoid Finset.univ Real.instMul Real.instPow Filter.atBot Real.instPreorder Filter.atTop	—	Finite.of_fintype Filter.Tendsto.const_mul_atTop Real.instIsStrictOrderedRing a_pos tendsto_rpow_atBot_of_base_lt_one b_pos lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le b_lt_one Filter.tendsto_atTop_mono Finset.single_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.rpow_pos_of_pos Finset.mem_univ
tendsto_zero_sumCoeffsExp 📖	mathematical	—	Filter.Tendsto Real Finset.sum Real.instAddCommMonoid Finset.univ Real.instMul Real.instPow Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	Finset.sum_const_zero tendsto_finset_sum IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal MulZeroClass.mul_zero Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal Filter.atTop_neBot instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean tendsto_rpow_atTop_of_base_lt_one b_pos lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le b_lt_one

(root)

Definitions

Name	Category	Theorems
AkraBazziRecurrence 📖	CompData	—

---

← Back to Index