Documentation

Verification.SchurUnorderedNelsen818

← Mathematical handbook

Schur non-monotonicity for Nelsen 8 and Nelsen 18 #

Nelsen 8 starts at W and tends to Clayton(1); an exact conditional energy computation at θ=5, threshold 1/4, and the strip inequality for the Clayton(1) limit exclude a decreasing Schur order. Nelsen 18 tends to M; its θ=2 member has median energy below 1/2, which excludes a decreasing Schur order.

Nelsen 8 #

source
theorem Verification.nelsen8_two_section {u : ℝ} (hu : u ∈ Set.Ioo (1 / 4) 1) :
(ProbabilityTheory.Copula.nelsen8 2 ⋯).cdfSection ProbabilityTheory.Copula.unitHalf u = (5 * u - 1) / (7 + u)
source
theorem Verification.nelsen8_two_median_energy_lt :
∫ (u : ↑unitInterval), (ProbabilityTheory.Copula.nelsen8 2 ⋯).conditionalCDF u ProbabilityTheory.Copula.unitHalf ^ 2 < 1 / 2
source
theorem Verification.nelsen8_not_schur_monotone :
¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η), (ProbabilityTheory.Copula.nelsen8 θ hθ).SchurLE (ProbabilityTheory.Copula.nelsen8 η ⋯)
source
noncomputable def Verification.unitQuarter :
↑unitInterval

The quarter point.

Equations
Instances For
    source
    theorem Verification.nelsen8_five_section {u : ℝ} (hu : u ∈ Set.Icc 0 1) :
    (ProbabilityTheory.Copula.nelsen8 5 ⋯).cdfSection unitQuarter u = max 0 ((7 * u - 3 / 4) / (13 + 12 * u))
    source
    theorem Verification.nelsen8_five_deriv {u : ℝ} (hu : u ∈ Set.Ioo 0 1) (hu3 : u ≠ 3 / 28) :
    deriv ((ProbabilityTheory.Copula.nelsen8 5 ⋯).cdfSection unitQuarter) u = if u < 3 / 28 then 0 else 100 / (13 + 12 * u) ^ 2
    source
    theorem Verification.nelsen8_five_quarter_energy :
    ∫ (u : ↑unitInterval), (ProbabilityTheory.Copula.nelsen8 5 ⋯).conditionalCDF u unitQuarter ^ 2 = 279 / 3600
    source
    theorem Verification.clayton_one_half_quarter :
    (ProbabilityTheory.Copula.clayton 2 1 ⋯).cdf ![ProbabilityTheory.Copula.unitHalf, unitQuarter] = 1 / 5
    source
    theorem Verification.nelsen8_not_schur_antitone :
    ¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η), (ProbabilityTheory.Copula.nelsen8 η ⋯).SchurLE (ProbabilityTheory.Copula.nelsen8 θ hθ)

    Nelsen 18 #

    source
    theorem Verification.nelsen18_two_section {u : ℝ} (hu : u ∈ Set.Ioo (1 / 3) (3 / 4)) :
    (nelsen18 2 ⋯).cdfSection ProbabilityTheory.Copula.unitHalf u = 1 + 2 / Real.log (Real.exp (2 / (u - 1)) + Real.exp (-4))
    source
    theorem Verification.nelsen18_two_median_energy_lt :
    ∫ (u : ↑unitInterval), (nelsen18 2 ⋯).conditionalCDF u ProbabilityTheory.Copula.unitHalf ^ 2 < 1 / 2
    source
    theorem Verification.nelsen18_not_schur_antitone :
    ¬∀ (θ η : ℝ) (hθ : 2 ≤ θ) (hθη : θ ≤ η), (nelsen18 η ⋯).SchurLE (nelsen18 θ hθ)