← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.continuous_a {ι : Type u_1} [Fintype ι] (S : SignData ι) : Continuous S.a

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.continuous_b {ι : Type u_1} [Fintype ι] (S : SignData ι) : Continuous S.b

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.a_nonneg {ι : Type u_1} [Fintype ι] (S : SignData ι) (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) : 0 ≤ S.a u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.b_nonneg {ι : Type u_1} [Fintype ι] (S : SignData ι) (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) : 0 ≤ S.b u

def ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.simplexFibre {ι : Type u_1} [Fintype ι] (S : SignData ι) (x : ℝ) : Set (ι → ℝ)

Equations

• S.simplexFibre x = {u : ι → ℝ | (∀ (i : ι), 0 ≤ u i) ∧ ∑ i : ι, u i = 1 ∧ S.a u = x}

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.isCompact_simplexFibre {ι : Type u_1} [Fintype ι] (S : SignData ι) (x : ℝ) : IsCompact (S.simplexFibre x)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.exists_finite_minimizer {n : ℕ} (π : Equiv.Perm (Fin n)) (u : Fin n → ℝ) (hu : ∀ (i : Fin n), 0 ≤ u i) (hs : ∑ i : Fin n, u i = 1) : ∃ (σ : Equiv.Perm (Fin n)), ∃ v ∈ (permutationSigns σ).simplexFibre ((permutationSigns π).a u), (permutationSigns σ).b v ≤ (permutationSigns π).b u ∧ ∀ (θ : Equiv.Perm (Fin n)), ∀ w ∈ (permutationSigns θ).simplexFibre ((permutationSigns π).a u), (permutationSigns σ).b v ≤ (permutationSigns θ).b w

A global finite minimizer exists over all permutations and all weights at fixed a.