log 📖 | CompOp | 498 mathmath: Behrend.roth_lower_bound, Height.logHeight_eval_ge, HasStrictFDerivAt.log, le_log_one_add_of_nonneg, isBigO_log_mul_const_log_atTop, Polynomial.mahlerMeasure_def_of_ne_zero, Function.locallyFinsuppWithin.logCounting_single_eq_log_sub_const, Complex.ofNat_log, Complex.tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero, HasDerivAt.const_rpow, InformationTheory.integral_llr_add_mul_log_nonneg, not_continuousAt_inv_log_neg_one, Mathlib.Meta.Positivity.log_pos_of_isNat, log_le_self, Complex.log_re, sinh_log, Stirling.log_stirlingSeq_bounded_aux, range_log, DifferentiableWithinAt.log, HasStrictDerivAt.rpow, Continuous.log, ENNReal.log_pos_real', contDiffOn_log, hasDerivAt_sqrt_mul_log, deriv_negMulLog, deriv_binEntropy, rpow_eq_nhds_of_neg, le_log_of_zpow_le, log_div_le_sum_range_add, countingFunction_finsum_eq_finsum_add, log_sqrt, InformationTheory.mul_log_le_klDiv, posLog_norm_add_le, Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log, Stirling.log_stirlingSeq_sub_log_stirlingSeq_succ, Polynomial.logMahlerMeasure_C_mul, log_neg_natCast_nonneg, ContinuousAt.log, le_pow_iff_log_le, mul_log_nonneg, summable_log_one_add_of_summable, continuous_mul_log, log_prod, log_abs, deriv_log, Behrend.roth_lower_bound_explicit, circleAverage_log_norm_sub_const₁, NumberField.Units.regOfFamily_eq_det, AnalyticOnNhd.circleAverage_log_norm, Height.logHeight₁_sum_le, log_exp, Height.logHeight₁_add_le, hasSum_log_one_add_inv, differentiableOn_log, isLittleO_log_rpow_rpow_atTop, integral_log_sin_zero_pi_div_two, InformationTheory.rnDeriv_compProd_mul_log_eq_mul_add, BohrMollerup.le_logGammaSeq, rpow_def_of_pos, integral_inv_of_pos, log_add_one_le_harmonic, hasDerivAt_mul_log, log_mul_self_monotoneOn, Height.logHeight₁_sub_le, circleAverage_log_norm_sub_const_of_mem_closedBall, deriv_sqrt_mul_log, tendsto_mul_log_one_add_of_tendsto, hasStrictFDerivAt_rpow_of_pos, Stirling.log_stirlingSeq_formula, deriv.log, log_neg_eq_log, log_div_log, InformationTheory.klFun_apply, Behrend.log_two_mul_two_le_sqrt_log_eight, zpow_le_iff_le_log, rpow_inv_log, MeromorphicOn.extract_zeros_poles_log, isLittleO_log_id_atTop, surjOn_log', Chebyshev.psi_eq_sum_theta, Stirling.log_stirlingSeq_diff_hasSum, log_list_prod, Polynomial.logMahlerMeasure_of_degree_eq_one, zpow_lt_iff_lt_log, artanh_eq_half_log, continuousOn_log, Complex.hasDerivAt_GammaIntegral, circleAverage_log_norm_sub_const_eq_log_radius_add_posLog, not_continuousAt_deriv_mul_log_zero, ContinuousOn.log, log_two_near_10, Stirling.le_log_factorial_stirling, strictConcaveOn_log_Iio, mellin_hasDerivAt_of_isBigO_rpow, ProbabilityTheory.cgf_zero_fun, fderiv.log, UpperHalfPlane.dist_log_im_le, Complex.ofReal_log, pow_lt_iff_lt_log, AkraBazziRecurrence.eventually_deriv_one_add_smoothingFn, log_rpow, InformationTheory.hasDerivAt_klFun, continuous_log, log_neg_of_lt_zero, BohrMollerup.f_nat_eq, MeasureTheory.llr_tilted_right, ContDiff.log, AnalyticAt.log, hasSum_log_one_add, BohrMollerup.f_add_nat_ge, mellinInv_eq_fourierIntegralInv, strictConcaveOn_sqrt_mul_log_Ioi, Chebyshev.integral_one_div_log_sq_isBigO, Complex.natCast_log, isBigO_rpow_top_log_smul, le_zpow_iff_log_le, NumberField.Units.regulator_eq_det, InformationTheory.leftDeriv_klFun, le_exp_log, log_lt_iff_lt_exp, analyticOn_log, log_pos_iff, analyticOnNhd_log, log_nat_eq_sum_factorization, HasDerivWithinAt.const_rpow, mellinInv_eq_fourierInv, UpperHalfPlane.dist_of_re_eq, NumberField.Units.finrank_mul_regOfFamily_eq_det, intervalIntegral.intervalIntegrable_log, lt_log_iff_exp_lt, HasDerivAt.log, log_nonpos, AkraBazziRecurrence.isTheta_smoothingFn_sub_self, hasDerivAt_binEntropy, ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zero, hasDerivAt_qaryEntropy, Chebyshev.sum_PrimePow_eq_sum_sum, Behrend.lower_bound_le_one, DifferentiableAt.log, Complex.log_ofReal_mul, le_log_iff_exp_le, Stirling.log_stirlingSeq_diff_le, differentiableAt_log, deriv_inv_log, log_le_rpow_div, Chebyshev.primeCounting_eq_theta_div_log_add_integral, AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_sub_smoothingFn, posLog_sub_posLog_inv, ValueDistribution.characteristic_sub_characteristic_inv_at_zero, tendsto_harmonic_sub_log, ValueDistribution.proximity_sum_top_le, circleAverage_log_norm_sub_const₀, isBigO_log_const_mul_log_atTop, Projectivization.logHeight_eq_log_mulHeight, Polynomial.intervalIntegrable_mahlerMeasure, ENNReal.log_of_nnreal, deriv_log', log_zpow, DifferentiableOn.log, log_of_pos, log_two_gt_d9, Mathlib.Meta.Positivity.log_pos_of_isNNRat, HasStrictFDerivAt.rpow, rpow_def_of_neg, Function.Periodic.im_invQParam, MeasureTheory.integral_llr_tilted_left, lt_log_of_rpow_lt, Mathlib.Meta.Positivity.log_pos_of_isRat_neg, contDiffAt_log, leftDeriv_mul_log, circleIntegrable_log_norm_factorizedRational, ENNReal.log_pos_real, posLog_eq_log, log_one, strictConvexOn_mul_log, Chebyshev.integrableOn_theta_div_id_mul_log_sq, BohrMollerup.f_add_nat_le, hasStrictDerivAt_log, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, abs_log_sub_add_sum_range_le, log_pos, differentiableOn_mul_log, norm_inv_mul_rpow_sub_one_sub_log_le, ValueDistribution.proximity_add_top_le, AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_add_smoothingFn, deriv_qaryEntropy, HasDerivWithinAt.rpow, ProbabilityTheory.lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self, harmonic_le_one_add_log, isBigO_logb_mul_const_log_atTop, tendsto_rpow_sub_one_log, differentiableAt_log_iff, convexOn_log_Gamma, IntervalIntegrable.log, HasFDerivWithinAt.log, log_eq_zero, ArithmeticFunction.log_apply, neg_inv_le_log, Asymptotics.IsEquivalent.log, Summable.summable_log_norm_one_add, hasStrictDerivAt_const_rpow_of_neg, log_lt_sub_one_of_pos, sum_range_le_log_div, log_lt_log, Chebyshev.primeCounting_sub_theta_div_log_isBigO, isLittleO_log_rpow_nhdsGT_zero, isBigO_logb_log, ArithmeticFunction.vonMangoldt_sum, isLittleO_log_rpow_atTop, ValueDistribution.characteristic_sub_characteristic_inv_le, ContDiffOn.log, AnalyticOnNhd.circleAverage_log_norm_of_ne_zero, le_rpow_iff_log_le, tendsto_nat_mul_log_one_add_of_tendsto, Polynomial.logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots, ValueDistribution.characteristic_add_top_eventuallyLE, derivWithin_const_rpow, mul_log_nonpos, doublingGamma_log_convex_Ioi, le_log_of_pow_le, lt_zpow_iff_log_lt, log_le_iff_le_exp, log_div_self, ProbabilityTheory.Fernique.lintegral_closedBall_diff_exp_logRatio_mul_sq_le, hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range, exp_log_of_neg, Chebyshev.theta_eq_log_primorial, NumberField.mixedEmbedding.logMap_apply_of_norm_eq_one, lt_log_of_zpow_lt, Polynomial.logMahlerMeasure_def, tendsto_mul_log_one_add_div_atTop, Tactic.ComputeAsymptotics.WellFormedBasis.compare_right_aux, AEMeasurable.log, log_le_log, ZetaAsymptotics.term_one, log_div, ContDiffAt.log, Differentiable.log, integral_inv_of_neg, ProbabilityTheory.Fernique.measure_gt_normThreshold_le_exp, circleIntegrable_log_norm_meromorphicOn, MeasureTheory.log_rnDeriv_tilted_left_self, tendsto_log_nhdsGT_zero, isLittleO_abs_log_rpow_rpow_nhdsGT_zero, exp_log, NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero, MeasureTheory.llr_smul_nnreal_left, HasStrictDerivAt.log, AbsoluteValue.IsEquiv.log_div_log_pos, InformationTheory.mul_log_le_toReal_klDiv, tendsto_log_nhdsLT_zero, fderivWithin.log, NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le, harmonic_floor_le_one_add_log, HasFDerivAt.log, log_div_self_antitoneOn, tendsto_rightDeriv_mul_log_atTop, posLog_def, ValueDistribution.characteristic_sub_characteristic_inv, NumberField.mixedEmbedding.fundamentalCone.expMap_symm_apply, integral_inv, continuous_log', tendsto_log_div_rpow_nhdsGT_zero, ProbabilityTheory.Fernique.logRatio_mul_normThreshold_add_one_le, Height.logHeight_eq_log_mulHeight, Chebyshev.psi_eq_theta_add_sum_theta, rightDeriv_mul_log, Measurable.log, ValueDistribution.characteristic_sum_top_le, isLittleO_const_log_atTop, Polynomial.exists_approx_polynomial, log_div_sqrt_antitoneOn, HasDerivAt.rpow, integral_one_div_of_pos, ValueDistribution.characteristic_add_top_le, Polynomial.logMahlerMeasure_eq_log_MahlerMeasure, deriv_const_rpow, not_differentiableAt_inv_log_zero, deriv_mul_log, MeasureTheory.integral_rnDeriv_mul_log, integral_log_sin_zero_pi, log_natCast_nonneg, Stirling.log_stirlingSeq_bounded_by_constant, rpow_inv_log_le_exp_one, tendsto_log_comp_add_sub_log, surjOn_log, hasDerivAt_log, HasStrictFDerivAt.const_rpow, NumberField.Units.abs_det_eq_abs_det, ProbabilityTheory.cgf_zero', Stirling.log_stirlingSeq'_antitone, binEntropy_eq_log_two, ProbabilityTheory.cgf_const', Tactic.ComputeAsymptotics.WellFormedBasis.compare_left_aux, integral_log, Complex.IsExpCmpFilter.isLittleO_log_norm_re, circleAverage_log_norm_add_const_eq_posLog, MeromorphicOn.circleAverage_log_norm, abs_log_mul_self_rpow_lt, ContinuousWithinAt.log, CFC.log_smul', Chebyshev.theta_eq_sum_Icc, integral_log_from_zero_of_pos, log_le_harmonic_floor, tendstoLocallyUniformlyOn_rpow_sub_one_log, AkraBazziRecurrence.eventually_deriv_one_sub_smoothingFn, Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAt, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, log_le_log_iff, tendsto_deriv_mul_log_atTop, Mathlib.Meta.Positivity.log_nonneg_of_isNegNat, MeromorphicOn.log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles, log_surjective, NumberField.mixedEmbedding.fundamentalCone.expMap_single_symm_apply, hasDerivAt_Gamma_one_half, InformationTheory.toReal_klDiv_smul_right, rpow_def_of_nonneg, AkraBazziRecurrence.isEquivalent_smoothingFn_sub_self, intervalIntegrable_log_cos, Height.logHeight_eval_le, not_DifferentiableAt_log_mul_zero, InformationTheory.rightDeriv_klFun, lt_log_of_pow_lt, continuousAt_log_iff, AkraBazziRecurrence.deriv_smoothingFn, rpow_le_iff_le_log, HasFDerivWithinAt.rpow, negMulLog_eq_neg, circleAverage_log_norm_sub_const_eq_posLog, ArithmeticFunction.vonMangoldt_apply, AkraBazziRecurrence.dist_r_b, analyticAt_log, Filter.Tendsto.log, NumberField.Units.dirichletUnitTheorem.logEmbedding_component, circleAverage_log_norm_factorizedRational, Chebyshev.theta_le_log4_mul_x, NumberField.mixedEmbedding.logMap_apply, strictMonoOn_log, Mathlib.Meta.Positivity.log_nonneg_of_isNat, AnalyticAt.harmonicAt_log_norm, log_intCast_nonneg, AnalyticOnNhd.sum_divisor_le, Height.logHeight_linearMap_apply_le, NumberField.mixedEmbedding.logMap_apply_of_norm_one, HasFDerivAt.const_rpow, Finsupp.logHeight_eq_log_mulHeight, Continuous.mul_log, log_nonneg, negMulLog_def, Chebyshev.psi_le, log_two_lt_d9, rpow_lt_iff_lt_log, log_multiset_prod, circleAverage_log_norm_sub_const₂, mul_log_eq_log_iff, lt_log_one_add_of_pos, MeromorphicOn.intervalIntegrable_log, MeasureTheory.llr_tilted_left, Chebyshev.integral_theta_div_log_sq_isBigO, Finsupp.log_prod, integral_one_div, cosh_log, Complex.IsExpCmpFilter.isLittleO_log_re_re, pow_le_iff_le_log, Chebyshev.integral_theta_div_log_sq_isLittleO, binEntropy_lt_log_two, log_lt_log_iff, BohrMollerup.f_add_nat_eq, Tactic.ComputeAsymptotics.WellFormedBasis.tail_isLittleO_head, strictAntiOn_log, log_finprod, rpow_eq_nhds_of_pos, Stirling.log_stirlingSeq_diff_le_geo_sum, Behrend.le_sqrt_log, measurable_log, log_pow, ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const, expPartialHomeomorph_symm_apply, tendsto_log_atTop, ProbabilityTheory.Fernique.lintegral_exp_mul_sq_norm_le_mul, log_comp_exp, log_natCast_le_rpow_div, Polynomial.logMahlerMeasure_const, Behrend.lower_bound_le_one', strictConcaveOn_log_Ioi, HasFDerivWithinAt.const_rpow, BohrMollerup.logGammaSeq_add_one, ZetaAsymptotics.term_sum_one, Polynomial.logMahlerMeasure_monomial, intervalIntegrable_log_norm_meromorphicOn, log_neg, Polynomial.logMahlerMeasure_C_mul_X_add_C, binEntropy_le_log_two, not_continuousAt_inv_log_one, sum_range_sub_log_div_le, posLog_eq_log_max_one, ArithmeticFunction.vonMangoldt_le_log, Complex.log_mul_ofReal, rpow_def_of_nonpos, circleIntegrable_log_norm_sub_const, abs_rpow_le_exp_log_mul, binEntropy_two_inv, half_mul_log_add_log_abs, ruzsaSzemerediNumberNat_lower_bound, MeasureTheory.llr_smul_right, Complex.tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero, log_inv, isBigO_logb_const_mul_log_atTop, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, hasStrictDerivAt_const_rpow, hasSum_pow_div_log_of_abs_lt_one, continuousAt_log, CFC.log_algebraMap, le_log_of_rpow_le, tendsto_log_nat_add_one_sub_log, log_nonpos_iff, Chebyshev.intervalIntegrable_one_div_log_sq, NumberField.Units.finrank_mul_regulator_eq_det, ENNReal.log_ofReal_of_pos, log_pos_of_lt_neg_one, tendsto_pow_log_div_mul_add_atTop, log_of_nat_eq_posLog, ruzsaSzemerediNumberNat_asymptotic_lower_bound, NumberField.Units.sum_mult_mul_log, hasStrictFDerivAt_rpow_of_neg, tendsto_log_nhdsNE_zero, MeasureTheory.llr_def, rexp_tsum_eq_tprod, isLittleO_pow_log_id_atTop, posLog_sum, ValueDistribution.characteristic_sum_top_eventuallyLE, AnalyticOnNhd.log, log_zero, MeasureTheory.integral_llr_tilted_right, ArithmeticFunction.vonMangoldt_apply_prime, tendsto_log_mul_rpow_nhdsGT_zero, Height.logHeight₁_eq_log_mulHeight₁, integral_log_from_zero, deriv_log_comp_eq_logDeriv, Chebyshev.theta_eq_primeCounting_mul_log_sub_integral, NumberField.Units.dirichletUnitTheorem.exists_unit, log_div_self_rpow_antitoneOn, ValueDistribution.abs_characteristic_sub_characteristic_shift_le, Complex.log_ofReal_re, log_of_ne_zero, HasDerivWithinAt.log, qaryEntropy_one, ContDiffWithinAt.log, deriv_mul_log_zero, AnalyticWithinAt.log, log_mul, integral_one_div_of_neg, exp_log_eq_abs, convexOn_mul_log, Chebyshev.eventually_primeCounting_le, Complex.IsExpCmpFilter.isTheta_cpow_exp_re_mul_log, deriv_sqrt_mul_log', Chebyshev.psi_le_const_mul_self, tendsto_log_mul_self_nhdsLT_zero, Tactic.ComputeAsymptotics.WellFormedBasis.push_log_last, abs_log_mul_self_lt, intervalIntegrable_log_sin, InformationTheory.deriv_klFun, tendsto_harmonic_sub_log_add_one, posLog_nat_mul, CFC.log_smul, HasFDerivAt.rpow, InformationTheory.toReal_klDiv_smul_left, log_nonneg_iff, AnalyticOn.log, log_le_sub_one_of_pos, one_sub_inv_le_log_of_pos, MeasureTheory.llr_smul_left, intervalIntegral.intervalIntegrable_log', derivWithin.log, isBigO_rpow_zero_log_smul, ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage, MeasureTheory.llr_smul_nnreal_right, AbsoluteValue.IsEquiv.log_div_log_eq_log_div_log, hasSum_log_sub_log_of_abs_lt_one, posLog_norm_sum_le, lt_rpow_iff_log_lt, log_doublingGamma_eq, MeasureTheory.integrable_rnDeriv_mul_log_iff, BohrMollerup.tendsto_log_gamma, lt_pow_iff_log_lt, deriv2_sqrt_mul_log, hasStrictDerivAt_log_of_pos, log_injOn_pos, circleIntegrable_log_norm_meromorphicOn_of_nonneg, Mathlib.Meta.Positivity.log_pos_of_isNegNat, posLog_add, AkraBazziRecurrence.isLittleO_self_div_log_id, log_neg_iff, ENNReal.log_ofReal, deriv2_mul_log, hasDerivAt_negMulLog, AkraBazziRecurrence.growsPolynomially_log
|