| 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, isBigO_sub, isLittleO, le_of_lip', le_of_lipschitz, le_of_lipschitzOn, of_isLittleO, unique, congr_of_eventuallyEq, hasFDerivAtFilter, 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, isLittleO, mono, mono_of_mem_nhdsWithin, of_isLittleO, union, hasDerivAt, hasDerivAtFilter, hasDerivWithinAt, congr_deriv, congr_of_eventuallyEq, 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_hasFDerivAtFilter, 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 | 186 |
| Total | 192 |
| Name | Category | Theorems |
|---|
HasDerivAt 📖 | MathDef | 264 mathmath: HasDerivAt.fun_neg, hasFDerivAt_iff_hasDerivAt, Real.hasDerivAt_arccos, Real.hasDerivAt_fourier, HasDerivAt.ccos, HasDerivAt.const_rpow, HasDerivAt.const_sub, hasDerivAt_sqrt_mul_log, Real.hasDerivAt_sigmoid, taylorWithinEval_hasDerivAt_Ioo, hasDerivAt_integral_of_dominated_loc_of_lip, expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul, OpenPartialHomeomorph.hasDerivAt_symm, HasDerivAt.fun_finset_prod, hasDerivAt_neg', hasDerivAt_bernoulliFun, HasDerivAt.comp_ofReal, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, HasGradientAt.hasDerivAt', HasDerivAt.clm_apply, Real.hasDerivAt_sin, hasDerivAt_exp_zero_of_radius_pos, hasDerivAt_star_conj_iff, monomial_has_deriv_aux, Real.hasDerivAt_mul_log, hasDerivAt_of_hasDerivAt_of_ne, antideriv_bernoulliFun, ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀, DifferentiableAt.hasDerivAt, HasDerivAt.finCons, Real.hasDerivAt_arcosh, intervalIntegral.integral_hasDerivAt_of_tendsto_ae_right, HasDerivAt.cpow, hasDerivAt_iff_isLittleO, HasDerivAt.arctan, HasDerivAt.sqrt, HasDerivAt.congr_of_eventuallyEq, HasDerivAt.fun_pow', Complex.hasDerivAt_GammaIntegral, HasDerivAt.add, Real.hasDerivAt_arsinh, hasDerivAt_id', mellin_hasDerivAt_of_isBigO_rpow, hasDerivAt_abs_neg, HasDerivAt.pow, ContinuousLinearMap.hasDerivAt, hasDerivAt_of_tendstoUniformly, InformationTheory.hasDerivAt_klFun, HasDerivAt.fun_pow, hasDerivAt_of_tendstoLocallyUniformlyOn, HasCompactSupport.hasDerivAt_convolution_right, hasDerivAt_tsum_of_isPreconnected, AffineMap.hasDerivAt_lineMap, Complex.hasDerivAt_Gammaℝ_one, hasDerivAt_iff_tendsto_slope_left_right, HasDerivAt.fun_add, HasDerivAt.neg, HasDerivAt.star, hasDerivAt_abs_rpow, HasDerivAt.comp, HasFDerivAt.comp_hasDerivAt, HasDerivAt.log, Filter.EventuallyEq.hasDerivAt_iff, HasDerivAt.csinh, hasDerivAt_deriv_iff, Real.hasDerivAt_binEntropy, hasDerivAt_gronwallBound_shift, hasDerivAt_of_hasDerivAt_of_ne', intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_deriv_le, Real.hasDerivAt_qaryEntropy, hasDerivAt_add_const_iff, Monotone.ae_hasDerivAt, hasDerivAt_ofNat, HasDerivAt.cosh, HasDerivAt.sub, HasDerivAt.ccosh, hasDerivAt_update, hasDerivAt_tsum, hasDerivAt_jacobiTheta₂_fst, HasDerivAt.exp, Real.hasDerivAt_arcsin, Complex.hasDerivAt_sinh, HasDerivAt.csin, Real.hasDerivAt_tan, HasDerivAt.smul_const, HasDerivAt.cos, hasDerivAt_const, Complex.hasDerivAt_Gammaℂ_one, HasDerivAt.add_const, HasDerivAt.of_isLittleO, HasDerivAt.sub_const, hasDerivAt_of_tendstoUniformlyOn, AffineMap.hasDerivAt, has_antideriv_at_fourier_neg, hasDerivAt_inv, HasDerivAt.sinh, Complex.hasDerivAt_cos, hasDerivAt_fourier_neg, HasDerivAt.clm_comp, Real.hasDerivAt_cos, HasDerivWithinAt.comp_hasDerivAt_of_eq, HasDerivAt.fun_const_smul, HasDerivAt.fun_sub, hasDerivAt_exp_smul_const, HasDerivAt.clog, ProbabilityTheory.hasDerivAt_complexMGF, Real.hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range, HasDerivAt.const_smul, hasDerivAt_taylorWithinEval_succ, HasDerivAt.comp_const_sub, HasDerivAt.norm_sq, HasDerivAt.fun_div, 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.comp_const_add, hasDerivAt_circleMap, HasDerivWithinAt.scomp_hasDerivAt_of_eq, Complex.hasDerivAt_sqrt, hasDerivAt_iff_hasFDerivAt, HasDerivAt.arsinh, hasDerivAt_fourier, HasDerivAt.rpow, ProbabilityTheory.hasDerivAt_neg_exp_mul_exp, HasDerivAt.fun_sum, NumberField.mixedEmbedding.fundamentalCone.hasDerivAt_expMap_single, hasDerivWithinAt_univ, HasDerivAt.ofReal_comp, Real.hasDerivAt_log, SchwartzMap.hasDerivAt, Complex.hasDerivAt_cosh, Real.hasDerivAt_mulExpNegMulSq, hasDerivAt_iff_isLittleO_nhds_zero, Real.hasDerivAt_cosh, IsIntegralCurveAt.hasDerivAt, Complex.hasDerivAt_sin, ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf, Real.hasDerivAt_fourierChar, hasDerivAt_intCast, Real.hasDerivAt_Gamma_one_half, HasDerivAt.scomp, HasDerivAt.const_mul, 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, HasDerivAt.real_of_complex, HasFDerivWithinAt.comp_hasDerivAt, HasDerivAt.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.sum, HasDerivAt.fun_smul, hasDerivAt_zero, ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt, HasDerivWithinAt.scomp_hasDerivAt, hasDerivAt_exp_smul_const_of_mem_ball', Real.hasDerivAt_arctan', hasDerivAt_neg, intervalIntegral.integral_hasDerivAt_right, HasCompactSupport.hasDerivAt_convolution_left, HasDerivAt.const_add, HasDerivAt.prodMk, Complex.IsConservativeOn.hasDerivAt_wedgeIntegral, HasDerivAt.div_const, HasDerivAt.scomp_of_eq, HasDerivAt.cexp, hasDerivAt_pow, HasDerivAt.rpow_const, hasDerivAt_sub_const_iff, HasDerivAt.div, Complex.hasDerivAt_Gamma_one, ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF, Real.hasDerivAt_tan_of_mem_Ioo, Real.hasDerivAt_exp, HasDerivAt.iterate, ContDiffAt.exists_eventually_eq_hasDerivAt, StieltjesFunction.ae_hasDerivAt, HasDerivAt.inner, hasDerivAt_ofReal_cpow_const', Complex.hasDerivAt_Gamma_one_half, hasDerivAt_finCons', HasStrictDerivAt.hasDerivAt, hasDerivAt_single, Complex.IsExactOn.with_val_at, HasDerivAt.pow', ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real, Complex.hasDerivAt_tan, complexOfReal_hasDerivAt, HasDerivAt.fun_inv, ProbabilityTheory.hasDerivAt_mgf, hasDerivAt_mul_const, Real.hasDerivAt_arctan, hasDerivAt_exp_smul_const', HasDerivAt.comp_of_eq, hasDerivAt_iff_tendsto, HasDerivAt.finset_prod, intervalIntegral.integral_hasDerivAt_left, spectrum.hasDerivAt_resolvent_const_right, LSeries_hasDerivAt, Real.hasDerivAt_fourierIntegral, HasDerivAt.conj_conj, HasGradientAt.hasDerivAt, hasDerivAt_exp_zero, HasDerivAt.comp_ringHom, hasDerivAt_const_add_iff, intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_lip, Complex.hasDerivAt_exp, spectrum.hasDerivAt_resolvent_const_left, LinearMap.hasDerivAt, Complex.hasDerivAt_log_sub_logTaylor, hasDerivAt_iff_tendsto_slope, HasFDerivWithinAt.comp_hasDerivAt_of_eq, HasDerivWithinAt.comp_hasDerivAt, hasDerivAt_exp_of_mem_ball, Real.hasDerivAt_Gamma_nat, hasDerivAt_pi, HasDerivAt.of_notMem_tsupport, HasDerivAt.fun_mul, HasDerivAt.const_cpow, HasDerivAt.smul, Complex.hasDerivAt_log, hasDerivAt_zpow, HasDerivAt.sin, Real.hasDerivAt_sinh, HasDerivAt.comp_add_const, DifferentiableOn.hasDerivAt, hasDerivAt_of_tendsto_locally_uniformly_on', hasDerivAt_conj_conj_iff, Real.hasDerivAt_sqrt, hasDerivAt_exp_smul_const_of_mem_ball, HasDerivAt.comp_semilinear, LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv, HasDerivAt.clog_real, HasDerivAt.comp_sub_const, HasDerivAt.of_local_left_inverse, LSeries.hasDerivAt_term, HasDerivAt.star_conj, hasDerivAt_finCons, hasDerivAt_of_tendstoUniformlyOnFilter, HasDerivAt.inv, hasDerivAt_abs_pos, IsMIntegralCurveAt.eventually_hasDerivAt, HasDerivAt.congr_deriv, ContinuousLinearMap.hasDerivAt_of_bilinear, HasFDerivAt.comp_hasDerivAt_of_eq, Complex.hasDerivAt_Gamma_nat, HasDerivAt.mul_const, HasDerivAt.cpow_const, Real.hasDerivAt_negMulLog
|
HasDerivAtFilter 📖 | MathDef | 51 mathmath: HasDerivAtFilter.sum, AffineMap.hasDerivAtFilter, ContinuousLinearMap.hasDerivAtFilter, hasDerivAtFilter_ofNat, HasDerivAtFilter.add, hasDerivAtFilter_natCast, hasDerivAtFilter_zero, hasDerivAtFilter_iff_tendsto_slope, HasDerivAtFilter.mono, HasGradientAtFilter.hasDerivAtFilter', HasDerivAtFilter.fun_add, HasDerivAtFilter.sub, HasDerivAtFilter.iterate, HasDerivAtFilter.const_smul, hasDerivAtFilter_neg, hasDerivAtFilter_one, hasDerivAtFilter_id, hasDerivAtFilter_add_const_iff, HasDerivAtFilter.sub_const, hasFDerivAtFilter_iff_hasDerivAtFilter, HasDerivAtFilter.star, HasDerivAtFilter.scomp, hasDerivAtFilter_iff_isLittleO, HasDerivAtFilter.add_const, HasDerivAtFilter.scomp_of_eq, hasDerivAtFilter_sub_const_iff, HasDerivAtFilter.congr_of_eventuallyEq, HasDerivAtFilter.const_add, hasDerivAtFilter_intCast, hasDerivAtFilter_iff_tendsto, HasDerivAtFilter.comp_of_eq, hasDerivAtFilter_finCons', HasDerivAtFilter.fun_neg, HasDerivAtFilter.fun_sub, HasDerivAtFilter.prodMk, hasDerivAtFilter_iff_hasFDerivAtFilter, hasDerivAtFilter_finCons, hasDerivAtFilter_pi, hasDerivAtFilter_const_add_iff, hasDerivAtFilter_const, HasDerivAtFilter.finCons, HasDerivAt.hasDerivAtFilter, HasDerivAtFilter.comp, LinearMap.hasDerivAtFilter, HasDerivAtFilter.neg, HasGradientAtFilter.hasDerivAtFilter, HasFDerivAtFilter.hasDerivAtFilter, Filter.EventuallyEq.hasDerivAtFilter_iff, HasDerivAtFilter.fun_sum, HasDerivAtFilter.const_sub, HasDerivAtFilter.fun_const_smul
|
HasDerivWithinAt 📖 | MathDef | 168 mathmath: HasDerivWithinAt.clog_real, HasDerivWithinAt.clm_comp, HasDerivWithinAt.congr_of_mem, hasDerivWithinAt_Iio_iff_Iic, hasDerivWithinAt_ofNat, hasDerivWithinAt_add_const_iff, HasDerivWithinAt.Iio_of_Iic, HasDerivWithinAt.div_const, HasDerivWithinAt.congr_mono, complexOfReal_hasDerivWithinAt, intervalIntegral.integral_hasDerivWithinAt_right, HasDerivWithinAt.cosh, hasDerivWithinAt_Ioi_iff_Ici, hasDerivWithinAt_taylorWithinEval, HasDerivAt.hasDerivWithinAt, HasDerivWithinAt.fun_div, intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right, HasFDerivWithinAt.comp_hasDerivWithinAt_of_eq, AffineMap.hasDerivWithinAt, hasDerivWithinAt_iff_isLittleO, hasDerivWithinAt_zero, ContinuousLinearMap.hasDerivWithinAt_of_bilinear, HasDerivWithinAt.sub, hasDerivWithinAt_abs_pos, HasDerivWithinAt.sub_const, hasDerivWithinAt_pi, HasDerivWithinAt.Iic_of_Iio, HasDerivWithinAt.clm_apply, HasDerivWithinAt.sin, IsMIntegralCurveOn.hasDerivWithinAt, HasDerivWithinAt.comp, Filter.EventuallyEq.hasDerivWithinAt_iff_of_mem, HasDerivWithinAt.cos, hasDerivWithinAt_Iic_of_tendsto_deriv, hasDerivWithinAt_abs, HasDerivWithinAt.csinh, intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_left, HasDerivWithinAt.fun_pow', hasDerivWithinAt_neg, HasDerivWithinAt.const_add, HasDerivWithinAt.fun_finset_prod, HasDerivWithinAt.norm_sq, intervalIntegral.integral_hasDerivWithinAt_left, AffineMap.hasDerivWithinAt_lineMap, Real.hasDerivWithinAt_arccos_Ici, HasDerivWithinAt.const_cpow, HasDerivWithinAt.const_rpow, ConvexOn.hasDerivWithinAt_rightDeriv_of_mem_interior, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.mul, HasDerivWithinAt.sqrt, hasDerivWithinAt_pow, hasDerivWithinAt_iff_hasFDerivWithinAt, hasDerivWithinAt_one, HasDerivWithinAt.inner, HasDerivWithinAt.arsinh, HasDerivWithinAt.scomp_of_eq, hasFDerivWithinAt_iff_hasDerivWithinAt, HasDerivWithinAt.cpow, HasDerivWithinAt.fun_neg, HasDerivWithinAt.Ici_of_Ioi, HasDerivWithinAt.rpow, hasDerivWithinAt_congr_set, hasDerivWithinAt_taylorWithinEval_at_Icc, HasDerivWithinAt.congr_of_eventuallyEq_of_mem, HasDerivWithinAt.ccosh, HasDerivWithinAt.fun_smul, Convex.exists_forall_hasDerivWithinAt, hasDerivWithinAt_taylor_coeff_within, LinearMap.hasDerivWithinAt, Real.hasDerivWithinAt_arcsin_Ici, HasDerivAt.scomp_hasDerivWithinAt_of_eq, HasDerivWithinAt.add, hasDerivWithinAt_natCast, HasDerivWithinAt.fun_const_smul, HasDerivWithinAt.const_mul, HasDerivWithinAt.div, HasDerivWithinAt.arctan, HasDerivWithinAt.clog, HasDerivWithinAt.neg, HasFDerivWithinAt.hasDerivWithinAt, HasDerivWithinAt.Ioo_of_Ioi, HasFDerivAt.comp_hasDerivWithinAt, hasDerivWithinAt_const, HasDerivWithinAt.csin, Polynomial.hasDerivWithinAt_aeval, HasFDerivAt.comp_hasDerivWithinAt_of_eq, HasDerivWithinAt.of_notMem_tsupport, HasDerivWithinAt.mono_of_mem_nhdsWithin, HasDerivWithinAt.Ioi_of_Ioo, HasDerivWithinAt.fun_mul, HasDerivWithinAt.pow', HasDerivWithinAt.sinh, hasDerivWithinAt_univ, ConvexOn.hasDerivWithinAt_sSup_slope_of_mem_interior, HasDerivWithinAt.fun_sub, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn, hasDerivWithinAt_finCons', HasDerivWithinAt.scomp, hasDerivWithinAt_comp_mul_left_smul_iff, HasDerivWithinAt.congr_deriv, HasFDerivWithinAt.comp_hasDerivWithinAt, HasDerivWithinAt.inv, ODE.hasDerivWithinAt_picard_Icc, hasDerivWithinAt_diff_singleton, HasDerivAt.comp_hasDerivWithinAt, HasDerivWithinAt.congr, HasDerivWithinAt.ccos, HasDerivWithinAt.smul_const, HasDerivWithinAt.union, HasDerivWithinAt.add_const, HasDerivWithinAt.congr_set, hasDerivWithinAt_zpow, HasDerivWithinAt.smul, HasDerivWithinAt.fun_pow, HasDerivWithinAt.finset_prod, HasDerivWithinAt.mono, ConvexOn.hasDerivWithinAt_sInf_slope_of_mem_interior, HasDerivWithinAt.const_sub, HasDerivWithinAt.const_smul, hasDerivWithinAt_congr_set', HasDerivWithinAt.rpow_const, hasDerivWithinAt_const_add_iff, HasDerivWithinAt.star, hasDerivWithinAt_inter', HasDerivWithinAt.mul_const, HasDerivWithinAt.cexp, HasDerivWithinAt.Ioi_of_Ici, HasDerivWithinAt.Ioi_iff_Ioo, HasDerivWithinAt.fun_add, IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt, HasDerivWithinAt.of_isLittleO, HasDerivWithinAt.prodMk, hasDerivWithinAt_derivWithin_iff, HasDerivWithinAt.pow, HasDerivWithinAt.congr_of_eventuallyEq, hasDerivWithinAt_abs_neg, HasDerivAt.scomp_hasDerivWithinAt, HasDerivWithinAt.cpow_const, hasDerivWithinAt_id, HasDerivAt.comp_hasDerivWithinAt_of_eq, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith, hasDerivWithinAt_intCast, ContinuousLinearMap.hasDerivWithinAt, HasDerivWithinAt.comp_of_eq, hasDerivWithinAt_inv, hasDerivWithinAt_Ici_of_tendsto_deriv, HasDerivWithinAt.fun_sum, hasDerivWithinAt_finCons, HasDerivWithinAt.exp, IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt, hasDerivWithinAt_iff_tendsto_slope', Complex.hasDerivWithinAt_sqrt, ConvexOn.hasDerivWithinAt_leftDeriv_of_mem_interior, Polynomial.hasDerivWithinAt, HasDerivWithinAt.log, hasDerivWithinAt_iff_tendsto_slope, Real.hasDerivWithinAt_arccos_Iic, HasDerivWithinAt.sum, hasDerivWithinAt_inter, IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt₀, HasDerivWithinAt.iterate, hasDerivWithinAt_iff_tendsto, Real.hasDerivWithinAt_arcsin_Iic, HasDerivWithinAt.fun_inv, HasDerivWithinAt.finCons, Filter.EventuallyEq.hasDerivWithinAt_iff, hasDerivWithinAt_sub_const_iff
|
HasStrictDerivAt 📖 | MathDef | 148 mathmath: HasStrictDerivAt.fun_pow', AffineMap.hasStrictDerivAt_lineMap, HasStrictDerivAt.to_localInverse, hasStrictDerivAt_intCast, HasStrictDerivAt.rpow, Real.hasStrictDerivAt_rpow_const_of_ne, HasStrictDerivAt.pow, Continuous.integral_hasStrictDerivAt, HasStrictDerivAt.of_local_left_inverse, Complex.hasStrictDerivAt_tan, HasStrictDerivAt.pow', ContDiffAt.hasStrictDerivAt, HasStrictDerivAt.cpow, HasStrictFDerivAt.comp_hasStrictDerivAt, Real.hasStrictDerivAt_sinh, hasStrictDerivAt_abs_pos, HasStrictDerivAt.clm_comp, HasStrictDerivAt.fun_sum, Real.hasStrictDerivAt_arccos, hasStrictDerivAt_exp_smul_const, hasStrictDerivAt_add_const_iff, HasStrictDerivAt.csin, hasStrictDerivAt_exp_smul_const', HasStrictDerivAt.div, HasStrictDerivAt.arctan, HasStrictDerivAt.mul, Real.deriv_sqrt_aux, HasStrictDerivAt.real_of_complex, HasStrictDerivAt.const_mul, intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_left, LinearMap.hasStrictDerivAt, hasStrictDerivAt_const_add_iff, Complex.hasStrictDerivAt_sinh, HasStrictDerivAt.sin, HasStrictDerivAt.clog_real, HasStrictDerivAt.to_local_left_inverse, HasStrictDerivAt.exp, UpperHalfPlane.hasStrictDerivAt_smul, ContinuousLinearMap.hasStrictDerivAt_of_bilinear, Real.hasStrictDerivAt_arcosh, HasStrictDerivAt.sum, HasStrictDerivAt.smul, HasStrictDerivAt.csinh, Real.hasStrictDerivAt_cosh, HasStrictDerivAt.cosh, Complex.hasStrictDerivAt_const_cpow, intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right, Real.hasStrictDerivAt_log, HasStrictDerivAt.mul_const, hasStrictFDerivAt_iff_hasStrictDerivAt, HasStrictDerivAt.cexp, HasStrictDerivAt.scomp_of_eq, HasStrictDerivAt.fun_finset_prod, hasStrictDerivAt_finCons', hasStrictDerivAt_finCons, hasStrictDerivAt_zpow, HasStrictDerivAt.comp_of_eq, Real.hasStrictDerivAt_const_rpow_of_neg, HasStrictDerivAt.fun_div, HasFPowerSeriesAt.hasStrictDerivAt, hasStrictDerivAt_abs, Complex.hasStrictDerivAt_log, HasStrictDerivAt.congr_deriv, HasStrictDerivAt.add, HasStrictDerivAt.log, HasStrictDerivAt.const_add, Real.hasStrictDerivAt_arsinh, HasStrictDerivAt.cpow_const, HasStrictDerivAt.smul_const, HasStrictDerivAt.sub, hasStrictDerivAt_abs_neg, HasStrictDerivAt.of_notMem_tsupport, Complex.hasStrictDerivAt_cos, HasStrictDerivAt.const_smul, Polynomial.hasStrictDerivAt_aeval, Complex.hasStrictDerivAt_sin, hasStrictDerivAt_const, HasStrictDerivAt.scomp, HasStrictFDerivAt.comp_hasStrictDerivAt_of_eq, HasStrictDerivAt.comp, Real.hasStrictDerivAt_arctan, HasStrictDerivAt.fun_const_smul, Complex.hasStrictDerivAt_exp, HasStrictDerivAt.const_cpow, Complex.hasStrictDerivAt_cosh, HasStrictDerivAt.arsinh, HasStrictFDerivAt.hasStrictDerivAt, Real.hasStrictDerivAt_cos, HasStrictDerivAt.fun_sub, HasStrictDerivAt.finCons, Complex.hasStrictDerivAt_cpow_const, HasStrictDerivAt.prodMk, Polynomial.hasStrictDerivAt, Real.hasStrictDerivAt_arcsin, AffineMap.hasStrictDerivAt, Real.hasStrictDerivAt_sin, hasStrictDerivAt_one, hasStrictDerivAt_pi, ContDiff.hasStrictDerivAt, hasStrictDerivAt_exp, Real.hasStrictDerivAt_sqrt, HasStrictDerivAt.fun_neg, hasStrictDerivAt_inv, HasStrictDerivAt.ccosh, HasStrictDerivAt.sinh, hasStrictDerivAt_natCast, hasStrictDerivAt_exp_zero_of_radius_pos, hasStrictDerivAt_exp_of_mem_ball, hasStrictDerivAt_zero, hasStrictDerivAt_exp_smul_const_of_mem_ball', HasStrictDerivAt.div_const, HasStrictDerivAt.fun_mul, HasStrictDerivAt.add_const, intervalIntegral.integral_hasStrictDerivAt_right, Real.hasStrictDerivAt_tan, intervalIntegral.integral_hasStrictDerivAt_left, HasStrictDerivAt.finset_prod, Real.deriv_arcsin_aux, HasStrictDerivAt.fun_add, Real.hasStrictDerivAt_const_rpow, HasStrictDerivAt.cos, HasStrictDerivAt.iterate, hasStrictDerivAt_id, OpenPartialHomeomorph.hasStrictDerivAt_symm, Real.hasStrictDerivAt_rpow_const, hasStrictDerivAt_iff_hasStrictFDerivAt, hasStrictDerivAt_exp_smul_const_of_mem_ball, HasStrictDerivAt.const_sub, HasStrictDerivAt.neg, ContinuousLinearMap.hasStrictDerivAt, hasStrictDerivAt_exp_zero, Real.hasStrictDerivAt_exp, HasStrictDerivAt.congr_of_eventuallyEq, Complex.hasStrictDerivAt_sqrt, hasStrictDerivAt_of_hasDerivAt_of_continuousAt, HasStrictDerivAt_ofNat, ContDiffAt.hasStrictDerivAt', hasStrictDerivAt_pow, HasStrictDerivAt.sqrt, HasStrictDerivAt.ccos, HasStrictDerivAt.clm_apply, Real.hasStrictDerivAt_log_of_pos, AnalyticAt.hasStrictDerivAt, HasStrictDerivAt.clog, HasStrictDerivAt.fun_smul, HasStrictDerivAt.star, hasStrictDerivAt_neg, HasStrictDerivAt.fun_pow
|
deriv 📖 | CompOp | 424 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, UpperHalfPlane.deriv_smul, 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, AkraBazziRecurrence.isBigO_apply_r_sub_b, CPolynomialOn.iterated_deriv, ContDiff.continuous_deriv_one, intervalIntegral.integral_deriv_eq_sub, 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_conj_conj, deriv_sqrt_mul_log, intervalIntegral.deriv_integral_right, Real.fourier_deriv, 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, sum_mul_eq_sub_integral_mul', norm_sub_le_mul_volume_of_norm_deriv_le_of_le, measurable_deriv, StrictMonoOn.exists_slope_lt_deriv_aux, 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, deriv_neg_left_of_sign_deriv, 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', StrictMonoOn.exists_deriv_lt_slope_aux, 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, sum_mul_eq_sub_integral_mul₀', deriv_rpow_const, deriv_comp, logDeriv_apply, iteratedDeriv_vcomp_three, deriv.scomp, deriv_neg_right_of_sign_deriv, 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, tendsto_sum_mul_atTop_nhds_one_sub_integral₀, norm_deriv_le_of_lipschitz, ContDiff.iterate_deriv, ContDiff.deriv', sum_mul_eq_sub_integral_mul₁, 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_tsum, deriv.fun_neg, AnalyticOnNhd.deriv, deriv_zpow, AkraBazziRecurrence.eventually_deriv_one_sub_smoothingFn, deriv_const, deriv_eqOn, analyticOrderAt_deriv_of_pos, IsLocalMin.deriv_eq_zero, Real.tendsto_deriv_mul_log_atTop, HasFPowerSeriesAt.deriv, deriv_one, PeriodPair.deriv_derivWeierstrassPExcept_self, deriv_of_notMem_tsupport, 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_tsum_apply, 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, deriv_star_conj, AkraBazziRecurrence.isLittleO_deriv_one_sub_smoothingFn, deriv_fun_const_smul_field, tendsto_sum_mul_atTop_nhds_one_sub_integral, Complex.deriv_sinh, Complex.deriv_sin, Set.EqOn.deriv, MeromorphicAt.deriv, deriv_const_smul', deriv_pos_left_of_sign_deriv, 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, sum_mul_eq_sub_sub_integral_mul', ContDiffOn.continuousOn_deriv_of_isOpen, Complex.deriv_sqrt, AkraBazziRecurrence.growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn, analyticOrderAt_iterated_deriv, stronglyMeasurable_deriv_with_param, sum_mul_eq_sub_integral_mul, deriv_sin, AkraBazziRecurrence.isLittleO_deriv_smoothingFn, iteratedDeriv_vcomp_two, isTheta_deriv_ofReal_cpow_const_atTop, intervalIntegral.integral_deriv_eq_sub_uIoo, CircleIntegrable.out, contDiffOn_infty_iff_deriv_of_isOpen, StrictMonoOn.exists_slope_lt_deriv, deriv_pos_right_of_sign_deriv, StrictMonoOn.exists_deriv_lt_slope, 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, sum_mul_eq_sub_integral_mul₀, Complex.tendstoUniformlyOn_deriv_of_cthickening_subset, Real.fourierIntegral_deriv, 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', sum_mul_eq_sub_sub_integral_mul, 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, tsupport_deriv_subset, 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 | 204 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, contDiffOn_one_iff_derivWithin, 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, Complex.derivWithin_sqrt, 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, derivWithin_tsum, 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
|