Means and branch-safe quadratic domains

noncomputable def DirichletTransform.TwoVariable.arithmeticMeanSq (x y : ℂ) : ℂ

The squared arithmetic mean occurring in Carlson's first quadratic transformation.

Equations

• DirichletTransform.TwoVariable.arithmeticMeanSq x y = ((x + y) / 2) ^ 2

def DirichletTransform.TwoVariable.geometricMeanSq (x y : ℂ) : ℂ

The squared geometric mean occurring in Carlson's first quadratic transformation.

Equations

• DirichletTransform.TwoVariable.geometricMeanSq x y = x * y

theorem DirichletTransform.TwoVariable.arithmeticMeanSq_comm (x y : ℂ) : arithmeticMeanSq x y = arithmeticMeanSq y x

The arithmetic mean is symmetric in its arguments.

theorem DirichletTransform.TwoVariable.geometricMeanSq_comm (x y : ℂ) : geometricMeanSq x y = geometricMeanSq y x

The squared geometric mean is symmetric in its arguments.

def DirichletTransform.TwoVariable.FirstQuadraticDomain (x y : ℂ) : Prop

Branch-safe domain for Carlson's first quadratic transformation 6.9-3.

Equations

• One or more equations did not get rendered due to their size.

def DirichletTransform.TwoVariable.SecondQuadraticDomain (x y : ℂ) : Prop

Branch-safe domain for Carlson's second quadratic transformation 6.10-1.

Equations

• One or more equations did not get rendered due to their size.

theorem DirichletTransform.TwoVariable.FirstQuadraticDomain.affine {x y : ℂ} (hz : FirstQuadraticDomain x y) {r : ℝ} (hr : r ∈ Set.Icc 0 1) : FirstQuadraticDomain (1 - ↑r + ↑r * x) (1 - ↑r + ↑r * y)

The branch-safe domain is preserved along the segment from the all-one nodes.

theorem DirichletTransform.TwoVariable.SecondQuadraticDomain.affine {x y : ℂ} (hz : SecondQuadraticDomain x y) (hx : 0 < x.re) (hy : 0 < y.re) {r : ℝ} (hr : r ∈ Set.Icc 0 1) : SecondQuadraticDomain (1 - ↑r + ↑r * x) (1 - ↑r + ↑r * y)

The component with positive-real-part square roots is star-shaped about (1,1).

theorem DirichletTransform.TwoVariable.SecondQuadraticDomain.same_sign {x y : ℂ} (hz : SecondQuadraticDomain x y) : 0 < x.re ∧ 0 < y.re ∨ 0 < (-x).re ∧ 0 < (-y).re

The two square-root nodes lie in the same component of the square preimage of the right half-plane. The product condition rules out opposite components.