← Copula mathematical handbook

inductive ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter : Type

A complete, countable collection of explicitly polynomial upper-boundary arcs.

• endpoint : UpperParameter
• right (data : RightData) : UpperParameter
• left (data : LeftData) : UpperParameter

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.footrule : UpperParameter → ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.endpoint.footrule = 1
• (ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.right S).footrule = 1 - 3 * (S.w + ↑S.N * S.v + ↑S.N * (↑S.N + 1) * S.v ^ 2)
• (ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.left S).footrule = 1 - 3 * (S.w + (↑S.N + 1) * S.v - ↑S.N * (↑S.N + 1) * S.v ^ 2)

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.rho : UpperParameter → ℝ

Equations

• One or more equations did not get rendered due to their size.
• ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.endpoint.rho = 1

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.copula : UpperParameter → Copula 2

Equations

• ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.endpoint.copula = ProbabilityTheory.Copula.comonotonic 2
• (ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.right S).copula = S.copula
• (ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.left S).copula = S.copula

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.coefficients (a : UpperParameter) : a.copula.spearmanFootrule = a.footrule ∧ a.copula.spearmanRho = a.rho

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.maximizes (a : UpperParameter) (C : Copula 2) (h : C.spearmanFootrule = a.footrule) : C.spearmanRho ≤ a.rho

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.rightFamily (N : ℕ) (hN : 0 < N) (s : ↑unitInterval) : RightData

Equations

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

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.leftFamily (N : ℕ) (hN : 0 < N) (s : ↑unitInterval) : LeftData

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.rightFamily_footrule (N : ℕ) (hN : 0 < N) (s : ↑unitInterval) : (UpperParameter.right (rightFamily N hN s)).footrule = 1 - 3 * (1 / (2 * (↑N + 1)) + ↑s ^ 2 / (4 * ↑N * (↑N + 1)))

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.leftFamily_footrule (N : ℕ) (hN : 0 < N) (s : ↑unitInterval) : (UpperParameter.left (leftFamily N hN s)).footrule = 1 - 3 * (1 / (2 * ↑N) - ↑s ^ 2 / (4 * ↑N * (↑N + 1)))

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.contact_interval_cover {m : ℝ} (hm : 0 < m) (hm1 : m ≤ 1 / 2) : ∃ (N : ℕ), 0 < N ∧ 1 / (2 * (↑N + 1)) ≤ m ∧ m ≤ 1 / (2 * ↑N)

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.upperParameter_exists {p : ℝ} (hp : p ∈ Set.Icc (-1 / 2) 1) : ∃ (a : UpperParameter), a.footrule = p