| Name | Category | Theorems |
|---|
Differentiable π | MathDef | 209 mathmath: Differentiable.arsinh, Differentiable.const_sub, differentiable_of_differentiableOn_union_of_isOpen, Real.differentiable_arctan, differentiable_const_cpow_of_neZero, Differentiable.csin, ContinuousLinearEquiv.differentiable, HasFTaylorSeriesUpTo.differentiable, Differentiable.fun_div, Differentiable.fun_sub_iff_right, Differentiable.clm_comp, Differentiable.continuousMultilinear_apply_const, Differentiable.cosh, Differentiable.add_iff_right, Real.differentiable_sinh, differentiable_fun_neg_iff, Differentiable.fun_smul, ContDiff.differentiable_deriv_two, differentiable_intCast, ContinuousAffineMap.differentiable, Differentiable.fun_inv, Differentiable.fun_neg, contDiff_one_iff_fderiv, differentiable_descPochhammer_eval, differentiable_fst, Differentiable.restrictScalars, Differentiable.zpow, Differentiable.fst, differentiable_finCons', IsBoundedLinearMap.differentiable, StrongFEPair.differentiable_Ξ, Differentiable.fun_const_smul, Complex.analyticOnNhd_univ_iff_differentiable, differentiable_apply, differentiable_euclidean, Differentiable.abs, Differentiable.ccos, Differentiable.cexp, contDiff_succ_iff_fderiv, HurwitzZeta.differentiable_expZeta_of_ne_zero, SchwartzMap.differentiable, Differentiable.pow, Differentiable.finCons, Differentiable.const_smul, Differentiable.sinh, HurwitzZeta.differentiable_hurwitzZetaOdd, HurwitzZeta.differentiable_hurwitzZeta_sub_hurwitzZeta, differentiable_snd, differentiableOn_univ, Differentiable.sub_iff_right, Complex.differentiable_exp, Real.differentiable_cos, VectorFourier.differentiable_fourierIntegral, Differentiable.sin, Polynomial.differentiable_aeval, Complex.differentiable_iteratedDeriv_sin, ContDiff.differentiable_iteratedFDeriv, Differentiable.sum, Real.differentiable_fourierIntegral, ZMod.differentiable_completedLFunction, Differentiable.fun_add, contDiff_iff_iteratedDeriv, Real.differentiable_exp, Differentiable.fderiv_two, Differentiable.fun_pow, Differentiable.inverse, differentiable_inner, differentiable_add_const_iff, contDiff_iff_continuous_differentiable, MDifferentiable.differentiable, contDiff_nat_iff_iteratedDeriv, Differentiable.arctan, Complex.differentiable_Gammaβ_inv, differentiable_natCast, Differentiable.const_add, Differentiable.continuousMultilinearMapCompContinuousLinearMap, Differentiable.sigmoid, Differentiable.neg, Differentiable.norm_rpow, ContinuousLinearMap.differentiable, Differentiable.cpow, Differentiable.mul_const, Conformal.differentiable, Differentiable.log, Differentiable.sub, ContDiff.differentiable_iteratedDeriv, Differentiable.add_iff_left, differentiable_pi, Real.differentiable_iteratedDeriv_cos, Differentiable.norm_sq, differentiable_zero, Complex.differentiable_sin, DirichletCharacter.differentiable_LFunction, Differentiable.iterate, Differentiable.prodMk, contDiff_succ_iff_fderiv_apply, Differentiable.clm_apply, Complex.analyticOn_univ_iff_differentiable, differentiable_const_add_iff, Real.differentiable_sin, differentiable_const, Differentiable.fun_sub_iff_left, Real.differentiable_cosh, Differentiable.inner, Differentiable.sub_iff_left, intervalIntegral.differentiable_integral_of_continuous, differentiable_pow, Differentiable.const_mul, Differentiable.csinh, Differentiable.exp, Differentiable.continuousAlternatingMap_apply_const, differentiable_piLp, Differentiable.add_const, Real.differentiable_mulExpNegMulSq, Complex.differentiable_one_div_Gamma, contDiff_nat_iff_continuous_differentiable, Differentiable.dist, Differentiable.sqrt, Real.differentiable_iteratedDeriv_sin, Differentiable.fun_comp, Differentiable.fun_finset_prod, LinearIsometryEquiv.comp_differentiable_iff, ContinuousLinearEquiv.comp_differentiable_iff, differentiable_one, Differentiable.inversion, differentiable_neg, Real.differentiable_iteratedDeriv_cosh, HurwitzZeta.differentiable_cosZeta_of_ne_zero, Real.differentiable_fourierChar, contDiff_succ_iff_deriv, Differentiable.fun_add_iff_right, ContDiff.differentiable, Differentiable.div_const, differentiable_completedZetaβ, Complex.differentiable_sinh, contDiff_infty_iff_deriv, Complex.differentiable_iteratedDeriv_sinh, Function.Periodic.differentiable_qParam, Real.differentiable_fourierChar_neg_bilinear_right, differentiable_pi'', differentiable_norm_rpow, Differentiable.snd, Differentiable.clog, Differentiable.sub_const, Real.differentiable_iteratedDeriv_sinh, Differentiable.fun_mul, Differentiable.fun_add_iff_left, ContDiff.differentiable_iteratedDeriv', LinearIsometryEquiv.differentiable, ZMod.differentiable_completedLFunctionβ, differentiable_tsum', Differentiable.fun_sub, Polynomial.differentiable, Differentiable.mul, AffineMap.differentiable, ContinuousAlternatingMap.differentiable, Differentiable.fun_sum, Real.differentiable_fourierChar_neg_bilinear_left, differentiable_fun_id, differentiable_star_iff, Complex.differentiable_cosh, Differentiable.finset_prod, Complex.differentiable_iteratedDeriv_cos, Real.differentiable_arsinh, differentiable_id, IsBoundedBilinearMap.differentiable, Complex.differentiable_cos, Differentiable.continuousAlternatingMap_apply, Real.differentiable_rpow_const, differentiable_finCons, contDiff_infty_iff_fderiv, Differentiable.rpow_const, Differentiable.comp, Differentiable.add, Differentiable.const_cpow, ZMod.differentiable_LFunction_of_sum_zero, ContDiff.differentiable_one, expNegInvGlue.differentiable_polynomial_eval_inv_mul, Differentiable.rpow, Differentiable.smul_const, differentiable_tsum, HurwitzZeta.differentiable_completedHurwitzZetaEvenβ, Differentiable.inv, HurwitzZeta.differentiable_completedHurwitzZetaOdd, differentiable_of_differentiableOn_iUnion_of_isOpen, Differentiable.smul, DirichletCharacter.differentiable_LFunctionTrivCharβ, Real.differentiable_fourier, Differentiable.cos, mdifferentiable_iff_differentiable, HurwitzZeta.differentiable_completedSinZeta, HurwitzZeta.differentiable_hurwitzZetaEven_sub_hurwitzZetaEven, differentiable_sigmoid, Differentiable.star, Differentiable.div, WeakFEPair.differentiable_Ξβ, Differentiable.ccosh, Differentiable.norm, 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 | 290 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, DifferentiableAt.finCons, not_differentiableAt_of_local_left_inverse_hasDerivAt_zero, DifferentiableAt.mul, deriv_mem_iff, DifferentiableAt.congr_of_eventuallyEq, DifferentiableAt.div, DifferentiableAt.fun_inv, Filter.EventuallyEq.differentiableAt_iff, DifferentiableAt.prodMap, continuousOn_dslope, differentiableAt_natCast, AkraBazziRecurrence.differentiableAt_one_add_smoothingFn, differentiableAt_of_isInvertible_fderiv, not_differentiableAt_norm_zero, DifferentiableAt.csinh, DifferentiableAt.continuousAlternatingMapCompContinuousLinearMap, DifferentiableAt.sigmoid, DiffContOnCl.differentiableAt', FDerivMeasurableAux.differentiable_set_subset_D, DifferentiableAt.clog, DifferentiableAt.zpow, DifferentiableOn.eventually_differentiableAt, Complex.not_differentiableAt_Gamma_neg_nat, differentiableAt_sigmoid, DifferentiableAt.add_const, Complex.differentiableAt_GammaAux, Differentiable.differentiableAt, differentiableAt_smul_iff, differentiableAt_comp_add_const, DifferentiableAt.fun_finset_prod, LocallyBoundedVariationOn.ae_differentiableAt, ContDiffAt.differentiableAt, DifferentiableAt.fun_neg, ZMod.differentiableAt_completedLFunction, Function.Periodic.differentiableAt_cuspFunction, DifferentiableAt.continuousAlternatingMap_apply_const, ContDiffPointwiseHolderAt.differentiableAt, MDifferentiableAt.differentiableAt, DifferentiableAt.fun_div, HasFPowerSeriesAt.differentiableAt, DifferentiableAt.smul, DifferentiableWithinAt.differentiableAt, Monotone.ae_differentiableAt, DifferentiableAt.rpow_const, Real.differentiableAt_rpow_const_of_ne, DifferentiableAt.neg, DifferentiableAt.const_cpow, DifferentiableAt.const_add, DifferentiableAt.const_smul, DifferentiableAt.add_iff_left, HasDerivAt.differentiableAt, DifferentiableAt.fun_add, DifferentiableAt.star_conj, ae_differentiableAt_norm, DirichletCharacter.differentiableAt_LFunction, differentiableAt_star_iff, DifferentiableAt.inverse, differentiableAt_ofNat, ProbabilityTheory.differentiableAt_mgf, FDerivMeasurableAux.D_subset_differentiable_set, FDerivMeasurableAux.differentiable_set_eq_D, differentiableAt_apply, differentiableAt_pi'', DifferentiableAt.ccosh, measurableSet_of_differentiableAt_of_isComplete, hasDerivAt_deriv_iff, continuousAt_dslope_same, differentiableAt_star_conj_iff, DifferentiableAt.log, Real.differentiableAt_rpow_of_ne, Real.differentiableAt_log, DifferentiableAt.inner, HarmonicAt.differentiableAt_complex_partial, ContinuousLinearEquiv.differentiableAt, AkraBazziRecurrence.differentiableAt_one_sub_smoothingFn, differentiableAt_inv_iff, DifferentiableAt.conj_conj, DifferentiableOn.differentiableAt, Real.differentiableAt_cos, DifferentiableAt.comp_ringHom, DifferentiableAt.sqrt, LinearIsometryEquiv.comp_differentiableAt_iff, Real.differentiableAt_Gamma, differentiableAt_of_fderiv_injective, HasStrictFDerivAt.differentiableAt, DifferentiableAt.continuousAlternatingMap_apply, fderiv_mem_iff, DifferentiableAt.const_mul, DifferentiableAt.fun_sub, differentiableAt_fst, dense_differentiableAt_norm, Complex.differentiableAt_exp, DifferentiableAt.continuousMultilinearMapCompContinuousLinearMap, differentiableAt_jacobiThetaβ_fst, AffineMap.differentiableAt, Complex.differentiableAt_tan, ModularForm.differentiableAt_eta_tprod, Real.differentiableAt_log_iff, DifferentiableAt.norm_sq, differentiableAt_complex_iff_differentiableAt_real, differentiableAt_comp_const_sub, IsBoundedBilinearMap.differentiableAt, differentiableAt_abs_neg, differentiableAt_zero, DifferentiableAt.inv, differentiableAt_const_add_iff, DifferentiableAt.fun_pow, differentiableAt_finCons, HurwitzZeta.differentiableAt_completedHurwitzZetaEven, DifferentiableAt.fun_sub_iff_right, HurwitzZeta.differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven, HasGradientAt.differentiableAt, Real.differentiableAt_cosh, ContinuousLinearMap.differentiableAt, DifferentiableAt.fun_const_smul, differentiableAt_piLp, ProbabilityTheory.differentiableAt_iteratedDeriv_mgf, Polynomial.differentiableAt_aeval, DifferentiableAt.cosh, differentiableAt_norm_smul, ImplicitFunctionData.differentiableAt_implicitFunction, DifferentiableAt.sub_iff_left, DifferentiableAt.prodMk, Real.differentiableAt_arctan, HasFTaylorSeriesUpToOn.differentiableAt, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet, ModularFormClass.differentiableAt_cuspFunction, measurableSet_of_differentiableAt, DifferentiableAt.mul_const, LipschitzWith.ae_differentiableAt, DifferentiableAt.of_dslope, differentiableAt_fun_neg_iff, DirichletCharacter.differentiableAt_completedLFunction, Real.not_differentiableAt_inv_log_zero, differentiableAt_iff_comp_const_sub, Real.differentiableAt_tan, DifferentiableAt.rpow, differentiableAt_add_const_iff, DifferentiableAt.iterate, DifferentiableAt.sin, DifferentiableAt.ofReal_cpow_const, DifferentiableAt.fun_sum, DifferentiableAt.differentiableAt_norm_of_smul, HasFPowerSeriesAt.eventually_differentiableAt, DifferentiableAt.arsinh, HurwitzZeta.differentiableAt_hurwitzZeta, DifferentiableAt.comp_semilinearβ, DifferentiableAt.fun_comp', DifferentiableAt.continuousMultilinear_apply_const, differentiableAt_riemannZeta, Complex.differentiableAt_sqrt, differentiableAt_comp_add_left, differentiableAt_euclidean, HurwitzZeta.differentiableAt_update_of_residue, DifferentiableAt.const_sub, ContinuousLinearEquiv.comp_differentiableAt_iff, DifferentiableAt.clm_comp, DifferentiableAt.sub, differentiableAt_abs_pos, DifferentiableAt.fun_smul, differentiableAt_const_cpow_of_neZero, DifferentiableAt.restrictScalars, ContinuousLinearEquiv.comp_right_differentiableAt_iff, Real.differentiableAt_arccos, Real.not_DifferentiableAt_log_mul_zero, differentiableAt_comp_add_right, DifferentiableAt.sub_iff_right, Complex.not_differentiableAt_Gamma_zero, HasFDerivAt.differentiableAt, Real.not_differentiableAt_rpow_const_zero, AnalyticAt.differentiableAt, differentiableAt_intCast, HurwitzZeta.differentiableAt_completedCosZeta, differentiableAt_neg_iff, Function.Periodic.eventually_differentiableAt_cuspFunction_nhds_ne_zero, Complex.differentiableAt_cosh, Complex.differentiableAt_Gamma_nat_add_one, differentiableAt_fun_id, DifferentiableAt.cpow_const, DifferentiableAt.star_star, 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, DifferentiableAt.abs, Polynomial.differentiableAt, DifferentiableAt.cos, DifferentiableAt.star, Complex.differentiableAt_Gamma_one, Real.differentiableAt_arcosh, ContDiffAt.differentiableAt_one, DifferentiableAt.fst, mdifferentiableAt_iff_differentiableAt, differentiableAt_pow, measurableSet_of_differentiableAt_of_isComplete_with_param, differentiableAt_iff_comp_add_const, DifferentiableAt.add_iff_right, DifferentiableAt.fun_add_iff_right, differentiableAt_snd, DifferentiableAt.comp, Real.differentiableAt_negMulLog, DifferentiableAt.cexp, Complex.differentiableAt_sinh, DiffContOnCl.differentiableAt, Complex.differentiableAt_log, differentiableAt_completedZeta, DifferentiableAt.sinh, differentiableAt_conj_conj_iff, DifferentiableAt.clm_apply, differentiableAt_iff_restrictScalars, differentiableAt_pi, Real.differentiableAt_sinh, conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj, DifferentiableAt.smul_const, LinearIsometryEquiv.differentiableAt, DifferentiableAt.inversion, DifferentiableAt.div_const, Complex.differentiableAt_Gamma, HurwitzZeta.differentiableAt_cosZeta, DifferentiableAt.finset_prod, DifferentiableAt.norm, mellin_differentiableAt_of_isBigO_rpow, DifferentiableAt.fun_sub_iff_left, differentiableAt_of_deriv_ne_zero, differentiableWithinAt_univ, Real.differentiableAt_qaryEntropy, DifferentiableAt.exp, ContDiffAt.differentiableAt_iteratedFDeriv, UpperHalfPlane.mdifferentiableAt_iff, differentiableAt_one, DifferentiableAt.pow, DifferentiableAt.fun_mul, DifferentiableAt.sub_const, differentiableAt_inv, Function.Periodic.differentiableAt_cuspFunction_zero, DifferentiableAt.arctan, differentiableAt_abs, DifferentiableAt.comp_semilinearβ, differentiableAt_dslope_of_ne, DifferentiableAt.ccos, differentiableAt_iff_comp_const_add, differentiableAt_inverse, Real.differentiableAt_sin, differentiableAt_comp_sub, DifferentiableAt.add, InformationTheory.not_differentiableAt_klFun_zero, SchwartzMap.differentiableAt, Complex.differentiableAt_cos, DifferentiableAt.cpow, differentiableAt_iff_comp_sub_const, differentiableAt_id, Real.differentiableAt_binEntropy_iff_ne_zero_one, ContinuousAffineMap.differentiableAt, DifferentiableAt.sum, Complex.analyticAt_iff_eventually_differentiableAt, differentiableAt_comp_sub_const, DifferentiableAt.abs_of_pos, DifferentiableAt.abs_of_neg, not_differentiableAt_abs_zero, DifferentiableAt.fun_add_iff_left, differentiableAt_iff_comp_neg, DifferentiableAt.dist, LipschitzWith.ae_differentiableAt_real, HurwitzZeta.differentiableAt_expZeta, DifferentiableAt.csin, DifferentiableAt.snd, differentiableAt_jacobiTheta, differentiableAt_iteratedDerivWithin_cexp, measurableSet_of_differentiableAt_with_param, Real.differentiableAt_negMulLog_iff, InnerProductSpace.HarmonicContOnCl.differentiableAt
|
DifferentiableOn π | MathDef | 209 mathmath: Real.differentiableOn_arcosh, DifferentiableOn.zpow, differentiableOn_star_iff, DifferentiableOn.fun_add, DifferentiableOn.restrictScalars, DifferentiableOn.sqrt, mdifferentiableOn_iff, DifferentiableOn.sub_const, DifferentiableOn.deriv, DifferentiableOn.cpow_const, differentiableOn_pi, DifferentiableOn.congr, DifferentiableOn.clm_apply, Real.differentiableOn_log, Real.differentiableOn_arcsin, DifferentiableOn.fun_mul, contDiffOn_iff_continuousOn_differentiableOn, Complex.differentiableOn_dslope, DifferentiableOn.smul_const, differentiableOn_singleton, Complex.differentiableOn_sqrt, differentiableOn_iteratedDerivWithin_cotTerm, contDiffOn_nat_iff_continuousOn_differentiableOn_deriv, Polynomial.differentiableOn_aeval, DifferentiableOn.mul, DifferentiableOn.sub, DifferentiableOn.const_cpow, DifferentiableOn.rpow, DifferentiableOn.cpow, ContinuousLinearEquiv.comp_differentiableOn_iff, DifferentiableOn.csinh, HasFPowerSeriesWithinOnBall.differentiableOn, Complex.differentiableOn_update_limUnder_of_isLittleO, contDiffOn_one_iff_derivWithin, Complex.differentiableOn_update_limUnder_of_bddAbove, 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.ccos, differentiableOn_one, contDiffOn_nat_iff_continuousOn_differentiableOn, DifferentiableOn.iUnion_of_isOpen, DifferentiableOn.add_const, EisensteinSeries.div_linear_zpow_differentiableOn, DifferentiableOn.inv, DifferentiableOn.congr_mono, ProbabilityTheory.differentiableOn_mgf, DifferentiableOn.log, Complex.IsExactOn.differentiableOn, DifferentiableOn.div_const, PeriodPair.differentiableOn_derivWeierstrassP, LinearIsometryEquiv.comp_differentiableOn_iff, DifferentiableOn.fun_const_smul, DifferentiableOn.inversion, contDiffOn_succ_iff_fderiv_of_isOpen, ContDiffOn.differentiableOn, DifferentiableOn.clm_comp, Real.differentiableOn_Gamma_Ioi, Real.differentiableOn_mul_log, differentiableOn_pi'', differentiableOn_fun_neg_iff, mdifferentiable_iff, differentiableOn_const, differentiableOn_add_const_iff, AkraBazziRecurrence.differentiableOn_one_add_smoothingFn, ContDiffOn.differentiableOn_one, DifferentiableOn.add_iff_right, ContDiffOn.differentiableOn_iteratedDerivWithin, differentiableOn_piLp, Differentiable.comp_differentiableOn, HasFiniteFPowerSeriesOnBall.differentiableOn, differentiableOn_pow, mdifferentiableOn_iff_of_subset_source, DifferentiableOn.norm_sq, DifferentiableOn.const_sub, DifferentiableOn.const_add, DifferentiableOn.sinh, DifferentiableOn.abs, DifferentiableOn.continuousMultilinear_apply_const, contDiffOn_infty_iff_fderiv_of_isOpen, Complex.analyticOn_iff_differentiableOn, Complex.differentiableOn_compl_singleton_and_continuousAt_iff, contDiffOn_succ_iff_deriv_of_isOpen, DifferentiableOn.cos, DifferentiableOn.fun_add_iff_right, DifferentiableOn.fun_comp, differentiableOn_ofNat, DifferentiableOn.continuousAlternatingMap_apply, DifferentiableOn.add_iff_left, Real.differentiableOn_negMulLog, DifferentiableOn.fun_sum, differentiableOn_union_iff_of_isOpen, DifferentiableOn.snd, Polynomial.differentiableOn, DifferentiableOn.fun_inv, differentiableOn_neg, differentiableOn_neg_iff, ContinuousLinearEquiv.comp_right_differentiableOn_iff, DifferentiableOn.continuousMultilinearMapCompContinuousLinearMap, DifferentiableOn.finset_prod, DifferentiableOn.fst, DifferentiableOn.neg, DifferentiableOn.inner, DifferentiableOn.fun_finset_prod, MDifferentiableOn.differentiableOn, DifferentiableOn.fun_pow, DifferentiableOn.sub_iff_right, LSeries_differentiableOn, mdifferentiableOn_iff_of_mem_maximalAtlas', Real.differentiableOn_arccos, DifferentiableOn.div, differentiableOn_inverse, spectrum.differentiableOn_inverse_one_sub_smul, DifferentiableOn.fun_add_iff_left, differentiableOn_euclidean, DifferentiableOn.fun_sub_iff_left, Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn, mdifferentiableOn_iff_differentiableOn, ContinuousLinearEquiv.differentiableOn, DifferentiableOn.smul, SummableLocallyUniformlyOn.differentiableOn, AkraBazziRecurrence.differentiableOn_one_sub_smoothingFn, ProbabilityTheory.differentiableOn_complexMGF, DifferentiableOn.pow, differentiableOn_of_locally_differentiableOn, DifferentiableOn.arctan, DifferentiableOn.cosh, DifferentiableOn.inverse, TendstoLocallyUniformlyOn.differentiableOn, contDiffOn_succ_iff_fderivWithin, IsClosed.diffContOnCl_iff, DifferentiableOn.cexp, ContinuousAffineMap.differentiableOn, contDiffOn_succ_iff_fderiv_apply, DifferentiableOn.sin, DifferentiableOn.dist, DifferentiableOn.ccosh, contDiffOn_succ_iff_derivWithin, DifferentiableOn.iterate, differentiableOn_intCast, DifferentiableOn.rpow_const, ContinuousLinearMap.differentiableOn, AffineMap.differentiableOn, differentiableOn_congr, differentiableOn_zero, Differentiable.differentiableOn, differentiableOn_empty, DifferentiableOn.const_smul, DifferentiableOn.const_mul, DifferentiableOn.mono, PeriodPair.differentiableOn_weierstrassPExcept, Complex.analyticOnNhd_iff_differentiableOn, DifferentiableOn.add, PeriodPair.differentiableOn_weierstrassP, DifferentiableOn.finCons, differentiableOn_apply, EisensteinSeries.eisSummand_extension_differentiableOn, DifferentiableOn.mul_const, Set.Subsingleton.differentiableOn, HasFTaylorSeriesUpToOn.differentiableOn, ModularFormClass.differentiableOn_cuspFunction_ball, DifferentiableOn.continuousAlternatingMap_apply_const, Complex.differentiableOn_update_limUnder_insert_of_isLittleO, DifferentiableOn.star, differentiableOn_abs, DifferentiableOn.clog, differentiableOn_natCast, DifferentiableOn.exp, DifferentiableOn.fun_div, AnalyticOn.differentiableOn, DifferentiableOn.prodMk, contDiffOn_infty_iff_deriv_of_isOpen, DifferentiableOn.fun_sub_iff_right, DiffContOnCl.differentiableOn, DifferentiableOn.comp, differentiableOn_finCons, DifferentiableOn.norm, ContDiffOn.differentiableOn_iteratedFDerivWithin, DifferentiableOn.arsinh, contDiffOn_infty_iff_derivWithin, contDiffOn_iff_continuousOn_differentiableOn_deriv, differentiableOn_id, DifferentiableOn.csin, DifferentiableOn.sub_iff_left, LinearIsometryEquiv.differentiableOn, UpperHalfPlane.mdifferentiable_iff, differentiableOn_snd, mdifferentiableOn_iff_of_mem_maximalAtlas, differentiableOn_const_add_iff, DifferentiableOn.fun_sub, DifferentiableOn.of_dslope, mdifferentiableOn_iff_of_subset_source', DifferentiableOn.fun_neg, differentiableOn_inv, Complex.differentiableOn_tsum_of_summable_norm, AnalyticOnNhd.differentiableOn, DifferentiableOn.sum, differentiableOn_zpow, differentiableOn_fst, DifferentiableOn.fun_smul, intervalIntegral.differentiableOn_integral_of_continuous, DifferentiableOn.union_of_isOpen, PeriodPair.differentiableOn_derivWeierstrassPExcept
|
DifferentiableWithinAt π | MathDef | 218 mathmath: Polynomial.differentiableWithinAt, differentiableWithinAt_finCons', DifferentiableWithinAt.const_sub, DifferentiableWithinAt.singleton, DifferentiableWithinAt.log, ConvexOn.differentiableWithinAt_Iio_of_mem_interior, RightDerivMeasurableAux.D_subset_differentiable_set, ContinuousAffineMap.differentiableWithinAt, MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField, not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi, DifferentiableWithinAt.finCons, mdifferentiableWithinAt_iff_of_mem_maximalAtlas, differentiableWithinAt_pi'', differentiableWithinAt_neg_iff, differentiableWithinAt_abs_pos, DifferentiableWithinAt.norm, DifferentiableWithinAt.sqrt, DifferentiableWithinAt.fun_const_smul, DifferentiableWithinAt.add, ContinuousLinearEquiv.comp_right_differentiableWithinAt_iff, mdifferentiableWithinAt_iff_target_inter, differentiableWithinAt_fun_neg_iff, differentiableWithinAt_natCast, differentiableWithinAt_inv, DifferentiableWithinAt.inverse, IsBoundedLinearMap.differentiableWithinAt, DifferentiableWithinAt.of_insert, differentiableWithinAt_abs, LocallyBoundedVariationOn.ae_differentiableWithinAt, differentiableWithinAt_sub_const_iff, Complex.differentiableWithinAt_sqrt, Real.differentiableWithinAt_arccos_Ici, DifferentiableWithinAt.abs_of_pos, differentiableWithinAt_one, DifferentiableWithinAt.of_subsingleton, ContDiffWithinAt.differentiableWithinAt_iteratedDerivWithin, DifferentiableWithinAt.comp, mdifferentiableAt_iff, DifferentiableWithinAt.sum, DifferentiableWithinAt.congr, not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi, InformationTheory.not_differentiableWithinAt_klFun_Iio_zero, MDifferentiableWithinAt.differentiableWithinAt_writtenInExtChartAt, differentiableWithinAt_of_isInvertible_fderivWithin, DifferentiableWithinAt.dist, DifferentiableWithinAt.mul, AffineMap.differentiableWithinAt, HasGradientWithinAt.differentiableWithinAt, DifferentiableWithinAt.const_mul, differentiableWithinAt_pow, DifferentiableWithinAt.fun_pow, VectorField.DifferentiableWithinAt.pullbackWithin, DifferentiableWithinAt.prodMk, DifferentiableWithinAt.congr_mono, DifferentiableWithinAt.const_cpow, RightDerivMeasurableAux.differentiable_set_subset_D, DifferentiableWithinAt.continuousAlternatingMap_apply_const, DifferentiableAt.differentiableWithinAt, DifferentiableWithinAt.continuousAlternatingMapCompContinuousLinearMap, DifferentiableWithinAt.snd, DifferentiableWithinAt.congr_nhds, MDifferentiableAt.differentiableWithinAt_writtenInExtChartAt, differentiableWithinAt_of_derivWithin_ne_zero, Filter.EventuallyEq.differentiableWithinAt_iff_of_mem, DifferentiableWithinAt.fun_sum, DifferentiableWithinAt.abs, AnalyticWithinAt.differentiableWithinAt, DifferentiableWithinAt.arctan, mdifferentiableWithinAt_iff_image, DifferentiableWithinAt.fst, DifferentiableWithinAt.fun_mul, differentiableWithinAt_comp_sub, DifferentiableWithinAt.inversion, DifferentiableWithinAt.sin, mdifferentiableWithinAt_iff_differentiableWithinAt, DifferentiableWithinAt.congr_of_eventuallyEq, DifferentiableWithinAt.of_finite, ConvexOn.differentiableWithinAt_Ioi_of_mem_interior, DifferentiableWithinAt.restrictScalars, differentiableWithinAt_star_iff, measurableSet_of_differentiableWithinAt_Ici_of_isComplete, DifferentiableWithinAt.div_const, DifferentiableWithinAt.sub, HasDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.inv, Real.differentiableWithinAt_arcsin_Ici, DifferentiableWithinAt.fun_div, differentiableWithinAt_euclidean, differentiableWithinAt_inter, ContinuousLinearMap.differentiableWithinAt, LinearIsometryEquiv.comp_differentiableWithinAt_iff, DifferentiableWithinAt.csin, differentiableWithinAtProp_self_source, DifferentiableWithinAt.finset_prod, DifferentiableWithinAt.fun_neg, DifferentiableWithinAt.cpow_const, not_differentiableWithinAt_of_deriv_tendsto_atTop_Iio, differentiableWithinAt_iff_restrictScalars, differentiableWithinAt_of_fderivWithin_injective, HasFPowerSeriesWithinAt.differentiableWithinAt, differentiableWithinAt_abs_neg, differentiableWithinAt_dslope_of_ne, DifferentiableWithinAt.smul_const, DifferentiableWithinAt.neg, differentiableWithinAt_comp_add_right, DifferentiableWithinAt.abs_of_neg, DifferentiableWithinAt.cosh, DifferentiableWithinAt.csinh, differentiableWithinAt_const, mdifferentiableWithinAt_iff', Real.differentiableWithinAt_arcsin_Iic, DifferentiableWithinAt.clm_comp, differentiableWithinAt_pi, differentiableWithinAt_inter', DifferentiableWithinAt.mono, DifferentiableWithinAt.pow, differentiableWithinAt_congr_set', differentiableWithinAt_congr_set, DifferentiableWithinAt.sub_const, MDifferentiableWithinAt.differentiableWithinAt, differentiableWithinAt_id, DifferentiableWithinAtProp_self, DifferentiableWithinAt.const_smul, DifferentiableWithinAt.ccosh, mdifferentiableWithinAt_iff_target_inter', DifferentiableWithinAt.fun_sub, DifferentiableWithinAt.fun_smul, DifferentiableWithinAt.div, LipschitzOnWith.ae_differentiableWithinAt_real, differentiableWithinAt_insert_self, ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin, Real.differentiableWithinAt_arccos_Iic, mdifferentiableWithinAt_iff_of_mem_source', DifferentiableWithinAt.cpow, mdifferentiableWithinAt_iff, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.iterate, RightDerivMeasurableAux.differentiable_set_eq_D, DifferentiableWithinAt.rpow_const, measurableSet_of_differentiableWithinAt_Ioi, DifferentiableWithinAt.insert, DifferentiableWithinAt.arsinh, differentiableWithinAt_inverse, differentiableWithinAt_of_subsingleton, DifferentiableWithinAt.clog, MDifferentiableWithinAt.differentiableWithinAt_comp_extChartAt_symm, AnalyticAt.differentiableWithinAt, InformationTheory.not_differentiableWithinAt_klFun_Ioi_zero, DifferentiableWithinAt.norm_sq, differentiableWithinAt_id', mdifferentiableAt_iff_of_mem_source, differentiableWithinAt_ofNat, hasDerivWithinAt_derivWithin_iff, differentiableWithinAt_apply, DifferentiableWithinAt.continuousAlternatingMap_apply, differentiableWithinAt_insert, DifferentiableWithinAt.continuousMultilinear_apply_const, differentiableWithinAt_snd, DifferentiableWithinAt.fun_finset_prod, differentiableWithinAt_smul_iff, differentiableWithinAt_add_const_iff, not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio, DifferentiableWithinAt.zpow, DifferentiableWithinAt.clm_apply, DifferentiableAt.comp_differentiableWithinAt, not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero, Polynomial.differentiableWithinAt_aeval, differentiableWithinAt_const_sub_iff, DifferentiableWithinAt.cexp, DifferentiableWithinAt.insert', differentiableWithinAt_univ, differentiableWithinAt_comp_add_left, differentiableWithinAt_zpow, mdifferentiableWithinAt_iff_of_mem_source, differentiableWithinAt_piLp, ContinuousLinearEquiv.differentiableWithinAt, differentiableWithinAt_congr_set_nhdsNE, fderivWithin_def, DifferentiableWithinAt.fun_inv, differentiableWithinAt_complex_iff_differentiableWithinAt_real, ContDiffWithinAt.differentiableWithinAt', DifferentiableWithinAt.mul_const, DifferentiableWithinAt.mono_of_mem_nhdsWithin, DifferentiableWithinAt.empty, DifferentiableWithinAt.fun_add, DifferentiableWithinAt.sinh, DifferentiableWithinAt.exp, DifferentiableWithinAt.rpow, ContDiffWithinAt.differentiableWithinAt, LipschitzOnWith.ae_differentiableWithinAt, DifferentiableWithinAt.inner, measurableSet_of_differentiableWithinAt_Ici, differentiableWithinAt_intCast, ContinuousLinearEquiv.comp_differentiableWithinAt_iff, differentiableWithinAt_const_add_iff, DifferentiableWithinAt.const_add, fderivWithin_mem_iff, LinearIsometryEquiv.differentiableWithinAt, DifferentiableWithinAt.smul, differentiableWithinAt_fst, MonotoneOn.ae_differentiableWithinAt, DifferentiableWithinAt.ccos, DifferentiableWithinAt.of_dslope, DifferentiableWithinAt.comp', derivWithin_mem_iff, differentiableWithinAt_zero, differentiableWithinAtProp_self_target, DifferentiableWithinAt.congr_of_eventuallyEq_of_mem, differentiableWithinAt_Ioi_iff_Ici, DifferentiableWithinAt.star, DifferentiableWithinAt.continuousMultilinearMapCompContinuousLinearMap, differentiableWithinAt_finCons, IsBoundedBilinearMap.differentiableWithinAt, DifferentiableWithinAt.cos, DifferentiableWithinAt.add_const, differentiableWithinAt_congr_nhds, DifferentiableWithinAt.congr_of_eventuallyEq_insert, Filter.EventuallyEq.differentiableWithinAt_iff
|
HasFDerivAt π | MathDef | 243 mathmath: hasFDerivAt_iff_hasDerivAt, HasFDerivAt.const_add, 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_integral_of_dominated_loc_of_lip_interval, hasFDerivAt_stereoInvFunAux, HasFTaylorSeriesUpTo.hasFDerivAt, HasFDerivAt.fun_mul, HasDerivAt.comp_hasFDerivAt_of_eq, DifferentiableOn.hasFDerivAt, HasFDerivAt.of_isLittleO, HasFDerivAt.finset_prod, HasFDerivAt.norm_sq, ContinuousLinearEquiv.comp_hasFDerivAt_iff, ContinuousLinearMap.hasFDerivAt, HasFDerivAt.continuousMultilinear_apply_const, HasFDerivAt.of_notMem_tsupport, LipschitzWith.hasFDerivAt_of_hasLineDerivAt_of_closure, HasFDerivAt.sub, HasFDerivAt.star, HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, HasFDerivAt.multilinear_comp, IsContDiffImplicitAt.hasFDerivAt, HasFDerivAt.arctan, hasFDerivAt_snd, HasFDerivAt.fun_smul, intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip, HasFDerivAt.restrictScalars, HasFDerivAt.congr_fderiv, HasFDerivAt.fun_const_smul, hasFDerivAt_add_const_iff, HasFDerivAt.curveIntegral_segment_source, HasFDerivAt.add, hasFDerivAt_sub_const_iff, HasFDerivAt.sum, HasFDerivAt.congr_of_eventuallyEq, HasFDerivAt.clm_apply, Convex.exists_forall_hasFDerivAt_of_fderiv_symmetric, VectorFourier.hasFDerivAt_fourierIntegral, hasFDerivAt_ringInverse, contDiffAt_one_iff, HasFDerivAt.continuousAlternatingMap_apply, hasFDerivAt_finCons, HasFTaylorSeriesUpToOn.eventually_hasFDerivAt, hasFDerivAt_of_subsingleton, hasFDerivAt_jacobiThetaβ_term, HasDerivAt.hasFDerivAt, hasFDerivAt_norm_rpow, hasFDerivAt_iff_isLittleO, Real.hasFDerivAt_fourier, PiLp.hasFDerivAt_toLp, HasFDerivAt.pow, hasFDerivAt_id, hasFDerivAt_apply, HasFDerivAt.abs_of_pos, HasFDerivAt.abs, MeasureTheory.hasFDerivAt_convolution_right_with_param, hasFDerivAt_prodMk_left, HasCompactSupport.hasFDerivAt_convolution_right, hasFDerivAt_list_prod', hasFDerivAt_integral_of_dominated_loc_of_lip', HasDerivAt.complexToReal_fderiv', HasDerivAt.complexToReal_fderiv, hasFDerivAt_exp_smul_const', hasFDerivAt_finCons', HasFDerivAt.finCons, Complex.hasFDerivAt_cpow, HasFDerivAt.iterate, HasFDerivAt.cexp, HasFDerivAt.ccos, hasFTaylorSeriesUpTo_top_iff', hasFDerivAt_iff_tendsto, HasFDerivAt.clog, HasFDerivAt.of_local_left_inverse, 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, HasFDerivAt.ccosh, HasFDerivAt.abs_of_neg, ContinuousLinearEquiv.comp_right_hasFDerivAt_iff, HasFDerivAt.multiset_prod, hasFDerivAt_of_restrictScalars, HasFDerivAt.mul_const, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMap, hasFDerivAt_pi'', SchwartzMap.hasFDerivAt, HasFDerivWithinAt.hasFDerivAt_of_univ, Polynomial.hasFDerivAt_aeval, HasFDerivAt.continuousAlternatingMap_apply_const, hasFDerivAt_pow, HasFDerivAt.log, HasFDerivAt.sub_const, hasFDerivAt_single, HasFDerivAt.of_isLittleOTVS, HasFTaylorSeriesUpToOn.hasFDerivAt, HasFDerivAt.exp, HasStrictFDerivAt.hasFDerivAt, HasFDerivAt.fun_pow', hasDerivAt_iff_hasFDerivAt, HasFDerivAt.smul_const, hasFDerivAt_zero_of_eventually_const, contDiffAt_succ_iff_hasFDerivAt, hasFDerivAt_const, HasFDerivAt.inner, HasFDerivAt.const_mul, hasFDerivAt_of_tendstoLocallyUniformlyOn, hasFDerivAt_polarCoord_symm, HasFDerivAt.mul, Filter.EventuallyEq.hasFDerivAt_iff, hasFDerivAt_exp_zero, HasMFDerivAt.hasFDerivAt, HasFDerivAt.sinh, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMapBasis, HasFDerivAt.complexOfReal_hasFDerivAt, hasGradientAt_iff_hasFDerivAt, hasFDerivAt_exp_smul_const_of_mem_ball, HasFDerivAt.const_smul, LinearIsometryEquiv.hasFDerivAt, HasFDerivAt.rpow_const, HasFPowerSeriesAt.hasFDerivAt, hasFDerivAt_exp_smul_const, hasFDerivAt_jacobiThetaβ, HasDerivAt.hasFDerivAt_equiv, HasFDerivAt.snd, hasFDerivAt_update, HasFDerivAt.fun_sum, DifferentiableAt.hasFDerivAt, HasFDerivAt.add_const, ContinuousAffineMap.hasFDerivAt, hasFDerivAt_comp_sub, HasDerivWithinAt.comp_hasFDerivAt, intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le, HasFDerivAt.sin, HasFDerivAt.csin, ContinuousLinearEquiv.comp_hasFDerivAt_iff', ContinuousMultilinearMap.hasFDerivAt, spectrum.hasFDerivAt_resolvent, HasFDerivAt.hasFDerivAt_norm_smul, Real.hasFDerivAt_fourierIntegral, hasFDerivAt_iff_isLittleOTVS, HasFDerivAt.list_prod', HasFDerivAt.fun_neg, hasFDerivAt_pow', HasFDerivAt.fun_add, HasFDerivAt.fst, hasFDerivAt_of_tendstoUniformlyOnFilter, HasFPowerSeriesOnBall.hasFDerivAt, HasFDerivAt.prodMk, hasFDerivAt_sub_const, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, hasFDerivAt_natCast, hasFDerivAt_intCast, contDiff_one_iff_hasFDerivAt, HasFDerivWithinAt.comp_hasFDerivAt_of_eq, HasFDerivAt.cos, HasFDerivAt.linear_multilinear_comp, EuclideanGeometry.hasFDerivAt_inversion, PiLp.hasFDerivAt_ofLp, hasFDerivAt_tsum, HasFDerivAt.curveIntegral_segment_source', HasFDerivAt.const_rpow, NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm, HasFDerivAt.arsinh, HasFDerivAt.const_sub, hasFDerivAt_pi_polarCoord_symm, HasFDerivAt.pow', HasFDerivWithinAt.hasFDerivAt, ContinuousLinearMap.hasFDerivAt_of_bilinear, 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, HasFDerivAt.hasFDerivAt_norm_smul_neg, ContinuousLinearEquiv.hasFDerivAt, hasFDerivAt_integral_of_dominated_of_fderiv_le'', HasFDerivAt.comp_semilinear, hasFDerivAt_zero, HasFDerivAt.mul_const', HasFiniteFPowerSeriesOnBall.hasFDerivAt, Real.hasFDerivAt_fourierChar_neg_bilinear_right, hasFDerivAt_exp_smul_const_of_mem_ball', hasFDerivAt_of_tendstoUniformly, HasDerivAt.comp_hasFDerivAt, IsBoundedLinearMap.hasFDerivAt, HasFDerivAt.sqrt, HasFDerivAt.csinh, HasFDerivAt.hasFDerivAt_norm_smul_pos, hasFDerivAt_exp_zero_of_radius_pos, hasFDerivWithinAt_of_isOpen, HasFDerivAt.prodMap, HasFTaylorSeriesUpTo.fderiv, HasFDerivAt.cpow, intervalIntegral.integral_hasFDerivAt, ContinuousAlternatingMap.hasFDerivAt, ContinuousLinearEquiv.comp_right_hasFDerivAt_iff', hasFDerivAt_inv', HasFDerivAt.cosh, hasFDerivAt_of_tendstoUniformlyOn, VectorFourier.hasFDerivAt_fourierChar_smul, HasFDerivAt.neg, HasFDerivAt.star_star, hasFDerivAt_exp, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, hasFDerivAt_inv, HasFDerivWithinAt.comp_hasFDerivAt, HasFDerivAt.fun_mul', hasFDerivAt_fst, hasFDerivAt_pi', OpenPartialHomeomorph.hasFDerivAt_symm, hasFDerivAt_tsum_of_isPreconnected, HasFDerivAt.mul', hasFDerivWithinAt_univ, hasFDerivAt_list_prod_attach', HasDerivWithinAt.comp_hasFDerivAt_of_eq, HasFDerivAt.clm_comp, HasFDerivAt.rpow, hasFDerivAt_iff_isLittleO_nhds_zero, HasFDerivAt.smul, hasFDerivAt_exp_of_mem_ball, hasFDerivAt_stereoInvFunAux_comp_coe, contDiff_succ_iff_hasFDerivAt, HasCompactSupport.hasFDerivAt_convolution_left, hasFDerivAt_pi, Asymptotics.IsBigO.hasFDerivAt, HasFDerivAt.fun_sub, HasFDerivAt.const_cpow, hasFDerivAt_integral_of_dominated_loc_of_lip, HasFDerivAt.comp, hasFDerivAt_prodMk_right, HasFDerivAt.continuousMultilinearMap_apply, hasFDerivAt_finset_prod
|
HasFDerivAtFilter π | CompData | 54 mathmath: hasFDerivAtFilter_pi, HasDerivAtFilter.comp_hasFDerivAtFilter, HasFDerivAtFilter.fun_sum, HasFDerivAtFilter.sub, HasFDerivAtFilter.const_add, HasFDerivAtFilter.const_sub, HasFDerivAtFilter.neg, hasFDerivAtFilter_sub_const_iff, hasFDerivAtFilter_ofNat, hasFDerivAtFilter_zero, HasFDerivAt.hasFDerivAtFilter, hasFDerivAtFilter_const, hasFDerivAtFilter_iff_isLittleO, HasFDerivAtFilter.mono, HasFDerivAtFilter.sum, ContinuousLinearMap.hasFDerivAtFilter, hasFDerivAtFilter_iff_hasDerivAtFilter, HasFDerivAtFilter.congr_of_eventuallyEq, HasFDerivAtFilter.const_smul, HasFDerivAtFilter.fun_const_smul, HasFDerivAtFilter.fun_sub, hasFDerivAtFilter_snd, HasFDerivAtFilter.prodMk, HasFDerivAtFilter.fun_add, HasFDerivAtFilter.comp, hasFDerivAtFilter_fst, HasFDerivAtFilter.star, IsBoundedLinearMap.hasFDerivAtFilter, hasFDerivAtFilter_iff_isLittleOTVS, HasFDerivAtFilter.fst, HasFDerivAtFilter.add, ContinuousAffineMap.hasFDerivAtFilter, hasFDerivAtFilter_finCons, HasFDerivAtFilter.snd, HasFDerivAtFilter.fun_neg, HasDerivAtFilter.comp_hasFDerivAtFilter_of_eq, Filter.EventuallyEq.hasFDerivAtFilter_iff, hasFDerivAtFilter_id, hasDerivAtFilter_iff_hasFDerivAtFilter, hasFDerivAtFilter_iff_tendsto, HasFDerivAtFilter.of_isLittleO, HasDerivAtFilter.hasFDerivAtFilter, HasFDerivAtFilter.iterate, hasFDerivAtFilter_finCons', hasFDerivAtFilter_natCast, hasFDerivAtFilter_const_add_iff, HasFDerivAtFilter.finCons, HasFDerivAtFilter.restrictScalars, hasFDerivAtFilter_add_const_iff, hasFDerivAtFilter_pi', HasFDerivAtFilter.add_const, hasFDerivAtFilter_intCast, hasFDerivAtFilter_one, HasFDerivAtFilter.sub_const
|
HasFDerivWithinAt π | MathDef | 203 mathmath: hasFDerivWithinAt_pi'', HasFDerivWithinAt.congr_of_eventuallyEq, HasFDerivWithinAt.ccosh, HasFDerivWithinAt.continuousMultilinearMap_apply, HasFDerivWithinAt.ccos, Filter.EventuallyEq.hasFDerivWithinAt_iff, HasFDerivWithinAt.pow, hasFDerivWithinAt_const, HasFDerivWithinAt.add, hasFTaylorSeriesUpToOn_top_iff_right, HasFDerivWithinAt.of_subsingleton, HasDerivWithinAt.complexToReal_fderiv', HasFDerivWithinAt.of_local_left_inverse, HasFDerivWithinAt.clm_apply, HasFDerivWithinAt.of_finite, HasFDerivWithinAt.prodMap, HasFDerivWithinAt.complexOfReal, HasFDerivWithinAt.empty, HasFDerivWithinAt.linear_multilinear_comp, hasFDerivWithinAt_comp_smul_iff_smul, HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, HasFDerivWithinAt.comp_of_tendsto, HasFDerivWithinAt.fst, hasFDerivWithinAt_sub_const_iff, hasFDerivWithinAt_inv, HasFDerivWithinAt.csin, HasFDerivWithinAt.continuousAlternatingMap_apply, HasFDerivWithinAt.const_mul, HasDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.fun_const_smul, HasFDerivWithinAt.mul, ContinuousLinearMap.hasFDerivWithinAt_of_bilinear, hasFDerivWithinAt_pi', HasFDerivWithinAt.multiset_prod, HasFDerivAt.hasFDerivWithinAt, HasDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.exp, hasFDerivWithinAt_intCast, hasFDerivWithinAt_inter', HasFDerivWithinAt.const_sub, ContDiffWithinAt.hasFDerivWithinAt_nhds, HasFDerivWithinAt.of_notMem_tsupport, hasFDerivWithinAt_finCons, HasFDerivWithinAt.star, HasFDerivWithinAt.const_smul, hasGradientWithinAt_iff_hasFDerivWithinAt, HasFDerivAt.comp_hasFDerivWithinAt, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff', HasFTaylorSeriesUpToOn.hasFDerivWithinAt, HasFDerivWithinAt.abs_of_neg, HasFDerivWithinAt.fun_smul, HasFDerivWithinAt.neg, HasFDerivWithinAt.congr_fderiv, hasDerivWithinAt_iff_hasFDerivWithinAt, HasFDerivWithinAt.cpow, HasFDerivWithinAt.csinh, HasFDerivWithinAt.abs, HasFDerivWithinAt.mul_const, hasFDerivWithinAt_iff_isLittleO, HasFDerivWithinAt.mono_of_mem_nhdsWithin, HasFDerivWithinAt.inner, hasFDerivWithinAt_finCons', hasFTaylorSeriesUpToOn_top_iff', HasDerivWithinAt.complexToReal_fderiv, HasFDerivWithinAt.singleton, HasFDerivWithinAt.fun_sub, HasFDerivWithinAt.prodMk, HasFDerivWithinAt.of_isLittleO, hasFDerivWithinAt_const_add_iff, HasFDerivWithinAt.cexp, hasFDerivWithinAt_iff_hasDerivWithinAt, hasFTaylorSeriesUpToOn_succ_iff_right, HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, HasFDerivWithinAt.fun_neg, hasFDerivWithinAt_pow', HasMFDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.log, hasFDerivWithinAt_one, HasFDerivWithinAt.insert, hasFDerivWithinAt_of_mem_nhds, hasFDerivWithinAt_zero, HasFDerivWithinAt.norm_sq, hasFDerivWithinAt_piLp, HasFDerivWithinAt.smul_const, hasFDerivWithinAt_singleton, IsBoundedBilinearMap.hasFDerivWithinAt, hasFTaylorSeriesUpToOn_succ_nat_iff_right, HasFDerivWithinAt.finCons, hasFDerivWithinAt_comp_smul_smul_iff, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contDiffOn_succ_iff_hasFDerivWithinAt, HasFDerivWithinAt.const_add, HasFDerivWithinAt.mul_const', HasDerivAt.comp_hasFDerivWithinAt_of_eq, ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff', hasFDerivWithinAt_tangentCoordChange, HasFDerivWithinAt.of_notMem_closure, HasFTaylorSeriesUpToOn.fderivWithin, ContinuousLinearEquiv.hasFDerivWithinAt, ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff, HasFDerivWithinAt.sinh, HasFDerivWithinAt.iterate, HasFDerivWithinAt.restrictScalars, hasFDerivWithinAt_closure_of_tendsto_fderiv, ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff, ContinuousLinearMap.hasFDerivWithinAt, HasFDerivWithinAt.multilinear_comp, HasFDerivWithinAt.rpow_const, Asymptotics.IsBigO.hasFDerivWithinAt, ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff', HasFDerivWithinAt.snd, HasFDerivWithinAt.clog, HasFDerivWithinAt.insert', HasFDerivWithinAt.comp, hasFDerivWithinAt_euclidean, HasFDerivWithinAt.abs_of_pos, HasFDerivWithinAt.clm_comp, HasFDerivWithinAt.arsinh, HasDerivWithinAt.comp_hasFDerivWithinAt, Convex.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric, HasFDerivWithinAt.continuousMultilinear_apply_const, HasFDerivWithinAt.add_const, HasFDerivWithinAt.sub, hasFDerivWithinAt_natCast, Filter.EventuallyEq.hasFDerivWithinAt_iff_of_mem, HasFDerivWithinAt.curveIntegral_segment_source, HasFDerivWithinAt.sqrt, hasFDerivWithinAt_insert_self, HasFDerivWithinAt.pow', hasFDerivWithinAt_diff_singleton, HasFDerivWithinAt.const_cpow, hasFDerivWithinAt_comp_add_right, intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae, HasFDerivWithinAt.arctan, HasFDerivWithinAt.rpow, HasFDerivWithinAt.union, hasFDerivWithinAt_fst, intervalIntegral.integral_hasFDerivWithinAt, HasFDerivWithinAt.congr_mono, HasFDerivWithinAt.fun_sum, hasFTaylorSeriesUpToOn_succ_iff_left, hasFDerivWithinAt_ofNat, hasFDerivWithinAt_congr_set', hasFDerivWithinAt_iff_hasGradientWithinAt, HasFDerivWithinAt.smul, hasFDerivWithinAt_congr_set_nhdsNE, Convex.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric, hasFDerivWithinAt_pi, ContinuousAlternatingMap.hasFDerivWithinAt, Polynomial.hasFDerivWithinAt_aeval, HasFDerivWithinAt.fun_mul', contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, LinearIsometryEquiv.hasFDerivWithinAt, HasFDerivWithinAt.fun_pow', HasFDerivWithinAt.fun_add, ContinuousAffineMap.hasFDerivWithinAt, hasFDerivWithinAt_add_const_iff, HasFDerivWithinAt.of_not_accPt, HasFDerivWithinAt.mono, HasFDerivWithinAt.const_rpow, hasFDerivWithinAt_comp_sub, hasFDerivWithinAt_congr_set, HasFDerivWithinAt.congr', hasFDerivWithinAt_diff_singleton_self, HasFDerivWithinAt.congr, HasFDerivWithinAt.of_insert, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff, IsBoundedLinearMap.hasFDerivWithinAt, HasFDerivWithinAt.curveIntegral_segment_source', HasFDerivWithinAt.finset_prod, Convex.hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric, hasFDerivWithinAt_inter, hasFDerivWithinAt_of_isOpen, hasFDerivWithinAt_insert, fderivWithin_def, hasFDerivWithinAt_pow, hasFDerivWithinAt_iff_isLittleOTVS, HasFDerivWithinAt.mul', Polynomial.hasFDerivWithinAt, HasDerivWithinAt.comp_hasFDerivWithinAt_of_eq, hasFDerivWithinAt_of_subsingleton, hasFDerivWithinAt_iff_tendsto, HasFDerivWithinAt.cos, HasFPowerSeriesWithinAt.hasFDerivWithinAt, HasGradientWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.of_restrictScalars, HasFDerivWithinAt.sub_const, hasFDerivWithinAt_univ, HasFPowerSeriesWithinOnBall.hasFDerivWithinAt, hasMFDerivWithinAt_iff_hasFDerivWithinAt, DifferentiableWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.sin, HasFDerivWithinAt.continuousAlternatingMap_apply_const, HasFDerivWithinAt.of_isLittleOTVS, hasFDerivWithinAt_comp_add_left, HasFDerivWithinAt.sum, hasFDerivWithinAt_snd, HasFDerivWithinAt.fun_mul, contDiffWithinAt_succ_iff_hasFDerivWithinAt, hasFDerivWithinAt_apply, HasFDerivWithinAt.cosh, HasFDerivWithinAt.list_prod', hasFDerivWithinAt_id
|
HasStrictFDerivAt π | MathDef | 179 mathmath: HasStrictFDerivAt.log, hasStrictFDerivAt_const_add_iff, hasStrictFDerivAt_apply, LinearIsometryEquiv.hasStrictFDerivAt, HasStrictFDerivAt.fun_mul', HasStrictFDerivAt.abs_of_pos, hasStrictFDerivAt_exp_of_mem_ball, hasStrictFDerivAt_list_prod_finRange', HasStrictFDerivAt.csin, ContinuousAlternatingMap.hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff, hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt, ContDiff.hasStrictFDerivAt, OpenPartialHomeomorph.hasStrictFDerivAt_symm, ImplicitFunctionData.hasStrictFDerivAt_leftFun, ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap, ImplicitFunctionData.implicitFunction_hasStrictFDerivAt, HasStrictFDerivAt.add_const, HasStrictFDerivAt.finCons, hasStrictFDerivAt_snd, hasStrictFDerivAt_iff_isLittleOTVS, HasStrictFDerivAt.mul', Complex.hasStrictFDerivAt_exp_real, hasStrictFDerivAt_exp_smul_const_of_mem_ball', HasStrictFDerivAt.pow, HasStrictFDerivAt.const_mul, HasStrictFDerivAt.fun_sum, Real.hasStrictFDerivAt_rpow_of_pos, HasStrictFDerivAt.star, hasStrictFDerivAt_pi', HasStrictFDerivAt.const_smul, hasStrictFDerivAt_natCast, HasStrictFDerivAt.abs, ContinuousLinearMap.hasStrictFDerivAt_of_bilinear, HasStrictFDerivAt.arsinh, HasStrictFDerivAt.list_prod', Complex.hasStrictFDerivAt_cpow', HasStrictFDerivAt.hasStrictDerivAt_norm_smul_neg, hasStrictFDerivAt_multiset_prod, HasStrictFDerivAt.fst, HasStrictFDerivAt.to_implicitFunctionOfComplemented, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, HasStrictFDerivAt.congr_of_eventuallyEq, hasStrictFDerivAt_exp, hasStrictFDerivAt_iff_isLittleO, HasStrictFDerivAt.prodMk, HasStrictFDerivAt.of_notMem_tsupport, hasStrictFDerivAt_exp_smul_const', Complex.hasStrictFDerivAt_cpow, HasStrictFDerivAt.of_local_left_inverse, HasStrictFDerivAt.const_cpow, HasStrictFDerivAt.cexp, HasStrictFDerivAt.abs_of_neg, ImplicitFunctionData.hasStrictFDerivAt_implicitFunction_fderiv, ContDiffAt.hasStrictFDerivAt', HasStrictFDerivAt.clog, HasStrictFDerivAt.sqrt, HasStrictFDerivAt.rpow, hasStrictFDerivAt_finCons, HasStrictFDerivAt.ccos, HasStrictFDerivAt.hasStrictFDerivAt_implicitFunctionOfProdDomain, ContinuousAlternatingMap.hasStrictFDerivAt, ContinuousAffineMap.hasStrictFDerivAt, hasStrictFDerivAt_iff_hasStrictDerivAt, intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae, hasStrictFDerivAt_piLp, intervalIntegral.integral_hasStrictFDerivAt, HasStrictFDerivAt.neg, ContinuousMultilinearMap.hasStrictFDerivAt, Filter.EventuallyEq.hasStrictFDerivAt_iff, HasStrictFDerivAt.add, HasStrictFDerivAt.restrictScalars, HasStrictFDerivAt.arctan, HasStrictDerivAt.hasStrictFDerivAt, HasStrictFDerivAt.to_implicitFunction, hasStrictFDerivAt_zero, ContDiffAt.hasStrictFDerivAt, HasStrictFDerivAt.iterate, HasStrictFDerivAt.continuousMultilinear_apply_const, hasStrictFDerivAt_norm_sq, HasStrictFDerivAt.const_sub, ImplicitFunctionData.hasStrictFDerivAt, hasStrictFDerivAt_inv, HasStrictFDerivAt.fun_sub, HasStrictFDerivAt.continuousAlternatingMap_apply, HasStrictDerivAt.complexToReal_fderiv', hasStrictFDerivAt_pow', ContDiffAt.hasStrictFDerivAt_implicitFunction, hasStrictFDerivAt_finCons', ContinuousLinearMap.hasStrictFDerivAt, HasStrictFDerivAt.const_rpow, hasStrictFDerivAt_list_prod_attach', HasStrictFDerivAt.cos, hasStrictFDerivAt_ringInverse, HasStrictFDerivAt.hasStrictDerivAt_norm_smul_pos, HasStrictDerivAt.comp_hasStrictFDerivAt, 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, HasStrictDerivAt.comp_hasStrictFDerivAt_of_eq, HasStrictFDerivAt.fun_neg, HasStrictFDerivAt.sum, HasStrictFDerivAt.to_localInverse, hasStrictFDerivAt_one, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, HasStrictFDerivAt.fun_const_smul, HasStrictFDerivAt.prodMap, hasStrictFDerivAt_sub_const_iff, ImplicitFunctionData.hasStrictFDerivAt_implicitFunction, HasStrictFDerivAt.clm_apply, HasStrictFDerivAt.fun_smul, hasStrictFDerivAt_ofNat, HasStrictFDerivAt.cpow, HasStrictFDerivAt.pow', HasStrictFDerivAt.multiset_prod, HasStrictFDerivAt.of_isLittleO, HasStrictFDerivAt.mul_const', hasStrictFDerivAt_list_prod, HasStrictFDerivAt.to_local_left_inverse, HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt, HasStrictFDerivAt.continuousAlternatingMap_apply_const, hasStrictFDerivAt_add_const_iff, HasStrictFDerivAt.fun_pow', HasStrictFDerivAt.comp, HasStrictFDerivAt.sin, HasStrictFDerivAt.congr_fderiv, HasStrictFDerivAt.hasStrictFDerivAt_norm_smul, hasStrictFDerivAt_inv', hasStrictFDerivAt_exp_smul_const, Complex.hasStrictFDerivAt_log_real, HasStrictFDerivAt.mul, HasStrictFDerivAt.fun_add, hasStrictFDerivAt_const, hasStrictFDerivAt_list_prod', HasStrictFDerivAt.smul_const, HasStrictFDerivAt.ccosh, HasStrictFDerivAt.cosh, hasStrictFDerivAt_pow, PiLp.hasStrictFDerivAt_ofLp, HasStrictFDerivAt.fun_mul, hasStrictFDerivAt_pi'', HasStrictFDerivAt.sinh, Real.hasStrictFDerivAt_rpow_of_neg, hasStrictDerivAt_iff_hasStrictFDerivAt, HasStrictDerivAt.complexToReal_fderiv, HasFPowerSeriesAt.hasStrictFDerivAt, HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap, HasStrictFDerivAt.inner, HasStrictDerivAt.hasStrictFDerivAt_equiv, HasStrictFDerivAt.const_add, HasStrictFDerivAt.sub, HasStrictFDerivAt.csinh, hasStrictFDerivAt_intCast, ImplicitFunctionData.hasStrictFDerivAt_rightFun, HasStrictFDerivAt.clm_comp, HasStrictFDerivAt.sub_const, HasStrictFDerivAt.continuousMultilinearMap_apply, HasStrictFDerivAt.mul_const, AnalyticAt.hasStrictFDerivAt, ContinuousMultilinearMap.hasStrictFDerivAt_uncurry, UpperHalfPlane.hasStrictFDerivAt_smul, hasStrictFDerivAt_pi, HasStrictFDerivAt.exp, hasStrictFDerivAt_id, hasStrictFDerivAt_sub_const, LinearIsometryEquiv.comp_hasStrictFDerivAt_iff, HasStrictFDerivAt.smul, HasStrictFDerivAt.finset_prod, ContinuousLinearEquiv.comp_hasStrictFDerivAt_iff, HasStrictFDerivAt.rpow_const, hasStrictFDerivAt_exp_smul_const_of_mem_ball, HasStrictFDerivAt.snd, PiLp.hasStrictFDerivAt_toLp, hasStrictFDerivAt_euclidean
|
fderiv π | CompOp | 288 mathmath: Polynomial.fderiv, fderiv_iteratedFDeriv, DifferentiableAt.fderivWithin, fderiv_snd, LinearIsometryEquiv.comp_fderiv, extDeriv_constOfIsEmpty, Real.fderiv_fourierIntegral, ContDiff.fderiv_succ, fderiv_intCast, ContDiffAt.implicitFunction_def, 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, integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable, 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, TestFunction.fderivCLM_apply_of_le, HasFTaylorSeriesUpTo.fderiv_eq, 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, VectorField.fderiv_pullback, ContDiff.continuous_fderiv, HarmonicAt.differentiableAt_complex_partial, integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable, 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, Real.fourier_fderiv, 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, complexOfReal_deriv, fderiv_const_mul, fderiv_sub_const, fderiv_exp, fderiv_arctan, fderiv_tsum, 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, ContDiffAt.hasStrictFDerivAt_implicitFunction, 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, Real.fourierIntegral_fderiv, 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, ContDiffMapSupportedIn.fderivLM_apply, 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, norm_sub_le_mul_volume_of_norm_fderiv_le, Complex.norm_fderiv_le_one_of_mapsTo_ball, ContDiffMapSupportedIn.fderivCLM_apply_of_le, ContDiff.contDiff_fderiv_apply, differentiableAt_iff_restrictScalars, extDeriv_pullback, complexOfReal_fderiv, HasFiniteFPowerSeriesOnBall.fderiv', measurable_fderiv, ContDiffMapSupportedIn.fderivCLM_apply, TestFunction.fderivCLM_apply, complexOfReal_hasDerivAt, iteratedFDeriv_two_apply, fderiv_fst, ContDiffMapSupportedIn.fderivLM_apply_of_le, fderiv_norm_smul_pos, fderiv_mul_const, fderiv_csinh, iteratedFDeriv_succ_eq_comp_left, fderiv_of_notMem_tsupport, IsContDiffImplicitAt.implicitFunction_def, mfderiv_eq_fderiv, fderiv_comp_add_left, IsLocalMin.fderiv_eq_zero, fderiv_comp_sub, Complex.integral_boundary_rect_of_differentiableOn_real, 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, integral_bilinear_fderiv_right_eq_neg_left_of_integrable, exists_continuousLinearEquiv_fderiv_symm_eq, 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, VectorFourier.fourierIntegral_fderiv, fderiv_continuousLinearEquiv_comp', Real.fderiv_fourierChar_neg_bilinear_left_apply, AnalyticAt.hasStrictFDerivAt, inner_gradient_right, fderiv_single, DifferentiableAt.lineDeriv_eq_fderiv, fderiv_tsum_apply, 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 | 216 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, complexOfReal_hasDerivWithinAt, fderivWithin_fderivWithin_eq_of_mem_nhdsWithin, fderivWithin_extChartAt_comp_extChartAt_symm_range, 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, ModelWithCorners.isInvertible_fderivWithin_extendCoordChange, fderivWithin_star, fderivWithin_fun_neg, extDerivWithin_constOfIsEmpty, fderivWithin_sin, fderivWithin_congr', fderivWithin_finset_prod, fderivWithin_eq_fderiv, fderivWithin_eventually_congr_set', VectorField.fderivWithin_pullbackWithin, 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, complexOfReal_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, VectorField.mpullback_mfderivWithin_apply_smul, 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, exists_continuousLinearEquiv_fderivWithin_symm_eq, fderivWithin_congr_set, complexOfReal_derivWithin, 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'
|