AkraBazzi

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

Statistics

Metric	Count
Definitions	0
Theorems T_isBigO_smoothingFn_mul_asympBound, eventually_deriv_rpow_p_mul_one_add_smoothingFn, eventually_deriv_rpow_p_mul_one_sub_smoothingFn, growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn, growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn, isBigO_apply_r_sub_b, isBigO_asympBound, isBigO_symm_asympBound, isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn, isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn, isTheta_asympBound, isTheta_deriv_rpow_p_mul_one_add_smoothingFn, isTheta_deriv_rpow_p_mul_one_sub_smoothingFn, rpow_p_mul_one_add_smoothingFn_ge, rpow_p_mul_one_sub_smoothingFn_le, smoothingFn_mul_asympBound_isBigO_T	16
Total	16

AkraBazziRecurrence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
T_isBigO_smoothingFn_mul_asympBound 📖	mathematical	—	Asymptotics.IsBigO Real Real.norm Filter.atTop Nat.instPreorder Real.instMul Real.instSub Real.instOne smoothingFn Real.instNatCast asympBound	—	Asymptotics.isBigO_nat_atTop_induction_of_eventually_pos Filter.Eventually.of_forall T_nonneg Filter.mp_mem eventually_one_sub_smoothingFn_pos eventually_asympBound_pos Filter.univ_mem' mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Finite.of_fintype Nat.instAtLeastTwoHAddOfNat bi_min_div_two_pos eventually_atTop_sumTransform_ge Filter.eventually_ge_atTop eventually_bi_mul_le_r eventually_one_sub_smoothingFn_gt_const Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo rpow_p_mul_one_sub_smoothingFn_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Nat.le_ceil mul_comm div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono g_nonneg Nat.cast_nonneg' add_le_add_left covariant_swap_add_of_covariant_add Finset.sum_le_sum mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt a_pos Finset.sum_congr asympBound_def' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos 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_congr 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_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono add_nonneg zero_le_one Finset.sum_nonneg div_nonneg_iff Real.rpow_nonneg mul_nonneg eq_sub_of_add_eq add_comm add_eq_of_eq_sub Finset.sum_Ico_eq_sub r_lt_n LE.le.trans Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat sub_le_sub_left b_pos Real.rpow_pos_of_pos Finset.mul_sum sumCoeffsExp_p_eq_one mul_one add_le_add_right mul_nonpos_of_nonpos_of_nonneg sub_nonpos inv_mul_cancel₀ ne_of_gt Mathlib.Meta.NormNum.isNat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz mul_le_mul div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
eventually_deriv_rpow_p_mul_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.instMul Real.instPow Real.instAdd Real.instOne smoothingFn Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Real.log	—	Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' deriv_fun_mul Real.differentiableAt_rpow_const_of_ne ne_of_gt lt_trans Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one differentiableAt_one_add_smoothingFn eventually_deriv_one_add_smoothingFn Real.deriv_rpow_const sub_eq_add_neg neg_div mul_neg mul_div Real.rpow_add
eventually_deriv_rpow_p_mul_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.instMul Real.instPow Real.instSub Real.instOne smoothingFn Real.instAdd DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Real.log	—	Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' deriv_fun_mul Real.differentiableAt_rpow_const_of_ne ne_of_gt lt_trans Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one differentiableAt_one_sub_smoothingFn eventually_deriv_one_sub_smoothingFn Real.deriv_rpow_const mul_div Real.rpow_neg_one Real.rpow_add sub_eq_add_neg
growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn 📖	mathematical	—	GrowsPolynomially Norm.norm Real Real.norm 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.instMul Real.instPow Real.instAdd Real.instOne smoothingFn	—	eq_or_ne Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial eventually_deriv_one_add_smoothingFn Filter.univ_mem' Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing inv_pos_of_pos lt_trans Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul Real.rpow_zero one_mul neg_div norm_neg Real.norm_of_nonneg GrowsPolynomially.congr_of_eventuallyEq GrowsPolynomially.div GrowsPolynomially.inv growsPolynomially_id GrowsPolynomially.pow growsPolynomially_log Filter.eventually_ge_atTop Real.log_nonneg GrowsPolynomially.of_isTheta growsPolynomially_rpow isTheta_deriv_rpow_p_mul_one_add_smoothingFn norm_nonneg
growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn 📖	mathematical	—	GrowsPolynomially Norm.norm Real Real.norm 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.instMul Real.instPow Real.instSub Real.instOne smoothingFn	—	eq_or_ne Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial eventually_deriv_one_sub_smoothingFn Filter.univ_mem' Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing inv_pos_of_pos lt_trans Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul Real.rpow_zero one_mul Real.norm_of_nonneg GrowsPolynomially.congr_of_eventuallyEq GrowsPolynomially.div GrowsPolynomially.inv growsPolynomially_id GrowsPolynomially.pow growsPolynomially_log Filter.eventually_ge_atTop Real.log_nonneg GrowsPolynomially.of_isTheta growsPolynomially_rpow isTheta_deriv_rpow_p_mul_one_sub_smoothingFn norm_nonneg
isBigO_apply_r_sub_b 📖	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 Set.Ioi Real.instPreorder Real.instOne GrowsPolynomially Norm.norm Real.norm deriv	Asymptotics.IsBigO Filter.atTop Nat.instPreorder Real.instSub Real.instNatCast Real.instMul	—	Finite.of_fintype Nat.instAtLeastTwoHAddOfNat b_pos 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 div_two_lt_of_pos b_lt_one div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono min_bi_le le_of_lt Asymptotics.isBigO_iff Filter.Tendsto.const_mul_atTop Filter.tendsto_id Filter.mp_mem Filter.Eventually.natCast_atTop Real.instArchimedean Filter.Tendsto.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Filter.eventually_gt_atTop Nat.instNoMaxOrder Filter.eventually_ge_atTop eventually_bi_mul_le_r Filter.univ_mem' norm_mul NormedDivisionRing.toNormMulClass mul_assoc Convex.norm_image_sub_le_of_norm_deriv_le DifferentiableOn.differentiableAt Ioi_mem_nhds instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid convex_Icc IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike one_mul r_lt_n
isBigO_asympBound 📖	mathematical	—	Asymptotics.IsBigO Real Real.norm Filter.atTop Nat.instPreorder asympBound	—	T_isBigO_smoothingFn_mul_asympBound Asymptotics.IsBigO.mul NormedDivisionRing.toNormMulClass Asymptotics.isBigO_const_of_tendsto Filter.Tendsto.comp Asymptotics.IsEquivalent.tendsto_const isEquivalent_one_sub_smoothingFn_one tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean one_ne_zero NeZero.charZero_one RCLike.charZero_rclike Asymptotics.isBigO_refl one_mul
isBigO_symm_asympBound 📖	mathematical	—	Asymptotics.IsBigO Real Real.norm Filter.atTop Nat.instPreorder asympBound	—	one_mul Asymptotics.IsEquivalent.mul Asymptotics.IsEquivalent.symm Function.const_def Asymptotics.isEquivalent_const_iff_tendsto one_ne_zero NeZero.charZero_one RCLike.charZero_rclike Filter.Tendsto.comp Asymptotics.IsEquivalent.tendsto_const isEquivalent_one_add_smoothingFn_one tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean Asymptotics.IsEquivalent.refl smoothingFn_mul_asympBound_isBigO_T
isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn 📖	mathematical	—	Asymptotics.IsEquivalent Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.atTop Real.instPreorder deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Real.instPow Real.instAdd Real.instOne smoothingFn Real.instSub	—	eventually_deriv_rpow_p_mul_one_add_smoothingFn Asymptotics.IsEquivalent.add_isLittleO Asymptotics.IsEquivalent.mul Asymptotics.IsEquivalent.refl isEquivalent_one_add_smoothingFn_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one div_eq_mul_inv Asymptotics.IsBigO.mul_isLittleO NormedDivisionRing.toNormMulClass Asymptotics.isBigO_refl Asymptotics.IsLittleO.inv_rev Asymptotics.isLittleO_const_left Filter.Tendsto.comp tendsto_norm_atTop_atTop Filter.tendsto_pow_atTop Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_eq_false Nat.instCharZero Real.tendsto_log_atTop NeZero.charZero_one RCLike.charZero_rclike isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors Nat.instAtLeastTwoHAddOfNat instIsEmptyFalse instIsDirectedOrder Real.instArchimedean div_one Asymptotics.IsTheta.const_mul_right Asymptotics.isTheta_refl
isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn 📖	mathematical	—	Asymptotics.IsEquivalent Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.atTop Real.instPreorder deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Real.instPow Real.instSub Real.instOne smoothingFn	—	eventually_deriv_rpow_p_mul_one_sub_smoothingFn Asymptotics.IsEquivalent.add_isLittleO Asymptotics.IsEquivalent.mul Asymptotics.IsEquivalent.refl isEquivalent_one_sub_smoothingFn_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one div_eq_mul_inv Asymptotics.IsBigO.mul_isLittleO NormedDivisionRing.toNormMulClass Asymptotics.isBigO_refl Asymptotics.IsLittleO.inv_rev Asymptotics.isLittleO_const_left Filter.Tendsto.comp tendsto_norm_atTop_atTop Filter.tendsto_pow_atTop Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_eq_false Nat.instCharZero Real.tendsto_log_atTop NeZero.charZero_one RCLike.charZero_rclike isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors Nat.instAtLeastTwoHAddOfNat instIsEmptyFalse instIsDirectedOrder Real.instArchimedean div_one Asymptotics.IsTheta.const_mul_right Asymptotics.isTheta_refl
isTheta_asympBound 📖	mathematical	—	Asymptotics.IsTheta Real Real.norm Filter.atTop Nat.instPreorder asympBound	—	isBigO_asympBound isBigO_symm_asympBound
isTheta_deriv_rpow_p_mul_one_add_smoothingFn 📖	mathematical	—	Asymptotics.IsTheta Real Real.norm Filter.atTop Real.instPreorder Norm.norm 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.instMul Real.instPow Real.instAdd Real.instOne smoothingFn Real.instSub	—	Asymptotics.IsTheta.norm_left Asymptotics.IsEquivalent.isTheta isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn Asymptotics.IsTheta.const_mul_left Asymptotics.isTheta_refl
isTheta_deriv_rpow_p_mul_one_sub_smoothingFn 📖	mathematical	—	Asymptotics.IsTheta Real Real.norm Filter.atTop Real.instPreorder Norm.norm 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.instMul Real.instPow Real.instSub Real.instOne smoothingFn	—	Asymptotics.IsTheta.norm_left Asymptotics.IsEquivalent.isTheta isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn Asymptotics.IsTheta.const_mul_left Asymptotics.isTheta_refl
rpow_p_mul_one_add_smoothingFn_ge 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	Filter.eventually_all Finite.of_fintype DifferentiableOn.mul DifferentiableOn.mono Real.differentiableOn_rpow_const Set.mem_compl_singleton_iff ne_of_gt LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Set.mem_Ioi differentiableOn_one_add_smoothingFn Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.eventually_ne_atTop Filter.univ_mem' deriv_fun_mul differentiableAt_smoothingFn Asymptotics.IsBigO.add Asymptotics.IsBigO.mul NormedDivisionRing.toNormMulClass isBigO_deriv_rpow_const_atTop Asymptotics.isBigO_refl Asymptotics.IsEquivalent.isBigO isEquivalent_one_add_smoothingFn_one mul_one Asymptotics.IsLittleO.isBigO isLittleO_deriv_one_add_smoothingFn Real.rpow_neg_one Real.rpow_add sub_eq_add_neg Asymptotics.IsLittleO.eventuallyLE isBigO_apply_r_sub_b growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn Asymptotics.IsBigO.mul_isLittleO dist_r_b Asymptotics.IsBigO.natCast_atTop Real.instIsStrictOrderedRing Real.instArchimedean Nat.instNoMaxOrder Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Real.rpow_add_one sub_add_cancel mul_div Asymptotics.IsTheta.symm mul_assoc Asymptotics.IsTheta.const_mul_left b_pos Real.rpow_pos_of_pos Asymptotics.isTheta_refl Asymptotics.IsTheta.mul isTheta_smoothingFn_sub_self norm_sub_rev Real.le_norm_self Real.norm_of_nonneg sub_nonneg_of_le covariant_swap_add_of_covariant_add StrictAntiOn.le_iff_ge strictAntiOn_smoothingFn Nat.one_lt_cast mul_inv_cancel₀ mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Nat.le_ceil le_of_lt mul_lt_mul_of_pos_left IsStrictOrderedRing.toPosMulStrictMono Nat.strictMono_cast b_lt_one mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono lt_trans Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat one_mul mul_nonneg mul_pos Real.mul_rpow Nat.cast_nonneg' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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.add_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add sub_le_iff_le_add' sub_le_iff_le_add
rpow_p_mul_one_sub_smoothingFn_le 📖	mathematical	—	Filter.Eventually Filter.atTop Nat.instPreorder	—	Filter.eventually_all Finite.of_fintype DifferentiableOn.mul DifferentiableOn.mono Real.differentiableOn_rpow_const Set.mem_compl_singleton_iff ne_of_gt LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Set.mem_Ioi differentiableOn_one_sub_smoothingFn Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.eventually_ne_atTop Filter.univ_mem' deriv_fun_mul differentiableAt_smoothingFn Asymptotics.IsBigO.add Asymptotics.IsBigO.mul NormedDivisionRing.toNormMulClass isBigO_deriv_rpow_const_atTop Asymptotics.isBigO_refl Asymptotics.IsEquivalent.isBigO isEquivalent_one_sub_smoothingFn_one mul_one Asymptotics.IsLittleO.isBigO isLittleO_deriv_one_sub_smoothingFn Real.rpow_neg_one Real.rpow_add sub_eq_add_neg Asymptotics.IsLittleO.eventuallyLE isBigO_apply_r_sub_b growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn Asymptotics.IsBigO.mul_isLittleO dist_r_b Asymptotics.IsBigO.natCast_atTop Real.instIsStrictOrderedRing Real.instArchimedean Nat.instNoMaxOrder Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Real.rpow_add_one sub_add_cancel mul_div Asymptotics.IsTheta.symm mul_assoc Asymptotics.IsTheta.const_mul_left b_pos Real.rpow_pos_of_pos Asymptotics.isTheta_refl Asymptotics.IsTheta.mul isTheta_smoothingFn_sub_self Real.le_norm_self Real.norm_of_nonneg sub_nonneg_of_le covariant_swap_add_of_covariant_add StrictAntiOn.le_iff_ge strictAntiOn_smoothingFn Nat.one_lt_cast mul_inv_cancel₀ mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Nat.le_ceil le_of_lt mul_lt_mul_of_pos_left IsStrictOrderedRing.toPosMulStrictMono Nat.strictMono_cast b_lt_one mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono lt_trans Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat one_mul mul_nonneg mul_pos Real.mul_rpow Nat.cast_nonneg' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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.cast_pos Nat.cast_one 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 sub_le_iff_le_add'
smoothingFn_mul_asympBound_isBigO_T 📖	mathematical	—	Asymptotics.IsBigO Real Real.norm Filter.atTop Nat.instPreorder Real.instMul Real.instAdd Real.instOne smoothingFn Real.instNatCast asympBound	—	Asymptotics.isBigO_nat_atTop_induction_of_eventually_pos Filter.mp_mem eventually_one_add_smoothingFn_pos eventually_asympBound_pos Filter.univ_mem' le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Filter.Eventually.of_forall T_pos Finite.of_fintype Nat.instAtLeastTwoHAddOfNat bi_min_div_two_pos eventually_atTop_sumTransform_le Filter.eventually_ge_atTop eventually_bi_mul_le_r eventually_one_sub_smoothingFn_gt_const Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo rpow_p_mul_one_add_smoothingFn_ge IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Nat.le_ceil mul_comm div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono g_nonneg Nat.cast_nonneg' mul_add Distrib.leftDistribClass Finset.mul_sum add_le_add_left covariant_swap_add_of_covariant_add Finset.sum_le_sum mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing a_pos Finset.sum_congr asympBound_def' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono add_nonneg zero_le_one Finset.sum_nonneg div_nonneg_iff Real.rpow_nonneg eq_sub_of_add_eq add_comm add_eq_of_eq_sub Finset.sum_Ico_eq_sub r_lt_n LE.le.trans 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 sub_le_sub_left b_pos Real.rpow_pos_of_pos sumCoeffsExp_p_eq_one mul_one Mathlib.Tactic.Ring.mul_one add_le_add_right mul_nonneg sub_nonneg one_add_smoothingFn_le_two Mathlib.Tactic.Ring.cast_zero Nat.cast_zero

---

← Back to Index