| Metric | Count |
|---|
DefinitionsHasDerivAt, HasDerivAtFilter, HasDerivWithinAt, HasStrictDerivAt, deriv, derivWithin | 6 |
Theoremscomp_ringHom, comp_semilinear₁, derivWithin, hasDerivAt, hasDerivAt, hasDerivWithinAt, deriv, derivWithin_eq, derivWithin_eq_of_mem, derivWithin_eq_of_nhds, deriv_eq, hasDerivAtFilter_iff, hasDerivAt_iff, hasDerivWithinAt_iff, hasDerivWithinAt_iff_of_mem, nhdsNE_deriv, comp_ringHom, comp_semilinear, congr_deriv, congr_of_eventuallyEq, continuousAt, continuousOn, deriv, differentiableAt, hasDerivAtFilter, hasDerivWithinAt, hasFDerivAt, le_of_lip', le_of_lipschitz, le_of_lipschitzOn, unique, congr_of_eventuallyEq, isBigO_sub, isBigO_sub_rev, isEquivalent_sub, isTheta_sub, mono, tendsto_nhds, Ici_of_Ioi, Iic_of_Iio, Iio_of_Iic, Ioi_iff_Ioo, Ioi_of_Ici, Ioi_of_Ioo, Ioo_of_Ioi, congr_deriv, congr_mono, congr_of_eventuallyEq, congr_of_eventuallyEq_of_mem, congr_of_mem, congr_set, continuousOn, continuousWithinAt, derivWithin, deriv_eq_zero, differentiableWithinAt, hasDerivAt, hasFDerivWithinAt, mono, mono_of_mem_nhdsWithin, union, hasDerivAt, hasDerivAtFilter, hasDerivWithinAt, congr_deriv, hasDerivAt, hasStrictFDerivAt, HasStrictDerivAt_ofNat, hasStrictDerivAt, deriv, eq_deriv, derivWithin_Ioi_eq_Ici, derivWithin_congr, derivWithin_congr_set, derivWithin_congr_set', derivWithin_const, derivWithin_fderivWithin, derivWithin_fun_const, derivWithin_id, derivWithin_id', derivWithin_intCast, derivWithin_inter, derivWithin_mem_iff, derivWithin_natCast, derivWithin_ofNat, derivWithin_of_isOpen, derivWithin_of_mem_nhds, derivWithin_of_mem_nhdsWithin, derivWithin_one, derivWithin_subset, derivWithin_univ, derivWithin_zero, derivWithin_zero_of_notMem_closure, derivWithin_zero_of_not_accPt, derivWithin_zero_of_not_differentiableWithinAt, derivWithin_zero_of_not_uniqueDiffWithinAt, deriv_const, deriv_const', deriv_eq, deriv_eqOn, deriv_fderiv, deriv_id, deriv_id', deriv_id'', deriv_intCast, deriv_mem_iff, deriv_natCast, deriv_ofNat, deriv_one, deriv_zero, deriv_zero_of_not_differentiableAt, differentiableAt_of_deriv_ne_zero, differentiableWithinAt_Ioi_iff_Ici, differentiableWithinAt_of_derivWithin_ne_zero, fderivWithin_derivWithin, fderiv_apply_one_eq_deriv, fderiv_deriv, fderiv_eq_deriv_mul, fderiv_eq_smul_deriv, hasDerivAtFilter_const, hasDerivAtFilter_id, hasDerivAtFilter_iff_isLittleO, hasDerivAtFilter_iff_tendsto, hasDerivAtFilter_intCast, hasDerivAtFilter_natCast, hasDerivAtFilter_ofNat, hasDerivAtFilter_one, hasDerivAtFilter_zero, hasDerivAt_const, hasDerivAt_deriv_iff, hasDerivAt_id, hasDerivAt_id', hasDerivAt_iff_hasFDerivAt, hasDerivAt_iff_isLittleO, hasDerivAt_iff_isLittleO_nhds_zero, hasDerivAt_iff_tendsto, hasDerivAt_intCast, hasDerivAt_natCast, hasDerivAt_ofNat, hasDerivAt_one, hasDerivAt_zero, hasDerivWithinAt_Iio_iff_Iic, hasDerivWithinAt_Ioi_iff_Ici, hasDerivWithinAt_congr_set, hasDerivWithinAt_congr_set', hasDerivWithinAt_const, hasDerivWithinAt_derivWithin_iff, hasDerivWithinAt_diff_singleton, hasDerivWithinAt_id, hasDerivWithinAt_iff_hasFDerivWithinAt, hasDerivWithinAt_iff_isLittleO, hasDerivWithinAt_iff_tendsto, hasDerivWithinAt_intCast, hasDerivWithinAt_inter, hasDerivWithinAt_inter', hasDerivWithinAt_natCast, hasDerivWithinAt_ofNat, hasDerivWithinAt_one, hasDerivWithinAt_univ, hasDerivWithinAt_zero, hasFDerivAtFilter_iff_hasDerivAtFilter, hasFDerivAt_iff_hasDerivAt, hasFDerivWithinAt_iff_hasDerivWithinAt, hasStrictDerivAt_const, hasStrictDerivAt_id, hasStrictDerivAt_iff_hasStrictFDerivAt, hasStrictDerivAt_intCast, hasStrictDerivAt_natCast, hasStrictDerivAt_one, hasStrictDerivAt_zero, hasStrictFDerivAt_iff_hasStrictDerivAt, norm_derivWithin_eq_norm_fderivWithin, norm_deriv_eq_norm_fderiv, norm_deriv_le_of_lip', norm_deriv_le_of_lipschitz, norm_deriv_le_of_lipschitzOn, toSpanSingleton_deriv, toSpanSingleton_derivWithin | 178 |
| Total | 184 |
| Name | Category | Theorems |
|---|
HasDerivAt 📖 | MathDef | 159 mathmath: hasFDerivAt_iff_hasDerivAt, Real.hasDerivAt_arccos, Real.hasDerivAt_fourier, hasDerivAt_sqrt_mul_log, Real.hasDerivAt_sigmoid, taylorWithinEval_hasDerivAt_Ioo, expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul, hasDerivAt_neg', hasDerivAt_bernoulliFun, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, HasGradientAt.hasDerivAt', Real.hasDerivAt_sin, hasDerivAt_exp_zero_of_radius_pos, monomial_has_deriv_aux, Real.hasDerivAt_mul_log, antideriv_bernoulliFun, ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀, DifferentiableAt.hasDerivAt, Real.hasDerivAt_arcosh, intervalIntegral.integral_hasDerivAt_of_tendsto_ae_right, hasDerivAt_iff_isLittleO, Complex.hasDerivAt_GammaIntegral, Real.hasDerivAt_arsinh, hasDerivAt_id', mellin_hasDerivAt_of_isBigO_rpow, hasDerivAt_abs_neg, ContinuousLinearMap.hasDerivAt, hasDerivAt_of_tendstoUniformly, InformationTheory.hasDerivAt_klFun, hasDerivAt_of_tendstoLocallyUniformlyOn, HasCompactSupport.hasDerivAt_convolution_right, AffineMap.hasDerivAt_lineMap, Complex.hasDerivAt_Gammaℝ_one, hasDerivAt_iff_tendsto_slope_left_right, hasDerivAt_abs_rpow, Filter.EventuallyEq.hasDerivAt_iff, hasDerivAt_deriv_iff, Real.hasDerivAt_binEntropy, hasDerivAt_gronwallBound_shift, intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_deriv_le, Real.hasDerivAt_qaryEntropy, hasDerivAt_add_const_iff, Monotone.ae_hasDerivAt, hasDerivAt_ofNat, hasDerivAt_update, hasDerivAt_jacobiTheta₂_fst, Real.hasDerivAt_arcsin, Complex.hasDerivAt_sinh, Real.hasDerivAt_tan, hasDerivAt_const, Complex.hasDerivAt_Gammaℂ_one, hasDerivAt_of_tendstoUniformlyOn, AffineMap.hasDerivAt, has_antideriv_at_fourier_neg, hasDerivAt_inv, Complex.hasDerivAt_cos, hasDerivAt_fourier_neg, Real.hasDerivAt_cos, hasDerivAt_exp_smul_const, ProbabilityTheory.hasDerivAt_complexMGF, Real.hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range, hasDerivAt_taylorWithinEval_succ, hasDerivAt_id, Real.hasDerivAt_rpow_const, hasDerivAt_integral_of_dominated_loc_of_deriv_le, spectrum.hasDerivAt_resolvent, hasDerivAt_exp, Complex.hasDerivAt_logTaylor, hasDerivAt_iff_tendsto_slope_zero, hasDerivAt_circleMap, hasDerivAt_iff_hasFDerivAt, hasDerivAt_fourier, ProbabilityTheory.hasDerivAt_neg_exp_mul_exp, NumberField.mixedEmbedding.fundamentalCone.hasDerivAt_expMap_single, hasDerivWithinAt_univ, Real.hasDerivAt_log, SchwartzMap.hasDerivAt, Complex.hasDerivAt_cosh, Real.hasDerivAt_mulExpNegMulSq, hasDerivAt_iff_isLittleO_nhds_zero, Real.hasDerivAt_cosh, Complex.hasDerivAt_sin, ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf, Real.hasDerivAt_fourierChar, hasDerivAt_intCast, Real.hasDerivAt_Gamma_one_half, intervalIntegral.integral_hasDerivAt_of_tendsto_ae_left, hasDerivAt_one, hasDerivAt_const_mul, hasDerivAt_abs, Polynomial.hasDerivAt, hasDerivAt_natCast, Real.hasDerivAt_Gamma_one, EulerSine.antideriv_cos_comp_const_mul, EulerSine.antideriv_sin_comp_const_mul, HasDerivWithinAt.hasDerivAt, HasFPowerSeriesAt.hasDerivAt, Polynomial.hasDerivAt_aeval, hasDerivAt_gronwallBound, hasDerivAt_ofReal_cpow_const, hasDerivAt_norm_rpow, HasFDerivAt.hasDerivAt, hasDerivAt_zero, ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt, hasDerivAt_exp_smul_const_of_mem_ball', Real.hasDerivAt_arctan', hasDerivAt_neg, intervalIntegral.integral_hasDerivAt_right, HasCompactSupport.hasDerivAt_convolution_left, Complex.IsConservativeOn.hasDerivAt_wedgeIntegral, hasDerivAt_pow, hasDerivAt_sub_const_iff, Complex.hasDerivAt_Gamma_one, ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF, Real.hasDerivAt_tan_of_mem_Ioo, Real.hasDerivAt_exp, ContDiffAt.exists_eventually_eq_hasDerivAt, StieltjesFunction.ae_hasDerivAt, hasDerivAt_ofReal_cpow_const', Complex.hasDerivAt_Gamma_one_half, hasDerivAt_finCons', HasStrictDerivAt.hasDerivAt, hasDerivAt_single, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real, Complex.hasDerivAt_tan, complexOfReal_hasDerivAt, ProbabilityTheory.hasDerivAt_mgf, hasDerivAt_mul_const, Real.hasDerivAt_arctan, hasDerivAt_exp_smul_const', hasDerivAt_iff_tendsto, intervalIntegral.integral_hasDerivAt_left, LSeries_hasDerivAt, Real.hasDerivAt_fourierIntegral, HasGradientAt.hasDerivAt, hasDerivAt_exp_zero, hasDerivAt_const_add_iff, intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_lip, Complex.hasDerivAt_exp, LinearMap.hasDerivAt, Complex.hasDerivAt_log_sub_logTaylor, hasDerivAt_iff_tendsto_slope, hasDerivAt_exp_of_mem_ball, Real.hasDerivAt_Gamma_nat, hasDerivAt_pi, Complex.hasDerivAt_log, hasDerivAt_zpow, Real.hasDerivAt_sinh, DifferentiableOn.hasDerivAt, hasDerivAt_of_tendsto_locally_uniformly_on', Real.hasDerivAt_sqrt, hasDerivAt_exp_smul_const_of_mem_ball, LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv, LSeries.hasDerivAt_term, hasDerivAt_finCons, hasDerivAt_abs_pos, IsMIntegralCurveAt.eventually_hasDerivAt, Complex.hasDerivAt_Gamma_nat, Real.hasDerivAt_negMulLog
|
HasDerivAtFilter 📖 | MathDef | 26 mathmath: AffineMap.hasDerivAtFilter, ContinuousLinearMap.hasDerivAtFilter, hasDerivAtFilter_ofNat, hasDerivAtFilter_natCast, hasDerivAtFilter_zero, hasDerivAtFilter_iff_tendsto_slope, HasGradientAtFilter.hasDerivAtFilter', hasDerivAtFilter_neg, hasDerivAtFilter_one, hasDerivAtFilter_id, hasDerivAtFilter_add_const_iff, hasFDerivAtFilter_iff_hasDerivAtFilter, hasDerivAtFilter_iff_isLittleO, hasDerivAtFilter_sub_const_iff, hasDerivAtFilter_intCast, hasDerivAtFilter_iff_tendsto, hasDerivAtFilter_finCons', hasDerivAtFilter_finCons, hasDerivAtFilter_pi, hasDerivAtFilter_const_add_iff, hasDerivAtFilter_const, HasDerivAt.hasDerivAtFilter, LinearMap.hasDerivAtFilter, HasGradientAtFilter.hasDerivAtFilter, HasFDerivAtFilter.hasDerivAtFilter, Filter.EventuallyEq.hasDerivAtFilter_iff
|
HasDerivWithinAt 📖 | MathDef | 74 mathmath: hasDerivWithinAt_Iio_iff_Iic, hasDerivWithinAt_ofNat, hasDerivWithinAt_add_const_iff, complexOfReal_hasDerivWithinAt, intervalIntegral.integral_hasDerivWithinAt_right, hasDerivWithinAt_Ioi_iff_Ici, hasDerivWithinAt_taylorWithinEval, HasDerivAt.hasDerivWithinAt, intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right, AffineMap.hasDerivWithinAt, hasDerivWithinAt_iff_isLittleO, hasDerivWithinAt_zero, hasDerivWithinAt_abs_pos, hasDerivWithinAt_pi, IsMIntegralCurveOn.hasDerivWithinAt, Filter.EventuallyEq.hasDerivWithinAt_iff_of_mem, hasDerivWithinAt_Iic_of_tendsto_deriv, hasDerivWithinAt_abs, intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_left, hasDerivWithinAt_neg, intervalIntegral.integral_hasDerivWithinAt_left, AffineMap.hasDerivWithinAt_lineMap, Real.hasDerivWithinAt_arccos_Ici, ConvexOn.hasDerivWithinAt_rightDeriv_of_mem_interior, DifferentiableWithinAt.hasDerivWithinAt, hasDerivWithinAt_pow, hasDerivWithinAt_iff_hasFDerivWithinAt, hasDerivWithinAt_one, hasFDerivWithinAt_iff_hasDerivWithinAt, hasDerivWithinAt_congr_set, hasDerivWithinAt_taylorWithinEval_at_Icc, Convex.exists_forall_hasDerivWithinAt, hasDerivWithinAt_taylor_coeff_within, LinearMap.hasDerivWithinAt, Real.hasDerivWithinAt_arcsin_Ici, hasDerivWithinAt_natCast, HasFDerivWithinAt.hasDerivWithinAt, hasDerivWithinAt_const, Polynomial.hasDerivWithinAt_aeval, hasDerivWithinAt_univ, ConvexOn.hasDerivWithinAt_sSup_slope_of_mem_interior, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn, hasDerivWithinAt_finCons', hasDerivWithinAt_comp_mul_left_smul_iff, ODE.hasDerivWithinAt_picard_Icc, hasDerivWithinAt_diff_singleton, hasDerivWithinAt_zpow, ConvexOn.hasDerivWithinAt_sInf_slope_of_mem_interior, hasDerivWithinAt_congr_set', hasDerivWithinAt_const_add_iff, hasDerivWithinAt_inter', HasDerivWithinAt.Ioi_iff_Ioo, IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt, hasDerivWithinAt_derivWithin_iff, hasDerivWithinAt_abs_neg, hasDerivWithinAt_id, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith, hasDerivWithinAt_intCast, ContinuousLinearMap.hasDerivWithinAt, hasDerivWithinAt_inv, hasDerivWithinAt_Ici_of_tendsto_deriv, hasDerivWithinAt_finCons, IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt, hasDerivWithinAt_iff_tendsto_slope', ConvexOn.hasDerivWithinAt_leftDeriv_of_mem_interior, Polynomial.hasDerivWithinAt, hasDerivWithinAt_iff_tendsto_slope, Real.hasDerivWithinAt_arccos_Iic, hasDerivWithinAt_inter, IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt₀, hasDerivWithinAt_iff_tendsto, Real.hasDerivWithinAt_arcsin_Iic, Filter.EventuallyEq.hasDerivWithinAt_iff, hasDerivWithinAt_sub_const_iff
|
HasStrictDerivAt 📖 | MathDef | 76 mathmath: AffineMap.hasStrictDerivAt_lineMap, hasStrictDerivAt_intCast, Real.hasStrictDerivAt_rpow_const_of_ne, Continuous.integral_hasStrictDerivAt, Complex.hasStrictDerivAt_tan, ContDiffAt.hasStrictDerivAt, Real.hasStrictDerivAt_sinh, hasStrictDerivAt_abs_pos, Real.hasStrictDerivAt_arccos, hasStrictDerivAt_exp_smul_const, hasStrictDerivAt_add_const_iff, hasStrictDerivAt_exp_smul_const', Real.deriv_sqrt_aux, intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_left, LinearMap.hasStrictDerivAt, hasStrictDerivAt_const_add_iff, Complex.hasStrictDerivAt_sinh, Real.hasStrictDerivAt_arcosh, Real.hasStrictDerivAt_cosh, Complex.hasStrictDerivAt_const_cpow, intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right, Real.hasStrictDerivAt_log, hasStrictFDerivAt_iff_hasStrictDerivAt, hasStrictDerivAt_finCons', hasStrictDerivAt_finCons, hasStrictDerivAt_zpow, Real.hasStrictDerivAt_const_rpow_of_neg, HasFPowerSeriesAt.hasStrictDerivAt, hasStrictDerivAt_abs, Complex.hasStrictDerivAt_log, Real.hasStrictDerivAt_arsinh, hasStrictDerivAt_abs_neg, Complex.hasStrictDerivAt_cos, Polynomial.hasStrictDerivAt_aeval, Complex.hasStrictDerivAt_sin, hasStrictDerivAt_const, Real.hasStrictDerivAt_arctan, Complex.hasStrictDerivAt_exp, Complex.hasStrictDerivAt_cosh, HasStrictFDerivAt.hasStrictDerivAt, Real.hasStrictDerivAt_cos, Complex.hasStrictDerivAt_cpow_const, Polynomial.hasStrictDerivAt, Real.hasStrictDerivAt_arcsin, AffineMap.hasStrictDerivAt, Real.hasStrictDerivAt_sin, hasStrictDerivAt_one, hasStrictDerivAt_pi, ContDiff.hasStrictDerivAt, hasStrictDerivAt_exp, Real.hasStrictDerivAt_sqrt, hasStrictDerivAt_inv, hasStrictDerivAt_natCast, hasStrictDerivAt_exp_zero_of_radius_pos, hasStrictDerivAt_exp_of_mem_ball, hasStrictDerivAt_zero, hasStrictDerivAt_exp_smul_const_of_mem_ball', intervalIntegral.integral_hasStrictDerivAt_right, Real.hasStrictDerivAt_tan, intervalIntegral.integral_hasStrictDerivAt_left, Real.deriv_arcsin_aux, Real.hasStrictDerivAt_const_rpow, hasStrictDerivAt_id, Real.hasStrictDerivAt_rpow_const, hasStrictDerivAt_iff_hasStrictFDerivAt, hasStrictDerivAt_exp_smul_const_of_mem_ball, ContinuousLinearMap.hasStrictDerivAt, hasStrictDerivAt_exp_zero, Real.hasStrictDerivAt_exp, hasStrictDerivAt_of_hasDerivAt_of_continuousAt, HasStrictDerivAt_ofNat, ContDiffAt.hasStrictDerivAt', hasStrictDerivAt_pow, Real.hasStrictDerivAt_log_of_pos, AnalyticAt.hasStrictDerivAt, hasStrictDerivAt_neg
|
deriv 📖 | CompOp | 392 mathmath: iteratedDeriv_scomp_two, MeromorphicOn.deriv, deriv_sub_const_fun, deriv_exp, MeromorphicAt.fun_iterated_deriv, Complex.cderiv_eq_deriv, deriv_arctan, PeriodPair.deriv_weierstrassP, Real.deriv_negMulLog, Complex.hasSum_deriv_of_summable_norm, HasCompactSupport.integral_Ioi_deriv_eq, deriv_abs, Real.nnnorm_deriv_mulExpNegMulSq_le_one, iteratedDeriv_succ, Real.deriv_binEntropy, measurable_deriv_with_param, deriv_mem_iff, AbsolutelyContinuousOnInterval.integral_deriv_eq_sub, logDeriv_comp, Meromorphic.deriv, StrictConvexOn.deriv_lt_slope, circleIntegral_def_Icc, circleIntegrable_iff, DirichletCharacter.continuousOn_neg_logDeriv_LFunction_of_nontriv, intervalIntegral.integral_deriv_of_contDiffOn_uIcc, deriv_fun_finset_prod, deriv_eq, deriv_cpow_const, deriv_comp_const_sub, AkraBazziRecurrence.isLittleO_deriv_one_add_smoothingFn, deriv_fun_sum, deriv_mul_const_field, DifferentiableOn.deriv, deriv_fun_pow', deriv_csinh, Real.deriv_log, ContDiff.differentiable_deriv_two, deriv_const_smul, deriv_mul_const, CPolynomialOn.iterated_deriv, ContDiff.continuous_deriv_one, Set.OrdConnected.image_deriv, ContDiffAt.hasStrictDerivAt, fderiv_comp_deriv, PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_sub_smoothingFn, DirichletCharacter.LSeries_twist_vonMangoldt_eq, StrictConvexOn.strictMonoOn_deriv, iter_deriv_zpow', Complex.deriv_cos, deriv.scomp_of_eq, Real.deriv_arccos, deriv_sqrt_mul_log, intervalIntegral.deriv_integral_right, iteratedDeriv_scomp_three, deriv_const', deriv.star, deriv_abs_neg, deriv.log, ContDiff.continuous_deriv, deriv_fun_inv'', exists_deriv_eq_zero, DifferentiableAt.hasDerivAt, DirichletCharacter.deriv_LFunction_eq_deriv_LSeries, deriv_zero_of_not_differentiableAt, MonotoneOn.intervalIntegrable_deriv, fderiv_eq_deriv_mul, deriv_const_add', Complex.deriv_ofReal_cpow_const, derivWithin_univ, Real.norm_deriv_mulExpNegMulSq_le_one, StrictConcaveOn.deriv_lt_slope, deriv_fun_mul, Real.not_continuousAt_deriv_mul_log_zero, iteratedDeriv_succ', StrictConcaveOn.slope_lt_deriv, Filter.EventuallyEq.deriv, ConvexOn.slope_le_deriv, deriv_sub, deriv.fun_neg', dslope_sub_smul, deriv_fun_smul, LSeries_deriv_eqOn, ContinuousLinearMap.deriv, deriv_norm_ofReal_cpow, deriv_fderiv, Real.deriv_rpow_const, BoundedVariationOn.intervalIntegrable_deriv, AkraBazziRecurrence.eventually_deriv_one_add_smoothingFn, Complex.deriv_Gamma_add_one, Real.deriv_sinh, exists_ratio_deriv_eq_ratio_slope, StrictConvexOn.slope_lt_deriv, HasDerivAt.deriv, HasCompactSupport.hasDerivAt_convolution_right, AnalyticAt.deriv, Polynomial.deriv_aeval, MeromorphicOn.fun_deriv, aestronglyMeasurable_deriv, deriv_id'', aemeasurable_deriv_with_param, LSeries_deriv, deriv_const_mul_field', deriv_fun_div, deriv.neg, deriv_zero, norm_sub_le_mul_volume_of_norm_deriv_le_of_le, measurable_deriv, deriv_pow, Real.deriv_Gamma_nat, hasDerivAt_deriv_iff, deriv_pi, DiffContOnCl.deriv_eq_smul_circleIntegral, DifferentiableOn.deriv_eq_smul_circleIntegral, deriv_comp_add_const, AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub, Real.deriv_inv_log, IsLocalExtr.deriv_eq_zero, IsLocalMax.deriv_eq_zero, MeromorphicOn.fun_iterated_deriv, AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_sub_smoothingFn, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, LinearMap.deriv, deriv_ccosh, Complex.deriv_Gamma_nat, Real.deriv_log', deriv_const_mul_field, Real.deriv2_binEntropy, ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div, Real.deriv_tan_sub_id, deriv_inv, norm_deriv_le_of_lipschitzOn, deriv_add_const', iteratedDerivWithin_of_isOpen_eq_iterate, iter_deriv_zpow, gradient_eq_deriv', integrableOn_Ioi_deriv_ofReal_cpow, Real.deriv_mulExpNegMulSq, Real.deriv_fourierIntegral, AnalyticAt.analyticOrderAt_deriv_add_one, MeromorphicAt.iterated_deriv, AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_add_smoothingFn, MonotoneOn.intervalIntegral_deriv_mem_uIcc, Real.deriv_qaryEntropy, Real.deriv_arctan, monotoneOn_deriv_descPochhammer_eval, deriv_fun_add, HasCompactSupport.integral_Iic_deriv_eq, Complex.iter_deriv_exp, ContinuousLinearMap.deriv_of_bilinear, AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_add_smoothingFn, ContDiffAt.derivWithin, ModularForm.logDeriv_one_sub_mul_cexp_comp, Complex.two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable, ConvexOn.monotoneOn_deriv, TendstoLocallyUniformlyOn.deriv, deriv_abs_zero, HasCompactSupport.enorm_le_lintegral_Ici_deriv, deriv_rpow_const, deriv_comp, logDeriv_apply, iteratedDeriv_vcomp_three, deriv.scomp, deriv_fun_sub, intervalIntegral.deriv_integral_left, deriv_abs_pos, HasDerivWithinAt.deriv_eq_zero, complexOfReal_deriv, deriv_csin, Polynomial.hermite_eq_deriv_gaussian', support_deriv_subset, Real.deriv_exp, deriv_sinh, deriv_cexp, deriv_update, Real.iter_deriv_exp, deriv_zpow', isTheta_deriv_rpow_const_atTop, Polynomial.deriv_gaussian_eq_hermite_mul_gaussian, dslope_same, contDiffOn_succ_iff_deriv_of_isOpen, deriv_smul, iter_deriv_pow', deriv_neg'', MeromorphicAt.fun_deriv, norm_deriv_le_of_lipschitz, ContDiff.iterate_deriv, ContDiff.deriv', intervalIntegral.deriv_integral_of_tendsto_ae_right, fderiv_apply_one_eq_deriv, deriv_inv'', deriv_circleMap, ProbabilityTheory.deriv_mgf, Polynomial.hermite_eq_deriv_gaussian, StrictConcaveOn.strictAntiOn_deriv, Real.deriv_arcsin, ArithmeticFunction.LSeries_vonMangoldt_eq, deriv_neg', deriv_zero_of_frequently_const, Real.eulerMascheroniConstant_eq_neg_deriv, CPolynomialOn.deriv, deriv_const_rpow, Filter.EventuallyEq.deriv_eq, enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc, Real.deriv_mul_log, AnalyticAt.iterated_deriv, AnalyticOnNhd.deriv_of_isOpen, Complex.deriv_cosh, fderiv_deriv, deriv_sub_const, Complex.differentiable_on_off_countable_deriv_eq_smul_circleIntegral, ConcaveOn.deriv_le_slope, deriv_single, stronglyMeasurable_deriv, range_deriv_subset_closure_span_image, Complex.deriv_tan, SchwartzMap.hasDerivAt, iteratedDeriv_comp_two, iteratedDeriv_eq_iterate, Complex.deriv_const_cpow, deriv_cos, DirichletCharacter.deriv_LFunctionTrivChar₁_apply_of_ne_one, isSeparable_range_deriv, deriv.fun_neg, AnalyticOnNhd.deriv, deriv_zpow, AkraBazziRecurrence.eventually_deriv_one_sub_smoothingFn, deriv_const, deriv_eqOn, IsLocalMin.deriv_eq_zero, Real.tendsto_deriv_mul_log_atTop, HasFPowerSeriesAt.deriv, deriv_one, PeriodPair.deriv_derivWeierstrassPExcept_self, deriv_clm_comp, aemeasurable_deriv, deriv_ccos, deriv_comp_of_eq, DifferentiableAt.derivWithin, deriv.neg', deriv_fun_const_smul, PeriodPair.deriv_weierstrassPExcept_same, iter_deriv_inv, exists_deriv_eq_zero', AkraBazziRecurrence.deriv_smoothingFn, deriv_natCast, curveIntegral_eq_intervalIntegral_deriv, Monotone.deriv_nonneg, ProbabilityTheory.iteratedDeriv_two_cgf, ProbabilityTheory.deriv_mgf_zero, AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn, Real.deriv_sigmoid, exists_ratio_deriv_eq_ratio_slope', ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq, iter_deriv_inv', Complex.norm_deriv_le_one_of_mapsTo_ball, ProbabilityTheory.deriv_cgf, Complex.deriv_cos', deriv_smul_const, deriv_pow_field, deriv_comp_neg, deriv_finset_prod, isBigO_deriv_ofReal_cpow_const_atTop, deriv_div, exists_deriv_eq_slope', Real.not_continuousAt_deriv_qaryEntropy_zero, AnalyticAt.analyticAt_localInverse, SchwartzMap.integral_mul_deriv_eq_neg_deriv_mul, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, norm_deriv_eq_norm_fderiv, deriv_id, Complex.norm_deriv_le_div_of_mapsTo_ball, SchwartzMap.derivCLM_apply, Convex.image_deriv, Real.deriv_cos, ContDiff.iterate_deriv', deriv_comp_mul_left, deriv_bernoulliFun, HasCompactSupport.hasDerivAt_convolution_left, deriv_const_mul, Real.deriv2_qaryEntropy, deriv_clm_apply, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, deriv_intCast, toSpanSingleton_deriv, Meromorphic.iterated_deriv, Complex.deriv_cpow_const, ConvexOn.deriv_le_slope, ContDiff.hasStrictDerivAt, Real.deriv_cos', isBigO_deriv_rpow_const_atTop, contDiff_succ_iff_deriv, Continuous.deriv_integral, Real.deriv_rpow_const', deriv_add_const, Polynomial.deriv, Real.iter_deriv_rpow_const, iteratedDeriv_comp_three, deriv_comp_const_add, deriv_const_add, deriv_inner_apply, Real.deriv_fourierChar, contDiff_infty_iff_deriv, iteratedDeriv_one, iter_deriv_inv_linear_sub, Complex.norm_deriv_le_of_forall_mem_sphere_norm_le, AkraBazziRecurrence.isLittleO_deriv_one_sub_smoothingFn, deriv_fun_const_smul_field, Complex.deriv_sinh, Complex.deriv_sin, Set.EqOn.deriv, MeromorphicAt.deriv, deriv_const_smul', Antitone.deriv_nonpos, deriv_fun_pow, deriv_inv', deriv_descPochhammer_eval_eq_sum_prod_range_erase, exists_deriv_eq_slope, iter_deriv_inv_linear, ProbabilityTheory.deriv_cgf_zero, ContDiffOn.continuousOn_deriv_of_isOpen, AkraBazziRecurrence.growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn, stronglyMeasurable_deriv_with_param, deriv_sin, AkraBazziRecurrence.isLittleO_deriv_smoothingFn, iteratedDeriv_vcomp_two, isTheta_deriv_ofReal_cpow_const_atTop, CircleIntegrable.out, contDiffOn_infty_iff_deriv_of_isOpen, deriv_circleMap_eq_zero_iff, Complex.exists_cthickening_tendstoUniformlyOn, HasCompactSupport.deriv, ContDiffOn.deriv_of_isOpen, deriv_neg, deriv_sum, intervalIntegral.deriv_integral_of_tendsto_ae_left, deriv_mul, deriv_pow', gradient_eq_deriv, Real.not_continuousAt_deriv_qaryEntropy_one, MeromorphicOn.iterated_deriv, derivWithin_of_isOpen, Complex.tendstoUniformlyOn_deriv_of_cthickening_subset, Real.deriv_log_comp_eq_logDeriv, Real.deriv_cosh, AkraBazziRecurrence.growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn, deriv.star', Real.deriv_sin, AffineMap.deriv, fderiv_comp_deriv_of_eq, DifferentiableOn.hasDerivAt, SchwartzMap.integral_smul_deriv_right_eq_neg_left, AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul, AnalyticOnNhd.iterated_deriv, deriv_mul_const_field', aestronglyMeasurable_deriv_with_param, Real.deriv_mul_log_zero, ConcaveOn.slope_le_deriv, deriv_zero_of_frequently_mem, deriv_sqrt_mul_log', Complex.deriv_exp, Real.deriv_tan, ConcaveOn.antitoneOn_deriv, deriv_const_smul_field, InformationTheory.deriv_klFun, deriv_add, ProbabilityTheory.integral_tilted_mul_self, integrableOn_Ioi_deriv_norm_ofReal_cpow, deriv_const_sub, derivWithin_of_mem_nhds, AbsolutelyContinuousOnInterval.intervalIntegrable_deriv, deriv_div_const, Complex.deriv_log_comp_eq_logDeriv, intervalIntegral.integral_deriv_of_contDiffOn_Icc, Real.deriv_fourier, Filter.EventuallyEq.nhdsNE_deriv, DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁, AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn, deriv_fun_const_smul', norm_deriv_le_of_lip', deriv_cosh, deriv_ofNat, deriv_sqrt, contDiff_one_iff_deriv, deriv2_sqrt_mul_log, AnalyticAt.hasStrictDerivAt, iter_deriv_pow, Real.deriv2_negMulLog, fderiv_eq_smul_deriv, deriv_comp_sub_const, Real.deriv2_mul_log, deriv_id'
|
derivWithin 📖 | CompOp | 201 mathmath: ConvexOn.leftDeriv_le_rightDeriv_of_mem_interior, ContinuousLinearMap.derivWithin_of_bilinear, Filter.EventuallyEq.derivWithin_eq_of_nhds, fderivWithin_comp_derivWithin_of_eq, derivWithin_zero_of_frequently_mem, StrictConvexOn.slope_lt_leftDeriv, derivWithin_smul, ConvexOn.rightDeriv_le_slope_of_mem_interior, isSeparable_range_derivWithin, RightDerivMeasurableAux.D_subset_differentiable_set, intervalIntegral.derivWithin_integral_of_tendsto_ae_left, Polynomial.derivWithin_aeval, derivWithin_id', intervalIntegral.integral_derivWithin_uIcc_of_contDiffOn_uIcc, derivWithin_mul_const, derivWithin_const, iteratedDerivWithin_vcomp_two, iteratedDerivWithin_comp_two, StrictConcaveOn.slope_lt_rightDeriv, derivWithin_fderivWithin, derivWithin_natCast, StrictConvexOn.rightDeriv_lt_slope, derivWithin_arctan, derivWithin_congr, derivWithin_comp_const_sub, derivWithin_fun_const_smul_field, derivWithin_zero_of_frequently_const, derivWithin_cosh, derivWithin_fun_mul, stronglyMeasurable_derivWithin_Ioi, StrictConcaveOn.slope_lt_derivWithin, derivWithin.scomp_of_eq, derivWithin.scomp, derivWithin_clm_comp, InformationTheory.leftDeriv_klFun_one, ConvexOn.monotoneOn_rightDeriv, iteratedDerivWithin_eq_iterate, derivWithin_univ, derivWithin.fun_neg, iteratedDerivWithin_one, derivWithin_zpow, AntitoneOn.derivWithin_nonpos, InformationTheory.tendsto_rightDeriv_klFun_atTop, derivWithin_of_mem_nhdsWithin, derivWithin_congr_set', RightDerivMeasurableAux.differentiable_set_subset_D, InformationTheory.leftDeriv_klFun, derivWithin.neg, derivWithin_ofNat, ConvexOn.hasDerivWithinAt_rightDeriv_of_mem_interior, derivWithin_fun_div, derivWithin_inv, DifferentiableWithinAt.hasDerivWithinAt, derivWithin_const_add, derivWithin_subset, fderivWithin_comp_derivWithin, derivWithin_div_const, Set.OrdConnected.image_derivWithin, ContinuousLinearMap.derivWithin, aestronglyMeasurable_derivWithin_Ioi, Polynomial.derivWithin, derivWithin_const_smul_field, Real.leftDeriv_mul_log, iteratedDerivWithin_comp_three, derivWithin_fun_const_smul, ConvexOn.slope_le_leftDeriv, HasDerivWithinAt.derivWithin, enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc, ContDiffOn.derivWithin, derivWithin_comp_of_eq, derivWithin_cos, measurableSet_of_differentiableWithinAt_Ici_of_isComplete, derivWithin_const_rpow, iteratedDerivWithin_scomp_three, derivWithin_ccosh, derivWithin_cexp, StrictConvexOn.strictMonoOn_derivWithin, Filter.EventuallyEq.derivWithin_eq, derivWithin_mul_const_field, derivWithin_zero_of_notMem_closure, ContDiffWithinAt.derivWithin, derivWithin_exp, hasDerivAt_taylorWithinEval_succ, aestronglyMeasurable_derivWithin_Ici, derivWithin_rpow_const, intervalIntegral.derivWithin_integral_right, MonotoneOn.derivWithin_nonneg, derivWithin_pow_field, StrictConcaveOn.derivWithin_lt_slope, StrictConvexOn.slope_lt_derivWithin, Real.tendsto_rightDeriv_mul_log_atTop, derivWithin_comp_mul_left, derivWithin_zero_of_not_uniqueDiffWithinAt, derivWithin_fun_smul, curveIntegralFun_def', derivWithin_intCast, norm_derivWithin_eq_norm_fderivWithin, AffineMap.derivWithin, ContDiffOn.continuousOn_derivWithin, Real.rightDeriv_mul_log, derivWithin_fun_sub, ConcaveOn.slope_le_derivWithin, ConvexOn.monotoneOn_leftDeriv, derivWithin_zero_of_not_accPt, derivWithin_sin, Filter.EventuallyEq.derivWithin_eq_of_mem, Convex.image_derivWithin, intervalIntegral.derivWithin_integral_of_tendsto_ae_right, derivWithin_pi, ConcaveOn.leftDeriv_le_slope, derivWithin_one, derivWithin_ccos, ConcaveOn.derivWithin_le_slope, StrictConcaveOn.strictAntiOn_derivWithin, derivWithin_inv', derivWithin_fun_sum, derivWithin_csin, intervalIntegral.integral_derivWithin_Icc_of_contDiffOn_Icc, derivWithin_comp, derivWithin_const_smul, toSpanSingleton_derivWithin, ConvexOn.derivWithin_le_slope, DifferentiableAt.derivWithin, fderivWithin_derivWithin, ConvexOn.leftDeriv_eq_sSup_slope_of_mem_interior, InformationTheory.rightDeriv_klFun_one, InformationTheory.rightDeriv_klFun, RightDerivMeasurableAux.differentiable_set_eq_D, derivWithin_fun_finset_prod, derivWithin_sum, derivWithin_sub_const_fun, measurable_derivWithin_Ioi, Complex.derivWithin_const_cpow, stronglyMeasurable_derivWithin_Ici, derivWithin_fun_const, LinearMap.derivWithin, derivWithin_fun_pow, derivWithin_sqrt, iteratedDerivWithin_succ, ConvexOn.rightDeriv_le_slope, iteratedDerivWithin_succ', StrictConvexOn.derivWithin_lt_slope, contDiffOn_succ_iff_derivWithin, hasDerivWithinAt_derivWithin_iff, derivWithin_const_add_fun, derivWithin_comp_add_const, derivWithin.star, derivWithin_zero, derivWithin_fun_const_smul', derivWithin_fun_add, derivWithin_zero_of_not_differentiableWithinAt, ConvexOn.monotoneOn_derivWithin, ConcaveOn.slope_le_rightDeriv, ConcaveOn.antitoneOn_derivWithin, derivWithin_neg, ConvexOn.slope_le_derivWithin, derivWithin_finset_prod, derivWithin_div, derivWithin_csinh, derivWithin_comp_sub_const, derivWithin_Ioi_eq_Ici, derivWithin_id, derivWithin_mul, iteratedDerivWithin_scomp_two, derivWithin_add_const, aemeasurable_derivWithin_Ici, derivWithin_congr_set, derivWithin_sub, derivWithin_comp_const_add, intervalIntegral.derivWithin_integral_left, range_derivWithin_subset_closure_span_image, derivWithin_add, derivWithin_fun_inv', derivWithin_sinh, derivWithin_of_isOpen, measurable_derivWithin_Ici, StrictConcaveOn.leftDeriv_lt_slope, derivWithin_sub_const, contDiffOn_infty_iff_derivWithin, ConvexOn.hasDerivWithinAt_leftDeriv_of_mem_interior, complexOfReal_derivWithin, derivWithin_pow, derivWithin_inter, derivWithin_smul_const, derivWithin_const_sub, derivWithin_const_mul_field, derivWithin_clm_apply, RightDerivMeasurableAux.mem_A_of_differentiable, derivWithin_const_smul', derivWithin_of_mem_nhds, derivWithin.log, curveIntegralFun_def, ConvexOn.rightDeriv_eq_sInf_slope_of_mem_interior, derivWithin_mem_iff, ConvexOn.slope_le_leftDeriv_of_mem_interior, derivWithin_fun_pow', derivWithin_comp_neg, derivWithin_pow', iteratedDerivWithin_vcomp_three, derivWithin_const_mul, aemeasurable_derivWithin_Ioi
|