← all areas

Namespace Complex 64 theorems

• Residue theorem on a circle for simple poles Complex.circleIntegral_eq_sum_residue_of_simplePole 0 below · cited by 5 · depth 14
• A complete DVR with finite residue field embeds into ℂ Complex.exists_ringHom_comp_eq_subtype_of_isDiscreteValuationRing_of_finite_residueField 0 below · cited by 3 · depth 14
• Holomorphic dependence on t of oint G Φ'/(Φ-t) Complex.hasDerivAt_circleIntegral_mul_deriv_div_sub 0 below · cited by 4 · depth 14
• Stokes' theorem for Φ dz on the modular fundamental domain Complex.integral_modularFundamentalDomain_eq_boundary_of_hasFDerivAt 0 below · cited by 6 · depth 14
• Primitives of holomorphic functions on star-shaped domains Complex.exists_hasDerivAt_of_starConvex 0 below · cited by 3 · depth 15
• Boundedness of a continuous logarithm near a non-zero boundary limit Complex.exists_norm_le_of_continuousOn_of_exp_eq_of_tendsto 0 below · cited by 2 · depth 16
• Reduction of ℤ̄ to K sending e^{2π i/M} to ζ Complex.exists_ringHom_integralClosure_int_apply_eq_of_isPrimitiveRoot 0 below · cited by 5 · depth 16
• Cauchy–Pompeiu formula for simple poles Complex.integral_mul_dbar_eq_neg_pi_mul_finsum_residue 2 below · cited by 2 · depth 16
• Functions with at most simple poles are locally integrable Complex.locallyIntegrableOn_of_simplePoles 0 below · cited by 1 · depth 16
• Product rule for the principal square root across a quarter-turn Complex.sqrt_mul_sqrt_eq_of_re_pos 0 below · cited by 1 · depth 16
• Weighted argument principle on a disc Complex.circleIntegral_mul_deriv_div_sub_eq_sum_analyticOrderNatAt 1 below · cited by 2 · depth 17
• Holomorphy of integrals with compactly supported continuous integrand Complex.differentiableOn_integral_of_continuousOn_of_forall_differentiableOn 0 below · cited by 15 · depth 17
• Entire continuation glued from local quotients Z/(cE) Complex.exists_differentiable_eqOn_halfPlane_of_forall_exists_entire_mul_eq 0 below · cited by 1 · depth 17
• One-pole Cauchy–Pompeiu formula for C¹ test functions Complex.integral_inv_sub_mul_dbar_eq_neg_pi_mul 1 below · cited by 2 · depth 17
• Holomorphic functions are weak solutions of partial̄ Complex.integral_mul_dbar_eq_zero_of_differentiableOn 0 below · cited by 4 · depth 17
• Branch rule for log on the right half-plane Complex.log_add_log_eq_log_sub_of_re_pos 0 below · cited by 1 · depth 17
• Circle integral of Ψ/(R-t) over simple solutions of R=t Complex.circleIntegral_div_sub_eq_sum_div_deriv 1 below · cited by 1 · depth 19
• Residue theorem for a radially parametrised star-shaped loop Complex.integral_radial_loop_eq_two_pi_I_mul_sum_residue 1 below · cited by 2 · depth 19
• Two-sided exponential bounds for Γ on vertical strips Complex.exists_forall_norm_Gamma_le_mul_exp_and_exp_le_mul_norm_Gamma_of_re_mem_Icc_of_one_le_abs_im 0 below · cited by 12 · depth 20
• Stokes form of the argument principle for E F'/F Complex.integral_mul_logDeriv_mul_dbar_eq_neg_pi_mul_finsum 3 below · cited by 2 · depth 20
• Green–Pompeiu formula on a radially parametrised region Complex.integral_radial_loop_eq_two_mul_I_mul_setIntegral 0 below · cited by 1 · depth 20
• Trivialising ζ ↦ b + ζ^e away from a ray Complex.exists_trivialization_add_pow 0 below · cited by 1 · depth 21
• Argument principle in Stokes form for algebraic local models Complex.integral_logDeriv_wedge_add_finsum_eq_integral_dbarLogDeriv 2 below · cited by 3 · depth 21
• Countability of the zeros in a right half-plane Complex.countable_setOf_re_gt_and_eq_zero_of_differentiableOn_of_exists_ne_zero 0 below · cited by 1 · depth 22
• Simultaneous non-vanishing far right in a half-plane Complex.exists_forall_ne_zero_re_gt_of_differentiableOn_of_exists_ne_zero 0 below · cited by 1 · depth 22
• Laurent identity in q^{-s} and cancellation of the denominator Complex.forall_cpow_mul_eval_mul_eval_eq_and_exists_finset_forall_eq_mul_of_infinite 0 below · cited by 4 · depth 22
• Partial fraction expansion of π²/sin²(π z) Complex.tsum_int_one_div_add_sq_eq_pi_sq_div_sin_sq 0 below · cited by 1 · depth 22
• Rotation-invariant holomorphic functions on a disc factor through z^e Complex.exists_analyticOnNhd_comp_pow_of_forall_mul_eq 0 below · cited by 1 · depth 23
• Pigeonhole over abscissae for a finite family in ℂ Complex.exists_forall_not_countable_setOf_re_gt_mem_of_finite 0 below · cited by 1 · depth 23
• Finite δ-net of a complex rectangle with short δ-chains Complex.exists_grid_reProdIm 0 below · cited by 1 · depth 23
• Lipschitz divided minors of a holomorphic map Complex.exists_lipschitzWith_divided_minor 0 below · cited by 1 · depth 23
• Minor lower bound near an immersed point of a holomorphic curve Complex.exists_mul_norm_sub_le_iSup_norm_minor_of_wedge_deriv_ne_zero 0 below · cited by 1 · depth 23
• Rare vanishing of a random linear form along a small arc Complex.volume_ball_inter_exists_sum_mul_eq_zero_le 1 below · cited by 2 · depth 23
• Crofton-type bound for random hyperplanes meeting c(S) Complex.volume_ball_inter_exists_sum_mul_eq_zero_le_mul_volume 3 below · cited by 2 · depth 23
• Small-value bound for a linear form on the unit polydisc Complex.volume_ball_inter_norm_sum_mul_le 0 below · cited by 3 · depth 23
• Uniqueness of Laurent coefficients on an annulus Complex.eq_zero_of_summable_norm_mul_zpow_of_forall_tsum_mul_zpow_eq_zero 0 below · cited by 6 · depth 24
• Uniform lower bound for int_Blog|a·φ| over unit covectors Complex.exists_le_setIntegral_ball_log_norm_sum_mul 7 below · cited by 1 · depth 24
• Analytic continuation of a Dirichlet-polynomial identity to a half-plane Complex.forall_mul_polynomial_eval_cpow_eq_of_differentiableOn_of_forall_lt_re 0 below · cited by 2 · depth 24
• Integrability on a disc via polar coordinates Complex.integrableOn_ball_iff_integrableOn_smul_circleMap 0 below · cited by 2 · depth 24
• Polar coordinates on a disc, iterated form Complex.integral_ball_eq_integral_smul_intervalIntegral_circleMap 2 below · cited by 1 · depth 24
• Mellin transform of t^ke^{-rt} equals r^{-(s+k)}Γ(s+k) Complex.mellinConvergent_cpow_mul_exp_neg_mul_and_mellin_eq 0 below · cited by 2 · depth 24
• Polar coordinates on a disc Complex.integral_ball_eq_integral_smul_circleMap 0 below · cited by 1 · depth 25
• Two-term contiguity relation for balanced double Euler integrals Complex.mul_integral_Ioi_integral_Ioi_cpow_add_mul_integral_Ioi_integral_Ioi_cpow_eq_of_balance 2 below · cited by 1 · depth 25
• Half-line Euler beta integral equals Γ(a)Γ(b)/Γ(a+b) Complex.integrableOn_and_integral_Ioi_cpow_mul_one_add_cpow_neg_eq_Gamma_mul_Gamma_div 0 below · cited by 5 · depth 26
• Balanced double Euler integral in closed Gamma form Complex.integral_Ioi_integral_Ioi_cpow_mul_one_add_cpow_neg_mul_one_add_add_cpow_neg_of_balance 1 below · cited by 2 · depth 26
• Holomorphy of L²-pairings of a holomorphic family Complex.differentiableOn_integral_mul_of_memLp_two_of_tendsto_eLpNorm_of_forall_differentiableOn 0 below · cited by 2 · depth 28
• Logarithmic growth of ψ and archimedean Γ-factors on a half-plane Complex.exists_forall_norm_digamma_le_mul_log_norm_and_norm_logDeriv_GammaReal_le_and_norm_logDeriv_GammaComplex_le_of_le_re 3 below · cited by 1 · depth 28
• Osgood's lemma: holomorphic maps on ℂⁿ are C¹ Complex.contDiffOn_one_of_differentiableOn_pi 0 below · cited by 5 · depth 29
• Logarithmic growth of ψ and archimedean Γ-factors in a strip Complex.exists_forall_norm_digamma_le_mul_log_and_norm_logDeriv_GammaReal_le_and_norm_logDeriv_GammaComplex_le_of_le_re 2 below · cited by 1 · depth 29
• Dirichlet double integral Γ(α+β-γ)Γ(α)Γ(β)/Γ(α+β) Complex.integrable_and_integral_prod_Ioi_exp_neg_add_mul_cpow_mul_cpow_mul_add_cpow_neg 0 below · cited by 1 · depth 29
• Injective holomorphic map on a disc: open image, holomorphic inverse Complex.isOpen_image_and_exists_differentiableOn_leftInverse_of_injOn_ball 0 below · cited by 2 · depth 29
• Landau's lemma on F'/F on a zero-free disc Complex.norm_deriv_le_mul_norm_and_exp_neg_le_norm_of_forall_ne_zero_of_norm_le_exp 0 below · cited by 1 · depth 29
• De la Vallée Poussin–Landau zero-free region deduction Complex.div_le_one_sub_of_apply_eq_zero_of_norm_le_exp_of_three_four_one_nonneg 1 below · cited by 2 · depth 30
• Holomorphic implicit function theorem for a bivariate polynomial Complex.exists_differentiableOn_forall_evalEval_eq_zero_iff_eq_of_evalEval_derivative_ne_zero 0 below · cited by 1 · depth 30
• Logarithmic growth of digamma in a vertical strip Complex.exists_forall_norm_digamma_le_mul_log_of_le_re 1 below · cited by 1 · depth 30
• Complex differentiability on open U⊆ℂⁿ implies C^∞ Complex.contDiffOn_infty_of_differentiableOn_pi 1 below · cited by 3 · depth 31
• Gauss partial-fraction series for ψ on Re s>0 Complex.hasSum_one_div_add_one_sub_one_div_add_eq_digamma_add_eulerMascheroniConstant 0 below · cited by 1 · depth 31
• Landau's lemma on the logarithmic derivative Complex.neg_re_deriv_div_le_sub_sum_re_inv_sub_of_norm_le_exp_of_ne_zero_of_lt_re 0 below · cited by 1 · depth 31
• Holomorphic implicit function for a polynomial in one dependent variable Complex.exists_differentiableOn_forall_eval_map_eval_eq_zero_iff_eq_of_derivative_ne_zero_pi 0 below · cited by 1 · depth 32
• Fourth-order Lipschitz formula sum_{n∈ℤ}(x+n)⁻⁴ Complex.tsum_one_div_add_int_pow_four 0 below · cited by 2 · depth 34
• Lipschitz formula of order three on the real line Complex.tsum_one_div_add_int_pow_three 0 below · cited by 3 · depth 34
• Inversion identities for ‖1-exp(X/2+2π iTheta)⁻¹‖ Complex.norm_one_sub_inv_exp_and_sq_mul_log_eq_and_contDiff 0 below · cited by 1 · depth 35
• Local normal form of the germ |1-e^z|²log|1-e^z| Complex.exists_contDiffOn_norm_one_sub_exp_sq_mul_log_eq_mul_add 0 below · cited by 1 · depth 37
• The quadratic form |̄ z+̄ r z|² and its two completions of the square Complex.normSq_conj_add_conj_mul_eq_and_complete_square 0 below · cited by 1 · depth 39