Boundary value of on the gap
ProvedWeightedRootIntegralIdentity.weighted_root_complex_boundary_jumpanalysiscomplex-analysisgeometric-meanintegral-identity
Let , let be real numbers, and let be real weights with . For a complex number and a real exponent , let denote the principal power , whose branch cut is the negative real axis and which assigns argument to a negative real base.
Fix an index with and a real point strictly inside the gap, . Then
In other words, the principal branch of , evaluated on the real segment , is the upper boundary value of the analytic continuation from the upper half plane: the factors with have positive base and are real, while each factor with has negative base and contributes a phase . The total phase is therefore , and gives the stated formula. This is the jump of the multivalued function across its cut.
Preamble
import Mathlib open scoped BigOperators Interval
Formal statement
namespace WeightedRootIntegralIdentity
theorem weighted_root_complex_boundary_jump
(n : ℕ) (a w : ℕ → ℝ)
(hmono : ∀ i < n - 1, a i ≤ a (i + 1))
(hwsum : (∑ i ∈ Finset.range n, w i) = 1)
(k : ℕ) (hk : k < n - 1) (x : ℝ) (hxl : a k < x) (hxr : x < a (k + 1)) :
(∏ i ∈ Finset.range n, ((x : ℂ) - (a i : ℂ)) ^ ((w i : ℂ))).im
= Real.sin (Real.pi * (∑ i ∈ Finset.range (k + 1), w i)) *
∏ i ∈ Finset.range n, Real.rpow |x - a i| (w i) := by sorry
end WeightedRootIntegralIdentity
Source
Feng Qi, Xiao-Jing Zhang, and Wen-Hui Li, An integral representation for the weighted geometric mean and its applications, Acta Mathematica Sinica (English Series) 30 (2014), Theorem 3.1 (case z = 0); the identity is summarized as equation (4) at https://math.stackexchange.com/questions/4244874/can-we-prove-am-gm-inequality-using-these-integrals . This statement is one of the two steps of the standard contour-integral proof of that theorem, introduced here as a lemma in the decomposition of WeightedRootIntegralIdentity.weighted_geometric_mean_integral_identity.