Chebyshev

📁 Source: Mathlib/NumberTheory/Chebyshev.lean

Statistics

Metric	Count
Definitions `psi`, `termθ`, `termψ`, `theta`	4
Theorems `abs_psi_sub_theta_le_sqrt_mul_log`, `eventually_primeCounting_le`, `integrableOn_theta_div_id_mul_log_sq`, `integral_one_div_log_sq_isBigO`, `integral_theta_div_log_sq_isBigO`, `integral_theta_div_log_sq_isLittleO`, `intervalIntegrable_one_div_log_sq`, `primeCounting_eq_theta_div_log_add_integral`, `primeCounting_sub_theta_div_log_isBigO`, `psi_eq_psi_coe_floor`, `psi_eq_sum_Icc`, `psi_eq_sum_theta`, `psi_eq_theta_add_sum_theta`, `psi_eq_zero_of_lt_two`, `psi_le`, `psi_le_const_mul_self`, `psi_mono`, `psi_nonneg`, `psi_sub_theta_eq_sum_not_prime`, `sum_PrimePow_eq_sum_sum`, `theta_eq_log_primorial`, `theta_eq_sum_Icc`, `theta_eq_theta_coe_floor`, `theta_eq_zero_of_lt_two`, `theta_le_log4_mul_x`, `theta_le_psi`, `theta_mono`, `theta_nonneg`, `theta_pos`	29
Total	33

Chebyshev

Definitions

Name	Category	Theorems
`psi` 📖	CompOp	12 math math: `abs_psi_sub_theta_le_sqrt_mul_log`, `psi_eq_psi_coe_floor`, `psi_eq_sum_theta`, `psi_sub_theta_eq_sum_not_prime`, `psi_eq_zero_of_lt_two`, `psi_eq_theta_add_sum_theta`, `psi_le`, `psi_eq_sum_Icc`, `psi_nonneg`, `psi_mono`, `theta_le_psi`, `psi_le_const_mul_self`
`termθ` 📖	CompOp	—
`termψ` 📖	CompOp	—
`theta` 📖	CompOp	18 math math: `theta_eq_theta_coe_floor`, `abs_psi_sub_theta_le_sqrt_mul_log`, `theta_eq_zero_of_lt_two`, `psi_eq_sum_theta`, `psi_sub_theta_eq_sum_not_prime`, `primeCounting_eq_theta_div_log_add_integral`, `integrableOn_theta_div_id_mul_log_sq`, `primeCounting_sub_theta_div_log_isBigO`, `theta_eq_log_primorial`, `theta_mono`, `psi_eq_theta_add_sum_theta`, `theta_eq_sum_Icc`, `theta_nonneg`, `theta_le_log4_mul_x`, `integral_theta_div_log_sq_isBigO`, `integral_theta_div_log_sq_isLittleO`, `theta_le_psi`, `theta_pos`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_psi_sub_theta_le_sqrt_mul_log` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `psi` `theta` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.sqrt` `Real.log`	—	`Nat.instAtLeastTwoHAddOfNat` `psi_eq_zero_of_lt_two` `theta_eq_zero_of_lt_two` `sub_zero` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `zero_le_two` `Real.instZeroLEOneClass` `Real.log_nonneg` `Real.instIsStrictOrderedRing` `psi_eq_theta_add_sum_theta` `add_sub_cancel_left` `le_trans` `Finset.abs_sum_le_sum_abs` `Finset.sum_congr` `abs_of_nonneg` `theta_nonneg` `Finset.sum_le_sum` `theta_le_log4_mul_x` `Real.rpow_nonneg` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.neg_congr` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.sqrt_eq_rpow` `mul_le_mul_of_nonneg_left` `Real.rpow_le_rpow_of_exponent_le` `div_le_div₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `le_refl` `Mathlib.Meta.Positivity.log_pos_of_isNat` `Finset.sum_const` `Nat.card_Icc` `nsmul_eq_mul` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Nat.cast_sub` `Nat.le_floor` `one_le_div` `Real.log_pos` `Real.log_le_log` `zero_lt_two` `NeZero.charZero_one` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Linarith.without_one_mul` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_natCast` `CancelDenoms.sub_subst` `Nat.floor_le` `div_nonneg` `Mathlib.Meta.NormNum.isNat_le_true` `mul_pos` `Real.sqrt_pos_of_pos` `lt_of_lt_of_le` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Real.log_pow` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero`
`eventually_primeCounting_le` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter.Eventually` `Real.instLE` `Real.instNatCast` `Nat.primeCounting` `Nat.floor` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Real.instAdd` `Real.log` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Filter.atTop` `Real.instPreorder`	—	`Nat.instAtLeastTwoHAddOfNat` `Asymptotics.IsLittleO.bound` `integral_theta_div_log_sq_isLittleO` `Filter.mp_mem` `Real.instIsStrictOrderedRing` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `primeCounting_eq_theta_div_log_add_integral` `add_mul` `Distrib.rightDistribClass` `add_div` `Real.log_nonneg` `le_of_not_gt` `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.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `theta_le_log4_mul_x` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `le_refl` `add_le_add_right` `mul_div_assoc` `Real.norm_of_nonneg` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono`
`integrableOn_theta_div_id_mul_log_sq` 📖	mathematical	—	`MeasureTheory.IntegrableOn` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `theta` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.log` `Set.Icc` `Real.instPreorder` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.MeasureSpace.volume`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.instIsStrictOrderedRing` `theta.eq_1` `div_eq_mul_one_div` `mul_comm` `Finset.sum_filter` `integrableOn_mul_sum_Icc` `Mathlib.Meta.NormNum.isNat_le_true` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.instAtLeastTwo` `ContinuousOn.integrableOn_Icc` `BorelSpace.opensMeasurable` `Real.borelSpace` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousAt.continuousWithinAt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.neg_congr` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.atom_pf` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_mul` `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` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `sub_eq_zero_of_eq` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_ne_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `isReduced_of_noZeroDivisors` `Nat.instCharZero` `ContinuousAt.div₀` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuousAt_const` `ContinuousAt.fun_mul` `continuousAt_id'` `ContinuousAt.comp'` `ContinuousAt.pow` `ContinuousAt.log`
`integral_one_div_log_sq_isBigO` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `Real.norm` `Filter.atTop` `Real.instPreorder` `intervalIntegral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Monoid.toNatPow` `Real.instMonoid` `Real.log` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`Asymptotics.IsBigO.trans` `Nat.instAtLeastTwoHAddOfNat` `Asymptotics.IsBigO.of_bound'` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `le_trans` `intervalIntegral.abs_integral_le_integral_abs` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.neg_congr` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `intervalIntegral.integral_congr` `one_div` `abs_inv` `abs_pow` `sq_abs` `le_imp_le_of_le_of_le` `le_refl` `Real.norm_of_nonneg` `le_of_lt` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `mul_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `lt_of_lt_of_le` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `div_pos` `Real.sqrt_pos_of_pos` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.log_pos_of_isNat` `Asymptotics.IsBigO.add` `mul_div_assoc` `Asymptotics.isBigO_const_mul_self` `mul_one_div` `mul_comm` `Asymptotics.IsBigO.const_mul_left` `Asymptotics.IsLittleO.isBigO`
`integral_theta_div_log_sq_isBigO` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `Real.norm` `Filter.atTop` `Real.instPreorder` `intervalIntegral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `theta` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.log` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`Asymptotics.IsBigO.trans` `Nat.instAtLeastTwoHAddOfNat` `Asymptotics.IsBigO.of_bound` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `intervalIntegral.abs_integral_le_integral_abs` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.neg_congr` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `intervalIntegral.integral_mono_on` `IntervalIntegrable.abs` `intervalIntegrable_iff` `PseudoEMetricSpace.pseudoMetrizableSpace` `Set.uIoc_of_le` `integrableOn_Icc_iff_integrableOn_Ioc` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Real.noAtoms_volume` `enorm_ne_top` `integrableOn_theta_div_id_mul_log_sq` `IntervalIntegrable.const_mul` `intervalIntegrable_one_div_log_sq` `lt_of_not_ge` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `theta_nonneg` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `mul_nonneg` `IsOrderedRing.toPosMulMono` `le_of_lt` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `le_imp_le_of_le_of_le` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `theta_le_log4_mul_x` `le_refl` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Mathlib.Meta.Positivity.log_pos_of_isNat` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.mul_pf_right` `intervalIntegral.integral_const_mul` `intervalIntegral.integral_nonneg` `Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg` `integral_one_div_log_sq_isBigO`
`integral_theta_div_log_sq_isLittleO` 📖	mathematical	—	`Asymptotics.IsLittleO` `Real` `Real.norm` `Filter.atTop` `Real.instPreorder` `intervalIntegral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `theta` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.log` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`Asymptotics.IsBigO.trans_isLittleO` `Nat.instAtLeastTwoHAddOfNat` `integral_theta_div_log_sq_isBigO` `Asymptotics.isLittleO_iff_tendsto'` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Nat.instCharZero` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `Filter.Tendsto.congr'` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instNontrivial` `Filter.univ_mem'` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `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` `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_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Filter.Tendsto.inv_tendsto_atTop` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `Real.tendsto_log_atTop`
`intervalIntegrable_one_div_log_sq` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`IntervalIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Real.log` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`ContinuousOn.intervalIntegrable` `Real.locallyFinite_volume` `ContinuousAt.continuousWithinAt` `Set.mem_uIcc` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.log_ne_zero` `ContinuousAt.div₀` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuousAt_const` `ContinuousAt.comp'` `ContinuousAt.pow` `continuousAt_id'` `ContinuousAt.log`
`primeCounting_eq_theta_div_log_add_integral` 📖	mathematical	`Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Nat.primeCounting` `Nat.floor` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing` `Real.instAdd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `theta` `Real.log` `intervalIntegral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.instIsStrictOrderedRing` `Nat.count_eq_card_filter_range` `Finset.card_eq_sum_ones` `Nat.range_succ_eq_Icc_zero` `Finset.sum_filter` `Nat.cast_sum` `Finset.sum_congr` `Nat.cast_ite` `Nat.cast_one` `Nat.cast_zero` `Real.log_ne_zero_of_pos_of_ne_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Nat.Prime.pos` `Nat.Prime.ne_one` `Set.indicator_of_mem` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Set.indicator_of_notMem` `MulZeroClass.mul_zero` `sum_mul_eq_sub_integral_mul₁` `CharP.cast_eq_zero` `CharP.ofCharZero` `Real.log_zero` `Real.log_one` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `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.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `sub_eq_zero_of_eq` `lt_of_not_ge` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.add_pf_add_gt` `DifferentiableAt.fun_inv` `DifferentiableAt.log` `differentiableAt_id` `ContinuousOn.integrableOn_Icc` `BorelSpace.opensMeasurable` `Real.borelSpace` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousWithinAt.congr` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `ContinuousAt.continuousWithinAt` `ContinuousAt.div₀` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAt.neg` `IsTopologicalRing.toContinuousNeg` `ContinuousAt.inv₀` `continuousAt_id'` `ContinuousAt.comp'` `ContinuousAt.pow` `ContinuousAt.log` `Real.deriv_inv_log` `intervalIntegral.integral_of_le` `intervalIntegral.integral_congr` `mul_inv_rev` `mul_neg` `neg_div` `neg_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Set.indicator_apply` `intervalIntegral.integral_neg` `sub_neg_eq_add` `theta_eq_sum_Icc`
`primeCounting_sub_theta_div_log_isBigO` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `Real.norm` `Filter.atTop` `Real.instPreorder` `Real.instSub` `Real.instNatCast` `Nat.primeCounting` `Nat.floor` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `theta` `Real.log` `Monoid.toNatPow` `Real.instMonoid`	—	`Asymptotics.IsBigO.congr'` `Nat.instAtLeastTwoHAddOfNat` `Real.instIsStrictOrderedRing` `integral_theta_div_log_sq_isBigO` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `primeCounting_eq_theta_div_log_add_integral` `add_sub_cancel_left` `Filter.EventuallyEq.refl`
`psi_eq_psi_coe_floor` 📖	mathematical	—	`psi` `Real` `Real.instNatCast` `Nat.floor` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing`	—	`Real.instIsStrictOrderedRing` `Nat.floor_natCast`
`psi_eq_sum_Icc` 📖	mathematical	—	`psi` `Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.Icc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Nat.floor` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing` `DFunLike.coe` `ArithmeticFunction` `Real.instZero` `ArithmeticFunction.instFunLikeNat` `ArithmeticFunction.vonMangoldt`	—	`Real.instIsStrictOrderedRing` `psi.eq_1` `Finset.add_sum_Ioc_eq_sum_Icc` `Nat.instCanonicallyOrderedAdd` `ArithmeticFunction.map_zero` `zero_add`
`psi_eq_sum_theta` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`psi` `Finset.sum` `Real.instAddCommMonoid` `Finset.Icc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Nat.floor` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.log` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `theta` `Real.instPow` `Real.instOne`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `Finset.sum_congr` `sum_PrimePow_eq_sum_sum` `Nat.Prime.pow_minFac` `Finset.filter.congr_simp` `one_div` `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` `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.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_mul` `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` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `sub_eq_zero_of_eq` `Nat.cast_zero` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Nat.cast_one` `Finset.mem_Icc`
`psi_eq_theta_add_sum_theta` 📖	mathematical	`Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`psi` `Real.instAdd` `theta` `Finset.sum` `Real.instAddCommMonoid` `Finset.Icc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Nat.floor` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.log` `Real.instPow` `Real.instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.instIsStrictOrderedRing` `psi_eq_sum_theta` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.neg_congr` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Finset.add_sum_Ioc_eq_sum_Icc` `Nat.le_floor_iff'` `one_ne_zero` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Mathlib.Meta.Positivity.log_pos_of_isNat` `one_mul` `Real.log_le_log` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `div_self` `NeZero.charZero_one` `Real.rpow_one`
`psi_eq_zero_of_lt_two` 📖	mathematical	`Real` `Real.instLT` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`psi` `Real.instZero`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.sum_eq_zero` `Real.instIsStrictOrderedRing` `lt_of_le_of_lt` `Nat.le_floor_iff'` `LT.lt.ne` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `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` `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` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Nat.cast_zero` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `ArithmeticFunction.vonMangoldt_apply_one`
`psi_le` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`psi` `Real.instAdd` `Real.instMul` `Real.log` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.sqrt`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `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_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `le_trans` `le_abs_self` `abs_psi_sub_theta_le_sqrt_mul_log` `theta_le_log4_mul_x` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Linarith.add_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Meta.NormNum.instAtLeastTwo` `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.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_gt`
`psi_le_const_mul_self` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`psi` `Real.instMul` `Real.instAdd` `Real.log` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `psi_eq_zero_of_lt_two` `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.atom_pf` `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` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_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` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_nonneg` `IsOrderedRing.toPosMulMono` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.log_nonneg` `Mathlib.Meta.NormNum.isNat_le_true` `le_trans` `psi_le` `add_mul` `Distrib.rightDistribClass` `add_le_add_right` `Real.sqrt_eq_rpow` `le_imp_le_of_le_of_le` `mul_le_mul_of_nonneg_left` `Real.log_le_rpow_div` `le_of_not_gt` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Meta.NormNum.isNat_lt_true` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Real.rpow_pos_of_pos` `lt_of_lt_of_le` `le_refl` `mul_div_assoc` `mul_one_div` `mul_assoc` `Real.rpow_add` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNNRat_add` `Real.rpow_one` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Meta.NormNum.IsNat.to_raw_eq`
`psi_mono` 📖	mathematical	—	`Monotone` `Real` `Real.instPreorder` `psi`	—	`Finset.sum_le_sum_of_subset_of_nonneg` `Real.instIsStrictOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Finset.Ioc_subset_Ioc` `le_refl` `Nat.floor_le_floor`
`psi_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `psi`	—	`Finset.sum_nonneg` `Real.instIsStrictOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`psi_sub_theta_eq_sum_not_prime` 📖	mathematical	—	`Real` `Real.instSub` `psi` `theta` `Finset.sum` `Real.instAddCommMonoid` `Finset.filter` `Nat.Prime` `Nat.decidablePrime` `Finset.Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Nat.floor` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing` `DFunLike.coe` `ArithmeticFunction` `Real.instZero` `ArithmeticFunction.instFunLikeNat` `ArithmeticFunction.vonMangoldt`	—	`Real.instIsStrictOrderedRing` `psi.eq_1` `theta.eq_1` `Finset.sum_filter` `Finset.sum_sub_distrib` `Finset.sum_congr` `ArithmeticFunction.vonMangoldt_apply_prime` `sub_self` `sub_zero`
`sum_PrimePow_eq_sum_sum` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Finset.sum` `Finset.filter` `IsPrimePow` `Nat.instCommMonoidWithZero` `instDecidableIsPrimePowNat` `Finset.Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Nat.floor` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing` `Finset.Icc` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.log` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Nat.Prime` `Nat.decidablePrime` `Real.instPow` `Real.instOne` `Monoid.toNatPow` `Nat.instMonoid`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `Finset.sum_bij` `Finset.filter.congr_simp` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `Nat.cast_pow` `Real.instIsOrderedRing` `Real.instNontrivial` `Real.rpow_natCast` `Nat.Prime.pow_inj'` `Nat.le_floor` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.log_pos` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.log_pow` `Real.log_le_log` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instZeroLEOneClass` `LE.le.trans` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `Mathlib.Meta.NormNum.isNat_le_true` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.Prime.two_le` `Prime.nat_prime` `Nat.Prime.pos` `le_self_pow₀` `Nat.Prime.one_le` `LT.lt.ne'` `Finset.sum_filter` `Finset.sum_product` `Finset.sum_congr` `Finset.sum_ite` `Finset.sum_const_zero` `add_zero` `Finset.ext` `one_div` `le_imp_le_of_le_of_le` `le_refl` `Nat.floor_le_floor` `Real.rpow_le_self_of_one_le` `Nat.one_le_floor_iff` `le_trans` `Nat.one_le_cast` `Nat.instIsOrderedAddMonoid` `Nat.instCharZero` `Mathlib.Tactic.Contrapose.contrapose₁` `Real.rpow_lt_one` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Tactic.Bound.Nat.cast_pos_of_pos` `inv_le_one_of_one_le₀` `Mathlib.Tactic.Bound.Nat.one_le_cast_of_le`
`theta_eq_log_primorial` 📖	mathematical	—	`theta` `Real.log` `Real` `Real.instNatCast` `primorial` `Nat.floor` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing`	—	`Real.instIsStrictOrderedRing` `Nat.cast_prod` `Real.log_prod` `Nat.cast_zero` `RCLike.charZero_rclike` `LT.lt.ne'` `Nat.Prime.pos` `Finset.mem_filter` `Finset.ext` `Nat.instNoMaxOrder`
`theta_eq_sum_Icc` 📖	mathematical	—	`theta` `Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.filter` `Nat.Prime` `Nat.decidablePrime` `Finset.Icc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Nat.floor` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing` `Real.log` `Real.instNatCast`	—	`Real.instIsStrictOrderedRing` `theta.eq_1` `Finset.sum_filter` `Finset.add_sum_Ioc_eq_sum_Icc` `Nat.instCanonicallyOrderedAdd` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `Real.log_zero` `zero_add`
`theta_eq_theta_coe_floor` 📖	mathematical	—	`theta` `Real` `Real.instNatCast` `Nat.floor` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing`	—	`Real.instIsStrictOrderedRing` `Nat.floor_natCast`
`theta_eq_zero_of_lt_two` 📖	mathematical	`Real` `Real.instLT` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`theta` `Real.instZero`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.sum_eq_zero` `Real.instIsStrictOrderedRing` `lt_of_le_of_lt` `Nat.le_floor_iff'` `LT.lt.ne` `Nat.cast_one` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `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` `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` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `Real.log_one`
`theta_le_log4_mul_x` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`theta` `Real.instMul` `Real.log` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.instIsStrictOrderedRing` `theta_eq_log_primorial` `Real.log_le_log` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `primorial_pos` `primorial_le_4_pow` `Real.log_pow` `mul_comm` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Nat.floor_le` `le_of_lt` `Mathlib.Meta.Positivity.log_pos_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo`
`theta_le_psi` 📖	mathematical	—	`Real` `Real.instLE` `theta` `psi`	—	`Nat.instAtLeastTwoHAddOfNat` `theta_eq_zero_of_lt_two` `psi_eq_zero_of_lt_two` `le_refl` `Real.instIsStrictOrderedRing` `psi_eq_theta_add_sum_theta` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Finset.sum_nonneg` `theta_nonneg`
`theta_mono` 📖	mathematical	—	`Monotone` `Real` `Real.instPreorder` `theta`	—	`Finset.sum_le_sum_of_subset_of_nonneg` `Real.instIsStrictOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Finset.filter_subset_filter` `Finset.Ioc_subset_Ioc_right` `Nat.floor_mono` `Real.log_nonneg` `Nat.cast_one` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Nat.Prime.one_le`
`theta_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `theta`	—	`Finset.sum_nonneg` `Real.instIsStrictOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.log_nonneg` `Real.instZeroLEOneClass` `RCLike.charZero_rclike`
`theta_pos` 📖	mathematical	`Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instLT` `Real.instZero` `theta`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.sum_pos` `Real.instIsOrderedCancelAddMonoid` `Real.instIsStrictOrderedRing` `Real.log_pos` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Nat.Prime.one_lt` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Nat.le_floor_iff` `Nat.prime_two`

---

← Back to Index