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.toPow 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.toPow 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 Real Real.norm Filter.atTop Nat.instPreorder Real.instSub Real.instNatCast Real.instMul 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	—	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 Mathlib.Tactic.Ring.cast_zero Nat.cast_zero

---

← Back to Index