theorem negGeomMean_prod_deriv_at0 {n : ℕ} {x z : Fin n → ℝ} (hx : ∀ (i : Fin n), x i ≠ 0) : have P := fun (t : ℝ) => ∏ i : Fin n, (x i + t * z i); deriv P 0 = (∏ i : Fin n, x i) * ∑ i : Fin n, z i / x i

First derivative of the coordinate product along a line at 0.

theorem negGeomMean_prod_second_deriv_at0 {n : ℕ} {x z : Fin n → ℝ} (hx : ∀ (i : Fin n), x i ≠ 0) : have P := fun (t : ℝ) => ∏ i : Fin n, (x i + t * z i); deriv (deriv P) 0 = (∏ i : Fin n, x i) * ((∑ i : Fin n, z i / x i) ^ 2 - ∑ i : Fin n, (z i / x i) ^ 2)

Second derivative of the coordinate product along a line at 0.

theorem continuousOn_negGeomMean_nonneg {n : ℕ} : ContinuousOn (fun (x : Fin n → ℝ) => -(∏ i : Fin n, x i).rpow (1 / ↑n)) {x : Fin n → ℝ | ∀ (i : Fin n), 0 ≤ x i}

The negative geometric mean is continuous on the nonnegative orthant.

theorem prod_line_ne_zero_eventually {n : ℕ} {x z : Fin n → ℝ} (hx : ∀ (i : Fin n), 0 < x i) : ∀ᶠ (t : ℝ) in nhds 0, ∏ i : Fin n, (x i + t * z i) ≠ 0

The line product is nonzero near 0 when the base point is positive.

theorem deriv_line_prod_differentiable_at0 {n : ℕ} {x z : Fin n → ℝ} : DifferentiableAt ℝ (fun (t : ℝ) => deriv (fun (s : ℝ) => ∏ i : Fin n, (x i + s * z i)) t) 0

The derivative of the line product is differentiable at 0.

theorem line_rpow_second_deriv_at0 {P : ℝ → ℝ} {a : ℝ} (hP0 : P 0 ≠ 0) (hP_diff : ∀ᶠ (t : ℝ) in nhds 0, DifferentiableAt ℝ P t) (hP_near : ∀ᶠ (t : ℝ) in nhds 0, P t ≠ 0) (hP0_diff : DifferentiableAt ℝ P 0) (hP' : DifferentiableAt ℝ (deriv P) 0) : deriv (deriv fun (t : ℝ) => P t ^ a) 0 = a * (a - 1) * P 0 ^ (a - 1 - 1) * deriv P 0 ^ 2 + a * P 0 ^ (a - 1) * deriv (deriv P) 0

Second derivative of t ↦ (P t)^a at 0 under a local nonzero hypothesis.

theorem negGeomMean_line_second_deriv {n : ℕ} (hn : n ≠ 0) {x z : Fin n → ℝ} (hx : ∀ (i : Fin n), 0 < x i) : have g := fun (x : Fin n → ℝ) => -(∏ i : Fin n, x i).rpow (1 / ↑n); deriv (deriv fun (t : ℝ) => g (x + t • z)) 0 = (1 / ↑n) ^ 2 * g x * ((∑ i : Fin n, z i / x i) ^ 2 - ↑n * ∑ i : Fin n, (z i / x i) ^ 2)

Second derivative of the negative geometric mean along a line.

theorem negGeomMean_hessian_quadratic_form {n : ℕ} (hn : n ≠ 0) {x z : Fin n → ℝ} (hx : ∀ (i : Fin n), 0 < x i) : star z ⬝ᵥ (hessianMatrix (fun (x : Fin n → ℝ) => -(∏ i : Fin n, x i).rpow (1 / ↑n)) x).mulVec z = (1 / ↑n) ^ 2 * -(∏ i : Fin n, x i).rpow (1 / ↑n) * ((∑ i : Fin n, z i / x i) ^ 2 - ↑n * ∑ i : Fin n, (z i / x i) ^ 2)

The Hessian quadratic form for the negative geometric mean.

theorem negGeomMean_quadratic_form_nonneg {n : ℕ} {x z : Fin n → ℝ} (hx : ∀ (i : Fin n), 0 < x i) : 0 ≤ (1 / ↑n) ^ 2 * -(∏ i : Fin n, x i).rpow (1 / ↑n) * ((∑ i : Fin n, z i / x i) ^ 2 - ↑n * ∑ i : Fin n, (z i / x i) ^ 2)

Nonnegativity of the quadratic form for the negative geometric mean.

theorem negGeomMean_hessian_posSemidef {n : ℕ} (hn : n ≠ 0) (x : Fin n → ℝ) : (∀ (i : Fin n), 0 < x i) → (hessianMatrix (fun (x : Fin n → ℝ) => -(∏ i : Fin n, x i).rpow (1 / ↑n)) x).PosSemidef

The Hessian of the negative geometric mean is positive semidefinite on the positive orthant.

theorem convexOn_negGeomMean_pos {n : ℕ} (hn : n ≠ 0) : ConvexOn ℝ {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i} fun (x : Fin n → ℝ) => -(∏ i : Fin n, x i).rpow (1 / ↑n)

Convexity of the negative geometric mean on the positive orthant.