Schur order in the Fréchet and Mardia families #

Reflecting the first coordinate swaps the M and W weights of a Fréchet copula and preserves Schur equivalence. Hence every Fréchet copula whose weight pair lies in {λ₁(a,b)+λ₂(b,a) : λ₁,λ₂≥0, λ₁+λ₂≤1} is Schur-below Frechet(a,b) (a mixture of two Schur-equivalent copulas with independence). For Mardia, t=θ/η∈[0,1] gives λ₁=(t²+t³)/2, λ₂=(t²-t³)/2. This proves Schur monotonicity in |θ| on each sign (Table 5 / Appendix A.4.2, * cell), and on the unmixed Fréchet axes.

source

theorem Verification.FrechetSchur.frechet_cdf_two (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) (u v : ↑unitInterval) :

(ProbabilityTheory.Copula.frechet a b ha hb hab).cdf ![u, v] = a * min ↑u ↑v + b * max 0 (↑u + ↑v - 1) + (1 - a - b) * (↑u * ↑v)

source

theorem Verification.FrechetSchur.frechet_reflect_first (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) :

(ProbabilityTheory.Copula.frechet a b ha hb hab).reflect {0} = ProbabilityTheory.Copula.frechet b a hb ha ⋯

source

theorem Verification.FrechetSchur.frechet_isExchangeable (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) :

(ProbabilityTheory.Copula.frechet a b ha hb hab).IsExchangeable

source

theorem Verification.FrechetSchur.frechet_swap_schurLE (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) :

(ProbabilityTheory.Copula.frechet b a hb ha ⋯).SchurLE (ProbabilityTheory.Copula.frechet a b ha hb hab)

source

theorem Verification.FrechetSchur.frechet_schurLE_of_combo {a b l₁ l₂ : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) (hl₁ : 0 ≤ l₁) (hl₂ : 0 ≤ l₂) (hl : l₁ + l₂ ≤ 1) (ha' : 0 ≤ l₁ * a + l₂ * b) (hb' : 0 ≤ l₁ * b + l₂ * a) (hab' : l₁ * a + l₂ * b + (l₁ * b + l₂ * a) ≤ 1) :

(ProbabilityTheory.Copula.frechet (l₁ * a + l₂ * b) (l₁ * b + l₂ * a) ha' hb' hab').SchurLE (ProbabilityTheory.Copula.frechet a b ha hb hab)

A convex combination of (a,b), (b,a) and (0,0) is Schur-below Frechet(a,b).

source

theorem Verification.FrechetSchur.mardia_weights (θ : ℝ) (hθ : |θ| ≤ 1) :

ProbabilityTheory.Copula.mardia θ hθ = ProbabilityTheory.Copula.frechet (θ ^ 2 * (1 + θ) / 2) (θ ^ 2 * (1 - θ) / 2) ⋯ ⋯ ⋯

source

theorem Verification.FrechetSchur.mardia_schurLE_of_ratio {θ η : ℝ} (hθ : |θ| ≤ 1) (hη : |η| ≤ 1) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) (hte : θ = t * η) :

(ProbabilityTheory.Copula.mardia θ hθ).SchurLE (ProbabilityTheory.Copula.mardia η hη)

Mardia: if θ=tη with t∈[0,1], then C_θ ≤_∂S C_η.

source

theorem Verification.FrechetSchur.mardia_isExchangeable (θ : ℝ) (hθ : |θ| ≤ 1) :

(ProbabilityTheory.Copula.mardia θ hθ).IsExchangeable

source

theorem Verification.FrechetSchur.mardia_schur_nonnegative {θ η : ℝ} (hθ : 0 ≤ θ) (hθη : θ ≤ η) (hη : η ≤ 1) :

(ProbabilityTheory.Copula.mardia θ ⋯).SchurBothLE (ProbabilityTheory.Copula.mardia η ⋯)

Table 5 (* cell): Mardia increases in both-direction Schur order on θ≥0.

source

theorem Verification.FrechetSchur.mardia_schur_nonpositive {θ η : ℝ} (hθ : -1 ≤ θ) (hθη : θ ≤ η) (hη : η ≤ 0) :

(ProbabilityTheory.Copula.mardia η ⋯).SchurBothLE (ProbabilityTheory.Copula.mardia θ ⋯)

Table 5 (* cell): Mardia decreases in both-direction Schur order on θ≤0.

source

theorem Verification.FrechetSchur.frechet_schur_mono_first {a a' : ℝ} (ha : 0 ≤ a) (haa : a ≤ a') (ha' : a' ≤ 1) :

(ProbabilityTheory.Copula.frechet a 0 ha ⋯ ⋯).SchurBothLE (ProbabilityTheory.Copula.frechet a' 0 ⋯ ⋯ ⋯)

Fréchet: on the axis b=0, Schur order increases with the M weight.

source

theorem Verification.FrechetSchur.frechet_schur_mono_second {b b' : ℝ} (hb : 0 ≤ b) (hbb : b ≤ b') (hb' : b' ≤ 1) :

(ProbabilityTheory.Copula.frechet 0 b ⋯ hb ⋯).SchurBothLE (ProbabilityTheory.Copula.frechet 0 b' ⋯ ⋯ ⋯)

Fréchet: on the axis a=0, Schur order increases with the W weight.