GrowsPolynomially

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

Statistics

Metric	Count
Definitions `GrowsPolynomially`	1
Theorems `abs`, `add`, `add_isLittleO`, `congr_of_eventuallyEq`, `const_mul`, `div`, `eventually_atTop_ge`, `eventually_atTop_ge_nat`, `eventually_atTop_le`, `eventually_atTop_le_nat`, `eventually_atTop_nonneg_or_nonpos`, `eventually_atTop_zero_or_pos_or_neg`, `eventually_zero_of_frequently_zero`, `iff_eventuallyEq`, `inv`, `mul`, `neg`, `neg_iff`, `norm`, `of_isEquivalent`, `of_isEquivalent_const`, `of_isTheta`, `pow`, `rpow`, `zpow`, `growsPolynomially_const`, `growsPolynomially_id`, `growsPolynomially_log`, `growsPolynomially_pow`, `growsPolynomially_rpow`, `growsPolynomially_zpow`	31
Total	32

AkraBazziRecurrence

Definitions

Name	Category	Theorems
`GrowsPolynomially` 📖	MathDef	14 math math: `GrowsPolynomially.of_isEquivalent_const`, `growsPolynomially_id`, `growsPolynomially_const`, `growsPolynomially_pow`, `growsPolynomially_one_add_smoothingFn`, `GrowsPolynomially.iff_eventuallyEq`, `GrowsPolynomially.neg_iff`, `growsPolynomially_rpow`, `growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn`, `growsPolynomially_one_sub_smoothingFn`, `growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn`, `growsPolynomially_zpow`, `growsPolynomially_log`, `g_grows_poly`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`growsPolynomially_const` 📖	mathematical	—	`GrowsPolynomially`	—	`Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Nat.cast_one` `Filter.univ_mem'` `one_mul` `Set.Icc_self`
`growsPolynomially_id` 📖	mathematical	—	`GrowsPolynomially`	—	`Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Nat.cast_one` `Filter.univ_mem'` `one_mul`
`growsPolynomially_log` 📖	mathematical	—	`GrowsPolynomially` `Real.log`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isNNRat_lt_true` `Real.instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `Filter.Tendsto.const_mul_atTop` `Real.tendsto_log_atTop` `Filter.mp_mem` `Filter.Tendsto.eventually_forall_ge_atTop` `Filter.tendsto_id` `Filter.Tendsto.eventually` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instNontrivial` `Filter.univ_mem'` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `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.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.atom_pf` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `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.Tactic.Ring.neg_zero` `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.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` `Real.log_mul` `ne_of_gt` `lt_trans` `Mathlib.Meta.Positivity.pos_of_isNat` `mul_comm` `Real.log_le_log` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `one_mul`
`growsPolynomially_pow` 📖	mathematical	—	`GrowsPolynomially` `Real` `Monoid.toNatPow` `Real.instMonoid`	—	`GrowsPolynomially.pow` `growsPolynomially_id` `Filter.eventually_ge_atTop`
`growsPolynomially_rpow` 📖	mathematical	—	`GrowsPolynomially` `Real` `Real.instPow`	—	`GrowsPolynomially.rpow` `growsPolynomially_id` `Filter.eventually_ge_atTop`
`growsPolynomially_zpow` 📖	mathematical	—	`GrowsPolynomially` `Real` `DivInvMonoid.toZPow` `Real.instDivInvMonoid`	—	`GrowsPolynomially.zpow` `growsPolynomially_id` `Filter.eventually_ge_atTop`

AkraBazziRecurrence.GrowsPolynomially

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially`	`abs` `Real` `Real.lattice` `Real.instAddGroup`	—	`eventually_atTop_nonneg_or_nonpos` `Filter.mp_mem` `Filter.univ_mem'` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `iff_eventuallyEq` `abs_of_nonpos` `neg`
`add` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially` `Filter.EventuallyLE` `Real` `Real.instLE` `Filter.atTop` `Real.instPreorder` `Pi.instZero` `Real.instZero`	`Real.instAdd`	—	`lt_min` `lt_max_of_lt_left` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.Tendsto.eventually_forall_ge_atTop` `Filter.Tendsto.const_mul_atTop` `Real.instIsStrictOrderedRing` `Filter.tendsto_id` `Filter.univ_mem'` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `le_of_lt` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `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` `mul_add` `Distrib.leftDistribClass` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `min_le_left` `min_le_right` `le_max_left` `le_max_right`
`add_isLittleO` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially` `Asymptotics.IsLittleO` `Real` `Real.norm` `Filter.atTop` `Real.instPreorder`	`Real.instAdd`	—	`eventually_atTop_nonneg_or_nonpos` `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` `mul_pos` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.Tendsto.eventually_forall_ge_atTop` `Filter.Tendsto.const_mul_atTop` `Filter.tendsto_id` `Asymptotics.isLittleO_iff` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Filter.univ_mem'` `one_mul` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `le_of_lt` `Real.norm_of_nonneg` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.le_norm_self` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `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.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.add_pf_zero_add` `sub_eq_add_neg` `Real.norm_eq_abs` `neg_abs_le` `sub_le_sub_left` `covariant_swap_add_of_covariant_add` `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.Tactic.Ring.neg_zero` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_add` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Mathlib.Tactic.Ring.mul_pf_left` `Real.norm_of_nonpos` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsNat.to_isInt` `le_of_neg_le_neg` `neg_neg` `neg_mul` `neg_div`
`congr_of_eventuallyEq` 📖	—	`Filter.EventuallyEq` `Real` `Filter.atTop` `Real.instPreorder` `AkraBazziRecurrence.GrowsPolynomially`	—	—	`Filter.mp_mem` `Filter.Tendsto.eventually_forall_ge_atTop` `Filter.Tendsto.const_mul_atTop` `Real.instIsStrictOrderedRing` `Filter.tendsto_id` `Filter.univ_mem'`
`const_mul` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially`	`Real` `Real.instMul`	—	`mul` `AkraBazziRecurrence.growsPolynomially_const`
`div` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially`	`Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`div_eq_mul_inv` `mul` `inv`
`eventually_atTop_ge` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instZero` `Real.instOne` `AkraBazziRecurrence.GrowsPolynomially`	`Real.instLT` `Filter.Eventually` `Filter.atTop`	—	`Filter.mp_mem` `Filter.univ_mem'`
`eventually_atTop_ge_nat` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instZero` `Real.instOne` `AkraBazziRecurrence.GrowsPolynomially`	`Real.instLT` `Filter.Eventually` `Filter.atTop` `Nat.instPreorder`	—	`eventually_atTop_ge` `Filter.Eventually.natCast_atTop` `Real.instIsOrderedRing` `Real.instArchimedean`
`eventually_atTop_le` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instZero` `Real.instOne` `AkraBazziRecurrence.GrowsPolynomially`	`Real.instLT` `Filter.Eventually` `Filter.atTop`	—	`Filter.mp_mem` `Filter.univ_mem'`
`eventually_atTop_le_nat` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instZero` `Real.instOne` `AkraBazziRecurrence.GrowsPolynomially`	`Real.instLT` `Filter.Eventually` `Filter.atTop` `Nat.instPreorder`	—	`eventually_atTop_le` `Filter.Eventually.natCast_atTop` `Real.instIsOrderedRing` `Real.instArchimedean`
`eventually_atTop_nonneg_or_nonpos` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially`	`Filter.Eventually` `Real` `Real.instLE` `Real.instZero` `Filter.atTop` `Real.instPreorder`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `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.isNNRat_lt_true` `Real.instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Nat.cast_zero` `lt_trichotomy` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `Set.mem_Icc` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isRat_le_true` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `le_of_not_gt` `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.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.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `CancelDenoms.derive_trans` `CancelDenoms.sub_subst` `CancelDenoms.mul_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Meta.NormNum.isNat_lt_true` `Set.nonempty_of_mem` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_gt` `Set.nonempty_Icc` `nonneg_of_mul_nonneg_right` `IsStrictOrderedRing.toPosMulStrictMono` `lt_of_not_ge` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `nonpos_of_mul_nonpos_right` `Filter.eventually_atTop` `instIsDirectedOrder` `Real.instArchimedean` `Set.Icc_self` `Real.induction_Ico_mul` `lt_max_of_lt_right` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `one_le_pow₀` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Mathlib.Meta.NormNum.isNat_le_true` `le_or_gt` `le_of_lt`
`eventually_atTop_zero_or_pos_or_neg` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially`	`Filter.Eventually` `Real` `Real.instZero` `Filter.atTop` `Real.instPreorder` `Real.instLT`	—	`eventually_zero_of_frequently_zero` `eventually_atTop_nonneg_or_nonpos` `Filter.eventually_and` `Filter.mp_mem` `Filter.univ_mem'`
`eventually_zero_of_frequently_zero` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially` `Filter.Frequently` `Real` `Real.instZero` `Filter.atTop` `Real.instPreorder`	`Filter.Eventually`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `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.isNNRat_lt_true` `Real.instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Nat.cast_zero` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.eventually_forall_ge_atTop` `Filter.univ_mem'` `Filter.frequently_atTop` `instIsDirectedOrder` `Real.instArchimedean` `Mathlib.Meta.NormNum.isNat_lt_true` `le_of_max_le_right` `CharP.cast_eq_zero` `CharP.ofCharZero` `Int.instCharZero` `neg_zero` `zero_sub` `zpow_zero` `one_mul` `MulZeroClass.mul_zero` `Set.Icc_self` `le_of_max_le_left` `one_div` `zpow_neg` `zpow_one` `neg_add` `Nat.cast_add` `Set.left_mem_Icc` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `zpow_le_zpow_right₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instZeroLEOneClass` `Mathlib.Meta.NormNum.isNat_le_true` `le_of_lt` `zpow_neg_one` `mul_assoc` `zpow_add₀` `Mathlib.Meta.NormNum.isNat_eq_false` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `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.atom_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `le_rfl` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.logb_le_logb` `zpow_pos` `div_pos` `Real.rpow_intCast` `Real.logb_rpow` `neg_le_neg_iff` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Int.cast_sub` `Int.cast_neg` `Int.cast_natCast` `Int.cast_one` `neg_sub` `sub_neg_eq_add` `Nat.le_ceil` `add_comm` `Nat.ceil_le_floor_add_one` `div_le_iff₀` `neg_neg` `neg_nonneg` `Real.logb_nonpos` `div_le_one` `Nat.floor_le`
`iff_eventuallyEq` 📖	mathematical	`Filter.EventuallyEq` `Real` `Filter.atTop` `Real.instPreorder`	`AkraBazziRecurrence.GrowsPolynomially`	—	`congr_of_eventuallyEq` `Filter.EventuallyEq.symm`
`inv` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially`	`Real` `Real.instInv`	—	`eventually_atTop_zero_or_pos_or_neg` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Filter.mp_mem` `Filter.Tendsto.eventually_forall_ge_atTop` `Filter.Tendsto.const_mul_atTop` `Real.instIsStrictOrderedRing` `Filter.tendsto_id` `Filter.univ_mem'` `inv_zero` `MulZeroClass.mul_zero` `Set.Icc_self` `ne_of_lt` `ne_of_gt` `abs_inv` `abs` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `abs_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_inv` `inv_anti₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `mul_pos` `Mathlib.Meta.Positivity.abs_pos_of_ne_zero` `abs_of_nonneg` `inv_nonneg_of_nonneg` `le_of_lt` `iff_eventuallyEq` `abs_of_nonpos` `inv_nonpos` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `neg_neg` `neg`
`mul` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially`	`Real` `Real.instMul`	—	`abs` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Filter.mp_mem` `Filter.univ_mem'` `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` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `mul_nonneg` `le_of_lt` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `eventually_atTop_nonneg_or_nonpos` `abs_of_nonneg` `iff_eventuallyEq` `abs_of_nonpos` `mul_neg` `neg_mul` `neg_neg` `neg`
`neg` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially`	`Pi.instNeg` `Real` `Real.instNeg`	—	`Filter.mp_mem` `Filter.univ_mem'` `Real.instIsOrderedAddMonoid` `neg_mul_eq_mul_neg` `neg_neg`
`neg_iff` 📖	mathematical	—	`AkraBazziRecurrence.GrowsPolynomially` `Pi.instNeg` `Real` `Real.instNeg`	—	`neg` `neg_neg`
`norm` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially`	`Norm.norm` `Real` `Real.norm`	—	`abs`
`of_isEquivalent` 📖	—	`AkraBazziRecurrence.GrowsPolynomially` `Asymptotics.IsEquivalent` `Real` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Filter.atTop` `Real.instPreorder`	—	—	`add_sub_cancel` `add_isLittleO`
`of_isEquivalent_const` 📖	mathematical	`Asymptotics.IsEquivalent` `Real` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Filter.atTop` `Real.instPreorder`	`AkraBazziRecurrence.GrowsPolynomially`	—	`of_isEquivalent` `AkraBazziRecurrence.growsPolynomially_const`
`of_isTheta` 📖	—	`AkraBazziRecurrence.GrowsPolynomially` `Asymptotics.IsTheta` `Real` `Real.norm` `Filter.atTop` `Real.instPreorder` `Filter.Eventually` `Real.instLE` `Real.instZero`	—	—	`Asymptotics.isBigO_iff''` `Asymptotics.IsTheta.isBigO_symm` `Asymptotics.isBigO_iff'` `Asymptotics.IsTheta.isBigO` `norm` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `inv_mul_cancel₀` `ne_of_gt` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.Tendsto.eventually_forall_ge_atTop` `Filter.Tendsto.const_mul_atTop` `Filter.tendsto_id` `Filter.univ_mem'` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `le_of_lt` `one_mul` `Real.norm_of_nonneg` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.inv_congr` `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` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `mul_one`
`pow` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially` `Filter.Eventually` `Real` `Real.instLE` `Real.instZero` `Filter.atTop` `Real.instPreorder`	`Monoid.toNatPow` `Real.instMonoid`	—	`rpow`
`rpow` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially` `Filter.Eventually` `Real` `Real.instLE` `Real.instZero` `Filter.atTop` `Real.instPreorder`	`Real.instPow`	—	`Real.rpow_pos_of_pos` `le_or_gt` `Filter.mp_mem` `Filter.Tendsto.eventually_forall_ge_atTop` `Filter.Tendsto.const_mul_atTop` `Real.instIsStrictOrderedRing` `Filter.tendsto_id` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.univ_mem'` `Real.mul_rpow` `le_of_lt` `Real.rpow_le_rpow` `mul_nonneg` `IsOrderedRing.toPosMulMono` `eventually_atTop_zero_or_pos_or_neg` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Nat.cast_one` `Real.zero_rpow` `ne_of_lt` `MulZeroClass.mul_zero` `Set.Icc_self` `Real.rpow_le_rpow_of_nonpos` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `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.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_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Filter.NeBot.ne` `Filter.atTop_neBot` `instIsDirectedOrder` `Real.instArchimedean` `Filter.eventually_false_iff_eq_bot`
`zpow` 📖	mathematical	`AkraBazziRecurrence.GrowsPolynomially` `Filter.Eventually` `Real` `Real.instLE` `Real.instZero` `Filter.atTop` `Real.instPreorder`	`DivInvMonoid.toZPow` `Real.instDivInvMonoid`	—	`rpow`

---

← Back to Index