Table 3: families that are not Schur ordered in their parameter #
Table 3 marks Nelsen 2, Nelsen 8, Genest–Ghoudi (Nelsen 15), Nelsen 18 and Nelsen 21 as not
ordered in ≤_∂S (numerical observation *). We prove, for the directional order and hence
for the two-direction order, that Nelsen 2, Nelsen 8 and Genest–Ghoudi are neither
increasing nor decreasing, and that Nelsen 18 is not decreasing. (Nelsen 21 is covered in
Nelsen21.lean.) For Archimedean copulas the directional and two-direction orders agree.
theorem
Papers.AnsariRockel2024.nelsen2_not_schur_monotone :
¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η),
(ProbabilityTheory.Copula.nelsen2 θ hθ).SchurLE (ProbabilityTheory.Copula.nelsen2 η ⋯)
theorem
Papers.AnsariRockel2024.nelsen2_not_schur_antitone :
¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η),
(ProbabilityTheory.Copula.nelsen2 η ⋯).SchurLE (ProbabilityTheory.Copula.nelsen2 θ hθ)
theorem
Papers.AnsariRockel2024.genestGhoudi_not_schur_monotone :
¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η),
(ProbabilityTheory.Copula.genestGhoudi θ hθ).SchurLE (ProbabilityTheory.Copula.genestGhoudi η ⋯)
theorem
Papers.AnsariRockel2024.genestGhoudi_not_schur_antitone :
¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η),
(ProbabilityTheory.Copula.genestGhoudi η ⋯).SchurLE (ProbabilityTheory.Copula.genestGhoudi θ hθ)
theorem
Papers.AnsariRockel2024.nelsen8_not_schur_monotone :
¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η),
(ProbabilityTheory.Copula.nelsen8 θ hθ).SchurLE (ProbabilityTheory.Copula.nelsen8 η ⋯)
theorem
Papers.AnsariRockel2024.nelsen8_not_schur_antitone :
¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η),
(ProbabilityTheory.Copula.nelsen8 η ⋯).SchurLE (ProbabilityTheory.Copula.nelsen8 θ hθ)
theorem
Papers.AnsariRockel2024.nelsen8_five_quarter_energy :
∫ (u : ↑unitInterval), (ProbabilityTheory.Copula.nelsen8 5 ⋯).conditionalCDF u Verification.unitQuarter ^ 2 = 279 / 3600
Exact conditional energy of Nelsen 8 at θ=5, threshold 1/4, used above.
theorem
Papers.AnsariRockel2024.nelsen18_not_schur_antitone :
¬∀ (θ η : ℝ) (hθ : 2 ≤ θ) (hθη : θ ≤ η), (Verification.nelsen18 η ⋯).SchurLE (Verification.nelsen18 θ hθ)