← Copula mathematical handbook

Minimizing the third power sum at fixed first and second power sums

def ProbabilityTheory.Copula.RankRegion.RhoTau.momentFibre {ι : Type u_1} [Fintype ι] (q : ℝ) : Set (ι → ℝ)

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.momentFibre q = {u : ι → ℝ | (∀ (i : ι), 0 ≤ u i) ∧ ∑ i : ι, u i = 1 ∧ ∑ i : ι, u i ^ 2 = q}

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.isCompact_momentFibre {ι : Type u_1} [Fintype ι] (q : ℝ) : IsCompact (momentFibre q)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.exists_min_powerSum_three {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) (hs : ∑ i : ι, u i = 1) : ∃ v ∈ momentFibre (∑ i : ι, u i ^ 2), ∑ i : ι, v i ^ 3 ≤ ∑ i : ι, u i ^ 3 ∧ ∀ w ∈ momentFibre (∑ i : ι, u i ^ 2), ∑ i : ι, v i ^ 3 ≤ ∑ i : ι, w i ^ 3

def ProbabilityTheory.Copula.RankRegion.RhoTau.replaceThree {ι : Type u_1} [DecidableEq ι] (u : ι → ℝ) (i j k : ι) (a b c : ℝ) : ι → ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.replaceThree u i j k a b c = Function.update (Function.update (Function.update u i a) j b) k c

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.sum_replaceThree {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : ι → ℝ) (i j k : ι) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (a b c : ℝ) (f : ℝ → ℝ) : ∑ l : ι, f (replaceThree u i j k a b c l) = ∑ l : ι, f (u l) - f (u i) - f (u j) - f (u k) + f a + f b + f c

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.minimizing_no_unique_largest {ι : Type u_1} [Fintype ι] [DecidableEq ι] {q : ℝ} {v : ι → ℝ} (hv : v ∈ momentFibre q) (hmin : ∀ w ∈ momentFibre q, ∑ i : ι, v i ^ 3 ≤ ∑ i : ι, w i ^ 3) (i j k : ι) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (hxy : v j < v i) (hyz : v k ≤ v j) (hz : 0 < v k) : False

At a minimizing vector, no positive triple has a unique largest entry.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.minimizing_shape {ι : Type u_1} [Fintype ι] [DecidableEq ι] {q : ℝ} {v : ι → ℝ} (hv : v ∈ momentFibre q) (hmin : ∀ w ∈ momentFibre q, ∑ i : ι, v i ^ 3 ≤ ∑ i : ι, w i ^ 3) : ∃ (k : ℕ) (r : ℝ) (b : ℝ), 0 < k ∧ 0 < r ∧ 0 ≤ b ∧ b ≤ r ∧ ∀ (p : ℕ), 0 < p → ∑ i : ι, v i ^ p = ↑k * r ^ p + b ^ p

A minimizer has equal positive coordinates, apart from at most one smaller coordinate.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.powerSum_prototype {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) (hs : ∑ i : ι, u i = 1) : ∃ (k : ℕ) (r : ℝ) (b : ℝ), 0 < k ∧ 0 < r ∧ 0 ≤ b ∧ b ≤ r ∧ ↑k * r + b = 1 ∧ ↑k * r ^ 2 + b ^ 2 = ∑ i : ι, u i ^ 2 ∧ ↑k * r ^ 3 + b ^ 3 ≤ ∑ i : ι, u i ^ 3

Finite-dimensional symmetric-polynomial minimization, with an explicit two-level shape and no assumed extremal inequality.