| Name | Category | Theorems |
|---|
Differentiable 📖 | MathDef | 126 mathmath: differentiable_of_differentiableOn_union_of_isOpen, Real.differentiable_arctan, differentiable_const_cpow_of_neZero, ContinuousLinearEquiv.differentiable, HasFTaylorSeriesUpTo.differentiable, Real.differentiable_sinh, differentiable_fun_neg_iff, ContDiff.differentiable_deriv_two, differentiable_intCast, ContinuousAffineMap.differentiable, contDiff_one_iff_fderiv, differentiable_descPochhammer_eval, differentiable_fst, differentiable_finCons', IsBoundedLinearMap.differentiable, StrongFEPair.differentiable_Λ, Complex.analyticOnNhd_univ_iff_differentiable, differentiable_apply, differentiable_euclidean, contDiff_succ_iff_fderiv, HurwitzZeta.differentiable_expZeta_of_ne_zero, SchwartzMap.differentiable, HurwitzZeta.differentiable_hurwitzZetaOdd, HurwitzZeta.differentiable_hurwitzZeta_sub_hurwitzZeta, differentiable_snd, differentiableOn_univ, Complex.differentiable_exp, Real.differentiable_cos, VectorFourier.differentiable_fourierIntegral, Polynomial.differentiable_aeval, Complex.differentiable_iteratedDeriv_sin, ContDiff.differentiable_iteratedFDeriv, Real.differentiable_fourierIntegral, ZMod.differentiable_completedLFunction, contDiff_iff_iteratedDeriv, Real.differentiable_exp, Differentiable.fderiv_two, differentiable_inner, differentiable_add_const_iff, contDiff_iff_continuous_differentiable, MDifferentiable.differentiable, contDiff_nat_iff_iteratedDeriv, Complex.differentiable_Gammaℝ_inv, differentiable_natCast, ContinuousLinearMap.differentiable, Conformal.differentiable, ContDiff.differentiable_iteratedDeriv, differentiable_pi, Real.differentiable_iteratedDeriv_cos, differentiable_zero, Complex.differentiable_sin, DirichletCharacter.differentiable_LFunction, contDiff_succ_iff_fderiv_apply, Complex.analyticOn_univ_iff_differentiable, differentiable_const_add_iff, Real.differentiable_sin, differentiable_const, Real.differentiable_cosh, intervalIntegral.differentiable_integral_of_continuous, differentiable_pow, differentiable_piLp, Real.differentiable_mulExpNegMulSq, Complex.differentiable_one_div_Gamma, contDiff_nat_iff_continuous_differentiable, Real.differentiable_iteratedDeriv_sin, LinearIsometryEquiv.comp_differentiable_iff, ContinuousLinearEquiv.comp_differentiable_iff, differentiable_one, differentiable_neg, Real.differentiable_iteratedDeriv_cosh, HurwitzZeta.differentiable_cosZeta_of_ne_zero, Real.differentiable_fourierChar, contDiff_succ_iff_deriv, ContDiff.differentiable, differentiable_completedZeta₀, Complex.differentiable_sinh, contDiff_infty_iff_deriv, Complex.differentiable_iteratedDeriv_sinh, Function.Periodic.differentiable_qParam, Real.differentiable_fourierChar_neg_bilinear_right, differentiable_norm_rpow, Real.differentiable_iteratedDeriv_sinh, ContDiff.differentiable_iteratedDeriv', LinearIsometryEquiv.differentiable, ZMod.differentiable_completedLFunction₀, differentiable_tsum', Polynomial.differentiable, AffineMap.differentiable, ContinuousAlternatingMap.differentiable, Real.differentiable_fourierChar_neg_bilinear_left, differentiable_fun_id, differentiable_star_iff, Complex.differentiable_cosh, Complex.differentiable_iteratedDeriv_cos, Real.differentiable_arsinh, differentiable_id, IsBoundedBilinearMap.differentiable, Complex.differentiable_cos, Real.differentiable_rpow_const, differentiable_finCons, contDiff_infty_iff_fderiv, ZMod.differentiable_LFunction_of_sum_zero, ContDiff.differentiable_one, expNegInvGlue.differentiable_polynomial_eval_inv_mul, differentiable_tsum, HurwitzZeta.differentiable_completedHurwitzZetaEven₀, HurwitzZeta.differentiable_completedHurwitzZetaOdd, differentiable_of_differentiableOn_iUnion_of_isOpen, DirichletCharacter.differentiable_LFunctionTrivChar₁, Real.differentiable_fourier, mdifferentiable_iff_differentiable, HurwitzZeta.differentiable_completedSinZeta, HurwitzZeta.differentiable_hurwitzZetaEven_sub_hurwitzZetaEven, differentiable_sigmoid, WeakFEPair.differentiable_Λ₀, DirichletCharacter.differentiable_completedLFunction, differentiable_ofNat, ContinuousLinearEquiv.comp_right_differentiable_iff, diffContOnCl_univ, HurwitzZeta.differentiableAt_sinZeta, contDiff_one_iff_deriv, differentiable_circleMap, HurwitzZeta.differentiable_completedCosZeta₀, Complex.differentiable_iteratedDeriv_cosh, differentiable_neg_iff, differentiable_of_subsingleton
|
DifferentiableAt 📖 | MathDef | 183 mathmath: WeakFEPair.differentiableAt_Λ, IsBoundedLinearMap.differentiableAt, differentiableAt_comp_const_add, HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div, ConformalAt.differentiableAt, differentiableAt_comp_neg, ZMod.differentiableAt_LFunction, Complex.differentiableAt_sin, Real.differentiableAt_mulExpNegMulSq, HurwitzZeta.differentiableAt_hurwitzZeta_sub_one_div, ModularFormClass.differentiableAt_comp_ofComplex, Real.differentiableAt_arcsin, HurwitzZeta.differentiableAt_hurwitzZetaEven, differentiableAt_zpow, not_differentiableAt_of_local_left_inverse_hasDerivAt_zero, deriv_mem_iff, Filter.EventuallyEq.differentiableAt_iff, continuousOn_dslope, differentiableAt_natCast, AkraBazziRecurrence.differentiableAt_one_add_smoothingFn, differentiableAt_of_isInvertible_fderiv, not_differentiableAt_norm_zero, DiffContOnCl.differentiableAt', FDerivMeasurableAux.differentiable_set_subset_D, DifferentiableOn.eventually_differentiableAt, Complex.not_differentiableAt_Gamma_neg_nat, differentiableAt_sigmoid, Complex.differentiableAt_GammaAux, Differentiable.differentiableAt, differentiableAt_smul_iff, differentiableAt_comp_add_const, LocallyBoundedVariationOn.ae_differentiableAt, ContDiffAt.differentiableAt, ZMod.differentiableAt_completedLFunction, ContDiffPointwiseHolderAt.differentiableAt, MDifferentiableAt.differentiableAt, HasFPowerSeriesAt.differentiableAt, DifferentiableWithinAt.differentiableAt, Monotone.ae_differentiableAt, Real.differentiableAt_rpow_const_of_ne, HasDerivAt.differentiableAt, ae_differentiableAt_norm, DirichletCharacter.differentiableAt_LFunction, differentiableAt_star_iff, differentiableAt_ofNat, ProbabilityTheory.differentiableAt_mgf, FDerivMeasurableAux.D_subset_differentiable_set, FDerivMeasurableAux.differentiable_set_eq_D, differentiableAt_apply, measurableSet_of_differentiableAt_of_isComplete, hasDerivAt_deriv_iff, continuousAt_dslope_same, Real.differentiableAt_rpow_of_ne, Real.differentiableAt_log, HarmonicAt.differentiableAt_complex_partial, ContinuousLinearEquiv.differentiableAt, AkraBazziRecurrence.differentiableAt_one_sub_smoothingFn, differentiableAt_inv_iff, DifferentiableOn.differentiableAt, Real.differentiableAt_cos, LinearIsometryEquiv.comp_differentiableAt_iff, Real.differentiableAt_Gamma, HasStrictFDerivAt.differentiableAt, fderiv_mem_iff, differentiableAt_fst, dense_differentiableAt_norm, Complex.differentiableAt_exp, differentiableAt_jacobiTheta₂_fst, AffineMap.differentiableAt, Complex.differentiableAt_tan, ModularForm.differentiableAt_eta_tprod, Real.differentiableAt_log_iff, differentiableAt_complex_iff_differentiableAt_real, differentiableAt_comp_const_sub, IsBoundedBilinearMap.differentiableAt, differentiableAt_abs_neg, differentiableAt_zero, differentiableAt_const_add_iff, differentiableAt_finCons, HurwitzZeta.differentiableAt_completedHurwitzZetaEven, HurwitzZeta.differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven, HasGradientAt.differentiableAt, Real.differentiableAt_cosh, ContinuousLinearMap.differentiableAt, differentiableAt_piLp, ProbabilityTheory.differentiableAt_iteratedDeriv_mgf, Polynomial.differentiableAt_aeval, differentiableAt_norm_smul, ImplicitFunctionData.differentiableAt_implicitFunction, Real.differentiableAt_arctan, HasFTaylorSeriesUpToOn.differentiableAt, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet, ModularFormClass.differentiableAt_cuspFunction, measurableSet_of_differentiableAt, LipschitzWith.ae_differentiableAt, differentiableAt_fun_neg_iff, DirichletCharacter.differentiableAt_completedLFunction, Real.not_differentiableAt_inv_log_zero, differentiableAt_iff_comp_const_sub, Real.differentiableAt_tan, differentiableAt_add_const_iff, HasFPowerSeriesAt.eventually_differentiableAt, HurwitzZeta.differentiableAt_hurwitzZeta, differentiableAt_riemannZeta, differentiableAt_comp_add_left, differentiableAt_euclidean, ContinuousLinearEquiv.comp_differentiableAt_iff, differentiableAt_abs_pos, differentiableAt_const_cpow_of_neZero, ContinuousLinearEquiv.comp_right_differentiableAt_iff, Real.differentiableAt_arccos, Real.not_DifferentiableAt_log_mul_zero, differentiableAt_comp_add_right, Complex.not_differentiableAt_Gamma_zero, HasFDerivAt.differentiableAt, Real.not_differentiableAt_rpow_const_zero, AnalyticAt.differentiableAt, differentiableAt_intCast, HurwitzZeta.differentiableAt_completedCosZeta, differentiableAt_neg_iff, Complex.differentiableAt_cosh, Complex.differentiableAt_Gamma_nat_add_one, differentiableAt_fun_id, Real.differentiableAt_tan_of_mem_Ioo, differentiableAt_finCons', differentiableAt_jacobiTheta₂_snd, AkraBazziRecurrence.differentiableAt_smoothingFn, Real.differentiableAt_binEntropy, mellin_differentiableAt_of_isBigO_rpow_exp, Real.differentiableAt_exp, differentiableAt_const, LipschitzWith.ae_differentiableAt_of_real, Polynomial.differentiableAt, Complex.differentiableAt_Gamma_one, Real.differentiableAt_arcosh, ContDiffAt.differentiableAt_one, mdifferentiableAt_iff_differentiableAt, differentiableAt_pow, measurableSet_of_differentiableAt_of_isComplete_with_param, differentiableAt_iff_comp_add_const, differentiableAt_snd, Real.differentiableAt_negMulLog, Complex.differentiableAt_sinh, DiffContOnCl.differentiableAt, Complex.differentiableAt_log, differentiableAt_completedZeta, differentiableAt_pi, Real.differentiableAt_sinh, conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj, LinearIsometryEquiv.differentiableAt, Complex.differentiableAt_Gamma, HurwitzZeta.differentiableAt_cosZeta, mellin_differentiableAt_of_isBigO_rpow, differentiableAt_of_deriv_ne_zero, differentiableWithinAt_univ, Real.differentiableAt_qaryEntropy, ContDiffAt.differentiableAt_iteratedFDeriv, UpperHalfPlane.mdifferentiableAt_iff, differentiableAt_one, differentiableAt_inv, differentiableAt_abs, differentiableAt_dslope_of_ne, differentiableAt_iff_comp_const_add, differentiableAt_inverse, Real.differentiableAt_sin, differentiableAt_comp_sub, InformationTheory.not_differentiableAt_klFun_zero, SchwartzMap.differentiableAt, Complex.differentiableAt_cos, differentiableAt_iff_comp_sub_const, differentiableAt_id, Real.differentiableAt_binEntropy_iff_ne_zero_one, ContinuousAffineMap.differentiableAt, Complex.analyticAt_iff_eventually_differentiableAt, differentiableAt_comp_sub_const, not_differentiableAt_abs_zero, differentiableAt_iff_comp_neg, LipschitzWith.ae_differentiableAt_real, HurwitzZeta.differentiableAt_expZeta, differentiableAt_jacobiTheta, differentiableAt_iteratedDerivWithin_cexp, measurableSet_of_differentiableAt_with_param, Real.differentiableAt_negMulLog_iff
|
DifferentiableOn 📖 | MathDef | 111 mathmath: Real.differentiableOn_arcosh, differentiableOn_star_iff, mdifferentiableOn_iff, differentiableOn_pi, Real.differentiableOn_log, Real.differentiableOn_arcsin, contDiffOn_iff_continuousOn_differentiableOn, Complex.differentiableOn_dslope, differentiableOn_singleton, differentiableOn_iteratedDerivWithin_cotTerm, contDiffOn_nat_iff_continuousOn_differentiableOn_deriv, Polynomial.differentiableOn_aeval, ContinuousLinearEquiv.comp_differentiableOn_iff, HasFPowerSeriesWithinOnBall.differentiableOn, differentiableOn_univ, differentiableOn_iUnion_iff_of_isOpen, differentiableOn_dslope_of_notMem, Real.differentiableOn_rpow_const, HasFPowerSeriesOnBall.differentiableOn, IsBoundedBilinearMap.differentiableOn, differentiableOn_finCons', IsBoundedLinearMap.differentiableOn, contDiffOn_infty_iff_fderivWithin, differentiableOn_one, contDiffOn_nat_iff_continuousOn_differentiableOn, EisensteinSeries.div_linear_zpow_differentiableOn, ProbabilityTheory.differentiableOn_mgf, Complex.IsExactOn.differentiableOn, PeriodPair.differentiableOn_derivWeierstrassP, LinearIsometryEquiv.comp_differentiableOn_iff, contDiffOn_succ_iff_fderiv_of_isOpen, ContDiffOn.differentiableOn, Real.differentiableOn_Gamma_Ioi, Real.differentiableOn_mul_log, differentiableOn_fun_neg_iff, mdifferentiable_iff, differentiableOn_const, differentiableOn_add_const_iff, AkraBazziRecurrence.differentiableOn_one_add_smoothingFn, ContDiffOn.differentiableOn_one, ContDiffOn.differentiableOn_iteratedDerivWithin, differentiableOn_piLp, HasFiniteFPowerSeriesOnBall.differentiableOn, differentiableOn_pow, mdifferentiableOn_iff_of_subset_source, contDiffOn_infty_iff_fderiv_of_isOpen, Complex.analyticOn_iff_differentiableOn, Complex.differentiableOn_compl_singleton_and_continuousAt_iff, contDiffOn_succ_iff_deriv_of_isOpen, differentiableOn_ofNat, Real.differentiableOn_negMulLog, differentiableOn_union_iff_of_isOpen, Polynomial.differentiableOn, differentiableOn_neg, differentiableOn_neg_iff, ContinuousLinearEquiv.comp_right_differentiableOn_iff, MDifferentiableOn.differentiableOn, LSeries_differentiableOn, mdifferentiableOn_iff_of_mem_maximalAtlas', Real.differentiableOn_arccos, differentiableOn_inverse, spectrum.differentiableOn_inverse_one_sub_smul, differentiableOn_euclidean, Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn, mdifferentiableOn_iff_differentiableOn, ContinuousLinearEquiv.differentiableOn, SummableLocallyUniformlyOn.differentiableOn, AkraBazziRecurrence.differentiableOn_one_sub_smoothingFn, ProbabilityTheory.differentiableOn_complexMGF, contDiffOn_succ_iff_fderivWithin, IsClosed.diffContOnCl_iff, ContinuousAffineMap.differentiableOn, contDiffOn_succ_iff_fderiv_apply, contDiffOn_succ_iff_derivWithin, differentiableOn_intCast, ContinuousLinearMap.differentiableOn, AffineMap.differentiableOn, differentiableOn_congr, differentiableOn_zero, Differentiable.differentiableOn, differentiableOn_empty, PeriodPair.differentiableOn_weierstrassPExcept, Complex.analyticOnNhd_iff_differentiableOn, PeriodPair.differentiableOn_weierstrassP, differentiableOn_apply, EisensteinSeries.eisSummand_extension_differentiableOn, Set.Subsingleton.differentiableOn, HasFTaylorSeriesUpToOn.differentiableOn, ModularFormClass.differentiableOn_cuspFunction_ball, differentiableOn_abs, differentiableOn_natCast, AnalyticOn.differentiableOn, contDiffOn_infty_iff_deriv_of_isOpen, DiffContOnCl.differentiableOn, differentiableOn_finCons, ContDiffOn.differentiableOn_iteratedFDerivWithin, contDiffOn_infty_iff_derivWithin, contDiffOn_iff_continuousOn_differentiableOn_deriv, differentiableOn_id, LinearIsometryEquiv.differentiableOn, UpperHalfPlane.mdifferentiable_iff, differentiableOn_snd, mdifferentiableOn_iff_of_mem_maximalAtlas, differentiableOn_const_add_iff, mdifferentiableOn_iff_of_subset_source', differentiableOn_inv, AnalyticOnNhd.differentiableOn, differentiableOn_zpow, differentiableOn_fst, intervalIntegral.differentiableOn_integral_of_continuous, PeriodPair.differentiableOn_derivWeierstrassPExcept
|
DifferentiableWithinAt 📖 | MathDef | 122 mathmath: Polynomial.differentiableWithinAt, differentiableWithinAt_finCons', DifferentiableWithinAt.singleton, ConvexOn.differentiableWithinAt_Iio_of_mem_interior, RightDerivMeasurableAux.D_subset_differentiable_set, ContinuousAffineMap.differentiableWithinAt, MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField, not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi, mdifferentiableWithinAt_iff_of_mem_maximalAtlas, differentiableWithinAt_neg_iff, differentiableWithinAt_abs_pos, ContinuousLinearEquiv.comp_right_differentiableWithinAt_iff, mdifferentiableWithinAt_iff_target_inter, differentiableWithinAt_fun_neg_iff, differentiableWithinAt_natCast, differentiableWithinAt_inv, IsBoundedLinearMap.differentiableWithinAt, differentiableWithinAt_abs, LocallyBoundedVariationOn.ae_differentiableWithinAt, differentiableWithinAt_sub_const_iff, Real.differentiableWithinAt_arccos_Ici, differentiableWithinAt_one, DifferentiableWithinAt.of_subsingleton, ContDiffWithinAt.differentiableWithinAt_iteratedDerivWithin, mdifferentiableAt_iff, not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi, InformationTheory.not_differentiableWithinAt_klFun_Iio_zero, MDifferentiableWithinAt.differentiableWithinAt_writtenInExtChartAt, differentiableWithinAt_of_isInvertible_fderivWithin, AffineMap.differentiableWithinAt, HasGradientWithinAt.differentiableWithinAt, differentiableWithinAt_pow, RightDerivMeasurableAux.differentiable_set_subset_D, DifferentiableAt.differentiableWithinAt, MDifferentiableAt.differentiableWithinAt_writtenInExtChartAt, differentiableWithinAt_of_derivWithin_ne_zero, Filter.EventuallyEq.differentiableWithinAt_iff_of_mem, AnalyticWithinAt.differentiableWithinAt, mdifferentiableWithinAt_iff_image, differentiableWithinAt_comp_sub, mdifferentiableWithinAt_iff_differentiableWithinAt, DifferentiableWithinAt.of_finite, ConvexOn.differentiableWithinAt_Ioi_of_mem_interior, differentiableWithinAt_star_iff, measurableSet_of_differentiableWithinAt_Ici_of_isComplete, HasDerivWithinAt.differentiableWithinAt, Real.differentiableWithinAt_arcsin_Ici, differentiableWithinAt_euclidean, differentiableWithinAt_inter, ContinuousLinearMap.differentiableWithinAt, LinearIsometryEquiv.comp_differentiableWithinAt_iff, differentiableWithinAtProp_self_source, not_differentiableWithinAt_of_deriv_tendsto_atTop_Iio, HasFPowerSeriesWithinAt.differentiableWithinAt, differentiableWithinAt_abs_neg, differentiableWithinAt_dslope_of_ne, differentiableWithinAt_comp_add_right, differentiableWithinAt_const, mdifferentiableWithinAt_iff', Real.differentiableWithinAt_arcsin_Iic, differentiableWithinAt_pi, differentiableWithinAt_inter', differentiableWithinAt_congr_set', differentiableWithinAt_congr_set, MDifferentiableWithinAt.differentiableWithinAt, differentiableWithinAt_id, DifferentiableWithinAtProp_self, mdifferentiableWithinAt_iff_target_inter', LipschitzOnWith.ae_differentiableWithinAt_real, differentiableWithinAt_insert_self, ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin, Real.differentiableWithinAt_arccos_Iic, mdifferentiableWithinAt_iff_of_mem_source', mdifferentiableWithinAt_iff, HasFDerivWithinAt.differentiableWithinAt, RightDerivMeasurableAux.differentiable_set_eq_D, measurableSet_of_differentiableWithinAt_Ioi, differentiableWithinAt_inverse, AnalyticAt.differentiableWithinAt, InformationTheory.not_differentiableWithinAt_klFun_Ioi_zero, differentiableWithinAt_id', mdifferentiableAt_iff_of_mem_source, differentiableWithinAt_ofNat, hasDerivWithinAt_derivWithin_iff, differentiableWithinAt_apply, differentiableWithinAt_insert, differentiableWithinAt_snd, differentiableWithinAt_smul_iff, differentiableWithinAt_add_const_iff, not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio, not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero, Polynomial.differentiableWithinAt_aeval, differentiableWithinAt_const_sub_iff, differentiableWithinAt_univ, differentiableWithinAt_comp_add_left, differentiableWithinAt_zpow, mdifferentiableWithinAt_iff_of_mem_source, differentiableWithinAt_piLp, ContinuousLinearEquiv.differentiableWithinAt, differentiableWithinAt_congr_set_nhdsNE, fderivWithin_def, differentiableWithinAt_complex_iff_differentiableWithinAt_real, ContDiffWithinAt.differentiableWithinAt', DifferentiableWithinAt.empty, ContDiffWithinAt.differentiableWithinAt, LipschitzOnWith.ae_differentiableWithinAt, measurableSet_of_differentiableWithinAt_Ici, differentiableWithinAt_intCast, ContinuousLinearEquiv.comp_differentiableWithinAt_iff, differentiableWithinAt_const_add_iff, fderivWithin_mem_iff, LinearIsometryEquiv.differentiableWithinAt, differentiableWithinAt_fst, MonotoneOn.ae_differentiableWithinAt, derivWithin_mem_iff, differentiableWithinAt_zero, differentiableWithinAtProp_self_target, differentiableWithinAt_Ioi_iff_Ici, differentiableWithinAt_finCons, IsBoundedBilinearMap.differentiableWithinAt, differentiableWithinAt_congr_nhds, Filter.EventuallyEq.differentiableWithinAt_iff
|
HasFDerivAt 📖 | MathDef | 136 mathmath: hasFDerivAt_iff_hasDerivAt, hasFDerivAt_comp_add_right, Real.hasFDerivAt_fourierChar_neg_bilinear_left, hasFDerivAt_iff_hasGradientAt, IsBoundedBilinearMap.hasFDerivAt, hasFDerivAt_one, hasFDerivAt_multiset_prod, intervalIntegral.integral_hasFDerivAt_of_tendsto_ae, hasFDerivAt_stereoInvFunAux, HasFTaylorSeriesUpTo.hasFDerivAt, DifferentiableOn.hasFDerivAt, ContinuousLinearEquiv.comp_hasFDerivAt_iff, ContinuousLinearMap.hasFDerivAt, HasFDerivAt.of_notMem_tsupport, LipschitzWith.hasFDerivAt_of_hasLineDerivAt_of_closure, IsContDiffImplicitAt.hasFDerivAt, hasFDerivAt_snd, intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip, hasFDerivAt_add_const_iff, HasFDerivAt.curveIntegral_segment_source, hasFDerivAt_sub_const_iff, Convex.exists_forall_hasFDerivAt_of_fderiv_symmetric, VectorFourier.hasFDerivAt_fourierIntegral, hasFDerivAt_ringInverse, contDiffAt_one_iff, hasFDerivAt_finCons, HasFTaylorSeriesUpToOn.eventually_hasFDerivAt, hasFDerivAt_of_subsingleton, hasFDerivAt_jacobiTheta₂_term, HasDerivAt.hasFDerivAt, hasFDerivAt_norm_rpow, Real.hasFDerivAt_fourier, PiLp.hasFDerivAt_toLp, hasFDerivAt_id, hasFDerivAt_apply, MeasureTheory.hasFDerivAt_convolution_right_with_param, hasFDerivAt_prodMk_left, HasCompactSupport.hasFDerivAt_convolution_right, hasFDerivAt_list_prod', HasDerivAt.complexToReal_fderiv', HasDerivAt.complexToReal_fderiv, hasFDerivAt_exp_smul_const', hasFDerivAt_finCons', Complex.hasFDerivAt_cpow, hasFTaylorSeriesUpTo_top_iff', hasFDerivAt_iff_tendsto, Polynomial.hasFDerivAt, hasFDerivAt_ofNat, hasFDerivAt_list_prod_finRange', HasGradientAt.hasFDerivAt, hasFDerivAt_of_tendsto_locally_uniformly_on', hasFTaylorSeriesUpTo_succ_nat_iff_right, hasFDerivWithinAt_of_mem_nhds, hasFDerivAt_const_add_iff, ContinuousLinearEquiv.comp_right_hasFDerivAt_iff, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMap, SchwartzMap.hasFDerivAt, HasFDerivWithinAt.hasFDerivAt_of_univ, Polynomial.hasFDerivAt_aeval, hasFDerivAt_pow, hasFDerivAt_single, HasFTaylorSeriesUpToOn.hasFDerivAt, HasStrictFDerivAt.hasFDerivAt, hasDerivAt_iff_hasFDerivAt, hasFDerivAt_zero_of_eventually_const, contDiffAt_succ_iff_hasFDerivAt, hasFDerivAt_const, hasFDerivAt_polarCoord_symm, Filter.EventuallyEq.hasFDerivAt_iff, hasFDerivAt_exp_zero, HasMFDerivAt.hasFDerivAt, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMapBasis, hasGradientAt_iff_hasFDerivAt, hasFDerivAt_exp_smul_const_of_mem_ball, LinearIsometryEquiv.hasFDerivAt, HasFPowerSeriesAt.hasFDerivAt, hasFDerivAt_exp_smul_const, hasFDerivAt_jacobiTheta₂, HasDerivAt.hasFDerivAt_equiv, hasFDerivAt_update, DifferentiableAt.hasFDerivAt, ContinuousAffineMap.hasFDerivAt, hasFDerivAt_comp_sub, intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le, ContinuousLinearEquiv.comp_hasFDerivAt_iff', ContinuousMultilinearMap.hasFDerivAt, Real.hasFDerivAt_fourierIntegral, hasFDerivAt_pow', HasFPowerSeriesOnBall.hasFDerivAt, hasFDerivAt_sub_const, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, hasFDerivAt_natCast, hasFDerivAt_intCast, contDiff_one_iff_hasFDerivAt, EuclideanGeometry.hasFDerivAt_inversion, PiLp.hasFDerivAt_ofLp, HasFDerivAt.curveIntegral_segment_source', NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm, hasFDerivAt_pi_polarCoord_symm, HasFDerivWithinAt.hasFDerivAt, hasFDerivAt_integral_of_dominated_of_fderiv_le, hasFDerivAt_comp_add_left, LinearIsometryEquiv.comp_hasFDerivAt_iff', hasMFDerivAt_iff_hasFDerivAt, LinearIsometryEquiv.comp_hasFDerivAt_iff, PiLp.hasFDerivAt_apply, ContinuousLinearEquiv.hasFDerivAt, hasFDerivAt_integral_of_dominated_of_fderiv_le'', hasFDerivAt_zero, HasFiniteFPowerSeriesOnBall.hasFDerivAt, Real.hasFDerivAt_fourierChar_neg_bilinear_right, hasFDerivAt_exp_smul_const_of_mem_ball', IsBoundedLinearMap.hasFDerivAt, hasFDerivAt_exp_zero_of_radius_pos, hasFDerivWithinAt_of_isOpen, HasFTaylorSeriesUpTo.fderiv, intervalIntegral.integral_hasFDerivAt, ContinuousAlternatingMap.hasFDerivAt, ContinuousLinearEquiv.comp_right_hasFDerivAt_iff', hasFDerivAt_inv', VectorFourier.hasFDerivAt_fourierChar_smul, hasFDerivAt_exp, hasFDerivAt_inv, hasFDerivAt_fst, hasFDerivAt_pi', hasFDerivWithinAt_univ, hasFDerivAt_list_prod_attach', hasFDerivAt_iff_isLittleO_nhds_zero, hasFDerivAt_exp_of_mem_ball, hasFDerivAt_stereoInvFunAux_comp_coe, contDiff_succ_iff_hasFDerivAt, HasCompactSupport.hasFDerivAt_convolution_left, hasFDerivAt_pi, Asymptotics.IsBigO.hasFDerivAt, hasFDerivAt_prodMk_right, hasFDerivAt_finset_prod
|
HasFDerivAtFilter 📖 | CompData | 26 mathmath: hasFDerivAtFilter_pi, hasFDerivAtFilter_sub_const_iff, hasFDerivAtFilter_ofNat, hasFDerivAtFilter_zero, HasFDerivAt.hasFDerivAtFilter, hasFDerivAtFilter_const, hasFDerivAtFilter_iff_isLittleO, ContinuousLinearMap.hasFDerivAtFilter, hasFDerivAtFilter_iff_hasDerivAtFilter, hasFDerivAtFilter_snd, hasFDerivAtFilter_fst, IsBoundedLinearMap.hasFDerivAtFilter, hasFDerivAtFilter_iff_isLittleOTVS, ContinuousAffineMap.hasFDerivAtFilter, hasFDerivAtFilter_finCons, Filter.EventuallyEq.hasFDerivAtFilter_iff, hasFDerivAtFilter_id, hasFDerivAtFilter_iff_tendsto, HasFDerivAtFilter.of_isLittleO, hasFDerivAtFilter_finCons', hasFDerivAtFilter_natCast, hasFDerivAtFilter_const_add_iff, hasFDerivAtFilter_add_const_iff, hasFDerivAtFilter_pi', hasFDerivAtFilter_intCast, hasFDerivAtFilter_one
|
HasFDerivWithinAt 📖 | MathDef | 101 mathmath: Filter.EventuallyEq.hasFDerivWithinAt_iff, hasFDerivWithinAt_const, hasFTaylorSeriesUpToOn_top_iff_right, HasFDerivWithinAt.of_subsingleton, HasDerivWithinAt.complexToReal_fderiv', HasFDerivWithinAt.of_finite, HasFDerivWithinAt.empty, hasFDerivWithinAt_comp_smul_iff_smul, hasFDerivWithinAt_sub_const_iff, hasFDerivWithinAt_inv, HasDerivWithinAt.hasFDerivWithinAt, hasFDerivWithinAt_pi', HasFDerivAt.hasFDerivWithinAt, hasFDerivWithinAt_intCast, hasFDerivWithinAt_inter', ContDiffWithinAt.hasFDerivWithinAt_nhds, HasFDerivWithinAt.of_notMem_tsupport, hasFDerivWithinAt_finCons, hasGradientWithinAt_iff_hasFDerivWithinAt, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff', HasFTaylorSeriesUpToOn.hasFDerivWithinAt, hasDerivWithinAt_iff_hasFDerivWithinAt, hasFDerivWithinAt_finCons', hasFTaylorSeriesUpToOn_top_iff', HasDerivWithinAt.complexToReal_fderiv, HasFDerivWithinAt.singleton, hasFDerivWithinAt_const_add_iff, hasFDerivWithinAt_iff_hasDerivWithinAt, hasFTaylorSeriesUpToOn_succ_iff_right, hasFDerivWithinAt_pow', HasMFDerivWithinAt.hasFDerivWithinAt, hasFDerivWithinAt_one, hasFDerivWithinAt_of_mem_nhds, hasFDerivWithinAt_zero, hasFDerivWithinAt_piLp, hasFDerivWithinAt_singleton, IsBoundedBilinearMap.hasFDerivWithinAt, hasFTaylorSeriesUpToOn_succ_nat_iff_right, hasFDerivWithinAt_comp_smul_smul_iff, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contDiffOn_succ_iff_hasFDerivWithinAt, ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff', hasFDerivWithinAt_tangentCoordChange, HasFDerivWithinAt.of_notMem_closure, HasFTaylorSeriesUpToOn.fderivWithin, ContinuousLinearEquiv.hasFDerivWithinAt, ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff, hasFDerivWithinAt_closure_of_tendsto_fderiv, ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff, ContinuousLinearMap.hasFDerivWithinAt, Asymptotics.IsBigO.hasFDerivWithinAt, ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff', hasFDerivWithinAt_euclidean, Convex.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric, hasFDerivWithinAt_natCast, Filter.EventuallyEq.hasFDerivWithinAt_iff_of_mem, HasFDerivWithinAt.curveIntegral_segment_source, hasFDerivWithinAt_insert_self, hasFDerivWithinAt_diff_singleton, hasFDerivWithinAt_comp_add_right, intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae, hasFDerivWithinAt_fst, intervalIntegral.integral_hasFDerivWithinAt, hasFTaylorSeriesUpToOn_succ_iff_left, hasFDerivWithinAt_ofNat, hasFDerivWithinAt_congr_set', hasFDerivWithinAt_iff_hasGradientWithinAt, hasFDerivWithinAt_congr_set_nhdsNE, hasFDerivWithinAt_pi, ContinuousAlternatingMap.hasFDerivWithinAt, Polynomial.hasFDerivWithinAt_aeval, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, LinearIsometryEquiv.hasFDerivWithinAt, ContinuousAffineMap.hasFDerivWithinAt, hasFDerivWithinAt_add_const_iff, HasFDerivWithinAt.of_not_accPt, hasFDerivWithinAt_comp_sub, hasFDerivWithinAt_congr_set, hasFDerivWithinAt_diff_singleton_self, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff, IsBoundedLinearMap.hasFDerivWithinAt, HasFDerivWithinAt.curveIntegral_segment_source', hasFDerivWithinAt_inter, hasFDerivWithinAt_of_isOpen, hasFDerivWithinAt_insert, fderivWithin_def, hasFDerivWithinAt_pow, Polynomial.hasFDerivWithinAt, hasFDerivWithinAt_of_subsingleton, hasFDerivWithinAt_iff_tendsto, HasFPowerSeriesWithinAt.hasFDerivWithinAt, HasGradientWithinAt.hasFDerivWithinAt, hasFDerivWithinAt_univ, HasFPowerSeriesWithinOnBall.hasFDerivWithinAt, hasMFDerivWithinAt_iff_hasFDerivWithinAt, DifferentiableWithinAt.hasFDerivWithinAt, hasFDerivWithinAt_comp_add_left, hasFDerivWithinAt_snd, contDiffWithinAt_succ_iff_hasFDerivWithinAt, hasFDerivWithinAt_apply, hasFDerivWithinAt_id
|
HasStrictFDerivAt 📖 | CompData | 89 mathmath: hasStrictFDerivAt_const_add_iff, hasStrictFDerivAt_apply, LinearIsometryEquiv.hasStrictFDerivAt, hasStrictFDerivAt_exp_of_mem_ball, hasStrictFDerivAt_list_prod_finRange', ContinuousAlternatingMap.hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff, hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt, ContDiff.hasStrictFDerivAt, ImplicitFunctionData.hasStrictFDerivAt_leftFun, ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap, ImplicitFunctionData.implicitFunction_hasStrictFDerivAt, hasStrictFDerivAt_snd, hasStrictFDerivAt_iff_isLittleOTVS, Complex.hasStrictFDerivAt_exp_real, hasStrictFDerivAt_exp_smul_const_of_mem_ball', Real.hasStrictFDerivAt_rpow_of_pos, hasStrictFDerivAt_pi', hasStrictFDerivAt_natCast, Complex.hasStrictFDerivAt_cpow', hasStrictFDerivAt_multiset_prod, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, hasStrictFDerivAt_exp, hasStrictFDerivAt_iff_isLittleO, HasStrictFDerivAt.of_notMem_tsupport, hasStrictFDerivAt_exp_smul_const', Complex.hasStrictFDerivAt_cpow, ImplicitFunctionData.hasStrictFDerivAt_implicitFunction_fderiv, ContDiffAt.hasStrictFDerivAt', hasStrictFDerivAt_finCons, ContinuousAlternatingMap.hasStrictFDerivAt, ContinuousAffineMap.hasStrictFDerivAt, hasStrictFDerivAt_iff_hasStrictDerivAt, intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae, hasStrictFDerivAt_piLp, intervalIntegral.integral_hasStrictFDerivAt, ContinuousMultilinearMap.hasStrictFDerivAt, Filter.EventuallyEq.hasStrictFDerivAt_iff, HasStrictDerivAt.hasStrictFDerivAt, hasStrictFDerivAt_zero, ContDiffAt.hasStrictFDerivAt, hasStrictFDerivAt_norm_sq, ImplicitFunctionData.hasStrictFDerivAt, hasStrictFDerivAt_inv, HasStrictDerivAt.complexToReal_fderiv', hasStrictFDerivAt_pow', hasStrictFDerivAt_finCons', ContinuousLinearMap.hasStrictFDerivAt, hasStrictFDerivAt_list_prod_attach', hasStrictFDerivAt_ringInverse, PiLp.hasStrictFDerivAt_apply, hasStrictFDerivAt_fst, hasStrictFDerivAt_finset_prod, IsBoundedBilinearMap.hasStrictFDerivAt, hasStrictFDerivAt_exp_zero_of_radius_pos, HasFTaylorSeriesUpToOn.hasStrictFDerivAt, ContinuousLinearEquiv.hasStrictFDerivAt, hasStrictFDerivAt_exp_zero, ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap, hasStrictFDerivAt_one, hasStrictFDerivAt_sub_const_iff, hasStrictFDerivAt_ofNat, HasStrictFDerivAt.of_isLittleO, hasStrictFDerivAt_list_prod, HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt, hasStrictFDerivAt_add_const_iff, hasStrictFDerivAt_inv', hasStrictFDerivAt_exp_smul_const, Complex.hasStrictFDerivAt_log_real, hasStrictFDerivAt_const, hasStrictFDerivAt_list_prod', hasStrictFDerivAt_pow, PiLp.hasStrictFDerivAt_ofLp, Real.hasStrictFDerivAt_rpow_of_neg, hasStrictDerivAt_iff_hasStrictFDerivAt, HasStrictDerivAt.complexToReal_fderiv, HasFPowerSeriesAt.hasStrictFDerivAt, HasStrictDerivAt.hasStrictFDerivAt_equiv, hasStrictFDerivAt_intCast, ImplicitFunctionData.hasStrictFDerivAt_rightFun, AnalyticAt.hasStrictFDerivAt, ContinuousMultilinearMap.hasStrictFDerivAt_uncurry, hasStrictFDerivAt_pi, hasStrictFDerivAt_id, hasStrictFDerivAt_sub_const, LinearIsometryEquiv.comp_hasStrictFDerivAt_iff, ContinuousLinearEquiv.comp_hasStrictFDerivAt_iff, hasStrictFDerivAt_exp_smul_const_of_mem_ball, PiLp.hasStrictFDerivAt_toLp, hasStrictFDerivAt_euclidean
|
fderiv 📖 | CompOp | 263 mathmath: Polynomial.fderiv, fderiv_iteratedFDeriv, DifferentiableAt.fderivWithin, fderiv_snd, LinearIsometryEquiv.comp_fderiv, extDeriv_constOfIsEmpty, Real.fderiv_fourierIntegral, ContDiff.fderiv_succ, fderiv_intCast, ContinuousAffineMap.fderiv, MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv, ImplicitFunctionData.isInvertible_fderiv_prodFun, ContDiff.hasStrictFDerivAt, VectorField.fderiv_apply_lieBracket, fderiv_id, Real.fderiv_fourierChar_neg_bilinear_right_apply, intervalIntegral.fderiv_integral_of_tendsto_ae, ContDiffAt.fderiv_right_succ, fderiv_multiset_prod, VectorField.fderiv_apply_lieBracket_of_isSymmSndFDerivAt, fderiv_clm_comp, fderiv_continuousAlternatingMap_apply_const, DifferentiableOn.hasFDerivAt, Differentiable.fderiv_norm_rpow, fderiv_comp_deriv, fderiv_fun_pow, FDerivMeasurableAux.differentiable_set_subset_D, fderiv_fun_smul, contDiff_one_iff_fderiv, SchwartzMap.fderivCLM_apply, IsLocalMax.fderiv_eq_zero, fderiv_const_smul_field, DifferentiableAt.fderiv_prodMk, ContDiffAt.continuousAt_fderiv, fderiv_fun_pow', ContDiffAt.fderiv_succ, fderiv_add_const, fderiv_sum, HarmonicAt.analyticAt_complex_partial, fderiv_ofNat, enorm_fderiv_norm_rpow_le, fderiv_eq_deriv_mul, fderiv_continuousAlternatingMapCompContinuousLinearMap, Real.fderiv_fourier, ContinuousLinearMap.fderiv, fderiv_neg, fderiv_fun_sub, HasCompactSupport.fderiv, contDiff_succ_iff_fderiv, LinearIsometryEquiv.fderiv, Filter.EventuallyEq.fderiv_eq, fderiv.log, fderiv_continuousAlternatingMap_apply, deriv_fderiv, fderiv_smul, fderivWithin_eq_fderiv, DifferentiableAt.fderiv_norm_self, ContDiff.continuous_fderiv_apply, IsLocalExtr.fderiv_eq_zero, HasFPowerSeriesOnBall.fderiv_eq, ContinuousLinearMap.fderiv_of_bilinear, fderiv_mul_const', extDeriv_apply_vectorField, ContinuousLinearEquiv.comp_fderiv, ContDiffAt.fderiv_right, FDerivMeasurableAux.D_subset_differentiable_set, FDerivMeasurableAux.differentiable_set_eq_D, ContDiffOn.fderiv_of_isOpen, ContinuousLinearEquiv.comp_right_fderiv, AnalyticOnNhd.fderiv_of_isOpen, fderivWithin_of_isOpen, fderiv_inverse, HasFPowerSeriesOnBall.fderiv, ImplicitFunctionData.leftDeriv_fderiv_implicitFunction, measurableSet_of_differentiableAt_of_isComplete, fderiv_pow, fderiv_one, ContDiff.continuous_fderiv, HarmonicAt.differentiableAt_complex_partial, MeasureTheory.hasFDerivAt_convolution_right_with_param, fderiv_pow', fderiv_mul, fderivWithin_univ, HasCompactSupport.hasFDerivAt_convolution_right, Continuous.fderiv, norm_fderiv_le_of_lipschitz, ImplicitFunctionData.hasStrictFDerivAt_implicitFunction_fderiv, Differentiable.fderiv_two, fderiv_fun_add, fderiv_pow_ring, DifferentiableAt.fderiv_restrictScalars, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq_inner, contDiffOn_succ_iff_fderiv_of_isOpen, Polynomial.fderiv_aeval, fderivWithin_fderivWithin_eq_of_mem_nhds, fderiv_const_add, fderiv_mul', VectorField.lieBracket_fmul_left, fderiv_comp_fderivWithin, fderiv_mem_iff, VectorField.lieBracket_eq, fderiv_norm_smul_neg, fderiv_fun_sum, fderiv_const_smul_of_invertible, fderivWithin_of_mem_nhds, differentiableAt_complex_iff_differentiableAt_real, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one, norm_fderiv_norm_rpow_le, VectorFourier.fderiv_fourierIntegral, fderiv_cos, fderiv.snd, iteratedDeriv_vcomp_three, HasFPowerSeriesAt.fderiv_eq, ContDiffAt.hasStrictFDerivAt, fderiv_eq, conformalAt_iff_isConformalMap_fderiv, fderiv_const_mul, fderiv_sub_const, fderiv_exp, fderiv_arctan, contDiffOn_infty_iff_fderiv_of_isOpen, SchwartzMap.hasFDerivAt, fderiv_pow_ring', fderiv_natCast, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_le, fderiv_const, norm_fderiv_iteratedFDeriv, conformalFactorAt_inner_eq_mul_inner', fderiv_sub, measurable_fderiv_apply_const, fderiv_inv, contDiff_succ_iff_fderiv_apply, fderiv_ccos, fderiv_update, ContDiff.fderiv_apply, Filter.EventuallyEq.fderiv, fderiv_apply_one_eq_deriv, fderiv_continuousMultilinear_apply_const_apply, fderiv_add, IsBoundedBilinearMap.fderiv, iteratedFDeriv_one_apply, fderiv_fun_mul', iteratedFDeriv_succ_apply_right, fderiv_deriv, ImplicitFunctionData.fderiv_implicitFunction_apply_eq_iff, norm_fderiv_norm, fderiv_comp, fderiv_finset_prod, fderiv_continuousAlternatingMap_apply_apply, fderiv_comp_add_right, ContDiffOn.continuousOn_fderiv_of_isOpen, fderiv_def, fderiv_zero_of_not_differentiableAt, DifferentiableAt.hasFDerivAt, fderiv_smul_const, fderiv_fun_neg, fderiv_const_sub, tsupport_fderiv_subset, fderiv_id', FDerivMeasurableAux.mem_A_of_differentiable, ContinuousLinearEquiv.fderiv, AnalyticOnNhd.fderiv, iteratedFDeriv_succ_eq_comp_right, VectorField.lieBracket_smul_left, fderiv_continuousLinearEquiv_comp, nnnorm_fderiv_norm_rpow_le, fderiv_norm_smul, HasFDerivAt.fderiv, fderiv_continuousMultilinearMapCompContinuousLinearMap, fderiv_sinh, HasCompactSupport.fderiv_apply, fderiv_continuousMultilinear_apply_const, fderiv_zero, fderiv_comp', norm_iteratedFDeriv_one, norm_deriv_eq_norm_fderiv, MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux, ContDiffAt.fderiv, fderiv_fun_const_smul, tsupport_fderiv_apply_subset, fderiv.fst, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq, toSpanSingleton_deriv, fderiv_ccosh, ContDiffPointwiseHolderAt.fderiv, fderiv_fun_mul, extDeriv_apply_vectorField_of_pairwise_commute, norm_fderiv_le_of_lipschitzOn, CPolynomialOn.fderiv, measurable_fderiv_with_param, SchwartzMap.lineDerivOp_apply_eq_fderiv, measurableSet_of_differentiableAt_of_isComplete_with_param, fderiv_sqrt, fderiv_clm_apply, fderiv_star, Complex.norm_fderiv_le_one_of_mapsTo_ball, ContDiff.contDiff_fderiv_apply, differentiableAt_iff_restrictScalars, extDeriv_pullback, HasFiniteFPowerSeriesOnBall.fderiv', measurable_fderiv, iteratedFDeriv_two_apply, fderiv_fst, fderiv_norm_smul_pos, fderiv_mul_const, fderiv_csinh, iteratedFDeriv_succ_eq_comp_left, fderiv_of_notMem_tsupport, mfderiv_eq_fderiv, fderiv_comp_add_left, IsLocalMin.fderiv_eq_zero, fderiv_comp_sub, iteratedDeriv_vcomp_two, fderiv_norm_rpow, AnalyticAt.fderiv, fderiv_comp_smul, ContDiff.fderiv_right, fderiv_csin, norm_fderiv_le_of_lip', fderiv_cosh, support_fderiv_subset, contDiff_infty_iff_fderiv, HasGradientAt.fderiv_apply, VectorField.lieBracket_smul_right, HasFiniteFPowerSeriesOnBall.fderiv_eq, intervalIntegral.fderiv_integral, fderiv_fun_const, inner_gradient_left, MeasureTheory.eLpNorm_le_eLpNorm_fderiv, IsBoundedLinearMap.fderiv, fderiv_pi, Complex.norm_fderiv_le_div_of_mapsTo_ball, fderiv_const_smul_of_field, fderiv_comp_deriv_of_eq, ContDiff.fderiv, fderiv_list_prod', ImplicitFunctionData.rightDeriv_fderiv_implicitFunction, fderiv_continuousAlternatingMap_apply_const_apply, norm_fderiv_norm_id_rpow, fderiv_const_smul, measurable_fderiv_apply_const_with_param, fderiv_continuousLinearEquiv_comp', Real.fderiv_fourierChar_neg_bilinear_left_apply, AnalyticAt.hasStrictFDerivAt, inner_gradient_right, fderiv_single, DifferentiableAt.lineDeriv_eq_fderiv, LinearIsometryEquiv.comp_fderiv', fderiv_norm_sq_apply, fderiv_sin, norm_iteratedFDeriv_fderiv, fderiv_norm_sq, conformalAt_iff', extDeriv_apply, HasCompactSupport.hasFDerivAt_convolution_left, fderiv_inner_apply, fderiv_const_apply, HasFiniteFPowerSeriesOnBall.fderiv, fderiv_eq_smul_deriv, iteratedFDeriv_succ_apply_left, IsSymmSndFDerivAt.eq, fderiv_inv', Continuous.fderiv_one
|
fderivWithin 📖 | CompOp | 208 mathmath: IsLocalMaxOn.fderivWithin_nonpos, DifferentiableAt.fderivWithin, fderivWithin_ofNat, fderivWithin_comp_derivWithin_of_eq, Filter.EventuallyEq.fderivWithin, fderivWithin_one, fderivWithin_comp_add_left, fderivWithin_fun_smul, fderivWithin_fderivWithin_eq_of_mem_nhdsWithin, norm_iteratedFDerivWithin_one, fderivWithin_csinh, LinearIsometryEquiv.comp_fderivWithin, fderivWithin_fun_pow', iteratedFDerivWithin_succ_eq_comp_right, iteratedDerivWithin_vcomp_two, LinearIsometryEquiv.fderivWithin, fderivWithin_zero_of_not_accPt, dist_iteratedFDerivWithin_one, derivWithin_fderivWithin, extDerivWithin_pullback, fderivWithin_fderivWithin, lintegral_fderiv_lineMap_eq_edist, Filter.EventuallyEq.fderivWithin_eq_of_insert, tangentCoordChange_def, inner_gradientWithin_right, iteratedFDerivWithin_succ_eq_comp_left, Filter.EventuallyEq.fderivWithin_eq, fderivWithin_sinh, fderivWithin_intCast, DifferentiableWithinAt.fderivWithin_congr_mono, DifferentiableWithinAt.fderivWithin_prodMk, fderivWithin_zero, fderivWithin_const_sub, HasFPowerSeriesWithinOnBall.fderivWithin, fderivWithin_ccosh, fderivWithin_const_mul, fderivWithin_pi, fderivWithin_star, fderivWithin_fun_neg, extDerivWithin_constOfIsEmpty, fderivWithin_sin, fderivWithin_congr', fderivWithin_finset_prod, fderivWithin_eq_fderiv, fderivWithin_eventually_congr_set', fderivWithin_id, fderivWithin_continuousAlternatingMap_apply_const_apply, iteratedFDerivWithin_succ_apply_right, AnalyticOn.fderivWithin, IsBoundedBilinearMap.fderivWithin, HasFPowerSeriesWithinAt.fderivWithin_eq, contDiffOn_infty_iff_fderivWithin, fderivWithin_of_isOpen, fderivWithin_of_mem_nhdsWithin, fderivWithin_continuousMultilinear_apply_const_apply, fderivWithin_comp_derivWithin, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, fderivWithin_inv', ContinuousLinearMap.fderivWithin_of_bilinear, TangentBundle.trivializationAt_apply, fderivWithin_univ, fderivWithin_sub_const, fderivWithin.snd, fderivWithin_cos, fderivWithin_const_add, fderivWithin_continuousMultilinear_apply_const, fderivWithin_ccos, VectorField.lieBracketWithin_smul_left, extDerivWithin_apply_vectorField_of_pairwise_commute, ContDiffWithinAt.fderivWithin'', fderivWithin_fun_sub, fderivWithin_fun_mul', fderivWithin_fderivWithin_eq_of_mem_nhds, fderivWithin_const_smul_of_field, fderiv_comp_fderivWithin, ContDiffWithinAt.continuousWithinAt_fderivWithin, fderivWithin_fderivWithin_eq_of_eventuallyEq, iteratedFDerivWithin_one_apply, fderivWithin_iteratedFDerivWithin, fderivWithin_of_mem_nhds, fderivWithin_congr_set', fderivWithin_id', fderivWithin_mul_const', fderivWithin_smul, fderivWithin_comp_smul_eq_fderivWithin_smul, fderivWithin_zero_of_notMem_closure, VectorField.fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt, fderivWithin_fun_pow, iteratedFDerivWithin_two_apply', Filter.EventuallyEq.fderivWithin_eq_of_mem, fderivWithin_add_const, MDifferentiableAt.mfderiv, fderivWithin_congr, fderivWithin_const, iteratedFDerivWithin_succ_apply_left, ContinuousLinearEquiv.comp_right_fderivWithin, fderivWithin_comp_of_eq, MDifferentiableWithinAt.mfderivWithin, fderivWithin_snd, Filter.EventuallyEq.fderivWithin_eq_of_nhds, fderivWithin.log, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, ContDiffOn.continuousOn_fderivWithin_apply, differentiableWithinAt_iff_restrictScalars, tangentBundleCore_coordChange, fderivWithin_comp', norm_fderivWithin_iteratedFDerivWithin, contDiffOn_fderiv_coord_change, HasGradientWithinAt.fderivWithin_apply, norm_derivWithin_eq_norm_fderivWithin, extDerivWithin_apply_vectorField, ContDiffWithinAt.fderivWithin', ContDiffOn.continuousOn_fderivWithin, fderivWithin_const_smul_of_invertible, fderivWithin_exp, DifferentiableWithinAt.restrictScalars_fderivWithin, fderivWithin_multiset_prod, fderivWithin_neg, fderivWithin_comp₃, HasFDerivWithinAt.fderivWithin, fderivWithin_eventually_congr_set, fderivWithin_fun_const, fderivWithin_comp_of_eq', mfderivWithin_eq_fderivWithin, fderiv_def, HasFPowerSeriesWithinOnBall.fderivWithin_of_mem, fderivWithin_congr_set_nhdsNE, fderivWithin_continuousAlternatingMap_apply_apply, ContDiffOn.fderivWithin, toSpanSingleton_derivWithin, fderivWithin_fun_add, HasFPowerSeriesWithinOnBall.fderivWithin_eq, ContinuousAffineMap.fderivWithin, fderivWithin_sqrt, fderivWithin_natCast, fderivWithin_derivWithin, fderivWithin_const_smul_field, Polynomial.fderivWithin_aeval, Polynomial.fderivWithin, ContinuousLinearMap.fderivWithin, Filter.EventuallyEq.fderivWithin', fderivWithin_clm_comp, fderivWithin_inv, fderivWithin_csin, intervalIntegral.fderivWithin_integral_of_tendsto_ae, fderivWithin_continuousAlternatingMap_apply_const, fderivWithin_inter, fderivWithin_const_smul, VectorField.pullbackWithin_eq, ContinuousLinearEquiv.fderivWithin, VectorField.lieBracketWithin_smul_right, inner_gradientWithin_left, contDiffOn_succ_iff_fderivWithin, fderivWithin_sub, ContDiffWithinAt.fderivWithin, iteratedFDerivWithin_two_apply, contDiffOn_succ_iff_fderiv_apply, IsLocalMaxOn.fderivWithin_eq_zero, IsBoundedLinearMap.fderivWithin, fderivWithin_list_prod', fderivWithin_smul_const, fderivWithin_continuousLinearEquiv_comp, fderivWithin_const_apply, fderivWithin_pow_ring', ContDiffWithinAt.fderivWithin_right_apply, fderivWithin_mul_const, fderivWithin.fst, fderivWithin_cosh, fderivWithin_continuousAlternatingMap_apply, fderivWithin_add, IsLocalMinOn.fderivWithin_nonneg, norm_iteratedFDerivWithin_fderivWithin, extDerivWithin_apply, fderivWithin_zero_of_not_differentiableWithinAt, ContinuousLinearEquiv.comp_fderivWithin, VectorField.lieBracketWithin_eq, VectorField.fderivWithin_apply_lieBracket, fderivWithin_pow, fderivWithin_fun_const_smul, fderivWithin_arctan, fderivWithin_def, HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_analyticOn, differentiableWithinAt_complex_iff_differentiableWithinAt_real, contDiffOn_fderivWithin_apply, fderivWithin_mul', fderivWithin_comp_add_right, fderivWithin_comp_smul, fderivWithin_clm_apply, fderivWithin_fst, fderivWithin_congr_set, fderivWithin_sum, fderivWithin_pow_ring, fderivWithin_comp, IsSymmSndFDerivWithinAt.eq, fderivWithin_restrictScalars_comp, fderivWithin_fun_sum, fderivWithin_mem_iff, fderivWithin_comp_sub, fderivWithin_fun_mul, DifferentiableWithinAt.hasFDerivWithinAt, fderivWithin_mul, fderivWithin_subset, ContDiffWithinAt.fderivWithin_right, iteratedDerivWithin_vcomp_three, tangentBundleCore_coordChange_achart, ContDiffWithinAt.fderivWithin_apply, IsLocalMinOn.fderivWithin_eq_zero, fderivWithin_pow'
|