← Mathematical handbook

Nelsen 18 is not Schur-increasing in its parameter

At threshold v=1/9, with q=θ/(u-1), S=e^q+e^{θ/(v-1)}, L=log S and p=e^q/S, the conditional CDF on the positive region L<-θ equals e^q q²/(S L²)=p(1+(-log p)/(-L))². For θ=4 this is at most p(1-log p/4)² ≤ (2/5)(1+log(5/2)/4)² ≤ 5/8, because p<1-e^{-1/2}≤2/5. For θ=2, at the point with e^q=e^{-9/4}/4 (so p=1/5) it is (9/4+2log 2)²/(5(9/4-log(5/4))²)>5/8. The convex test z ↦ (z-5/8)₊ therefore separates the two conditional CDFs, so C₂ ≤_∂S C₄ fails.

noncomputable def Verification.N18Schur.S (θ K x : ℝ) : ℝ

Equations

• Verification.N18Schur.S θ K x = Real.exp (θ / (x - 1)) + K

noncomputable def Verification.N18Schur.F (θ K x : ℝ) : ℝ

Equations

• Verification.N18Schur.F θ K x = 1 + θ / Real.log (Verification.N18Schur.S θ K x)

noncomputable def Verification.N18Schur.G (θ K x : ℝ) : ℝ

Equations

• Verification.N18Schur.G θ K x = θ ^ 2 * Real.exp (θ / (x - 1)) / ((x - 1) ^ 2 * Verification.N18Schur.S θ K x * Real.log (Verification.N18Schur.S θ K x) ^ 2)

theorem Verification.N18Schur.S_pos {θ K : ℝ} (hK : 0 < K) (x : ℝ) : 0 < S θ K x

theorem Verification.N18Schur.continuousAt_S {θ K x : ℝ} (hx : x ≠ 1) : ContinuousAt (S θ K) x

theorem Verification.N18Schur.hasDerivAt_F {θ K x : ℝ} (hK : 0 < K) (hx : x ≠ 1) (hL : Real.log (S θ K x) ≠ 0) : HasDerivAt (F θ K) (G θ K x) x

theorem Verification.N18Schur.cdfSection_eq (θ : ℝ) (hθ : 2 ≤ θ) (v : ↑unitInterval) (hv : ↑v < 1) {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : (nelsen18 θ hθ).cdfSection v x = max 0 (F θ (Real.exp (θ / (↑v - 1))) x)

The CDF section on (0,1) for a threshold below one.

theorem Verification.N18Schur.hasDerivAt_cdfSection_pos (θ : ℝ) (hθ : 2 ≤ θ) (v : ↑unitInterval) (hv : ↑v < 1) {x : ℝ} (hx : x ∈ Set.Ioo 0 1) (hL : Real.log (S θ (Real.exp (θ / (↑v - 1))) x) < -θ) : HasDerivAt ((nelsen18 θ hθ).cdfSection v) (G θ (Real.exp (θ / (↑v - 1))) x) x

On the positive region the CDF section is differentiable with derivative G.

theorem Verification.N18Schur.hasDerivAt_cdfSection_zero (θ : ℝ) (hθ : 2 ≤ θ) (v : ↑unitInterval) (hv : ↑v < 1) {x : ℝ} (hx : x ∈ Set.Ioo 0 1) (hL : -θ < Real.log (S θ (Real.exp (θ / (↑v - 1))) x)) : HasDerivAt ((nelsen18 θ hθ).cdfSection v) 0 x

On the zero region the CDF section is locally zero.

The bound for θ=4

theorem Verification.N18Schur.hmono : MonotoneOn (fun (p : ℝ) => p * (1 - Real.log p / 4) ^ 2) (Set.Ioo 0 1)

h(p)=p(1-log p/4)² is monotone on (0,1).

theorem Verification.N18Schur.exp_neg_half_ge : 3 / 5 ≤ Real.exp (-(1 / 2))

theorem Verification.N18Schur.log_five_halves_le : Real.log (5 / 2) ≤ 1

theorem Verification.N18Schur.G_four_le {x : ℝ} (hx : x ∈ Set.Ioo 0 1) (hL : Real.log (S 4 (Real.exp (-(9 / 2))) x) < -4) : G 4 (Real.exp (-(9 / 2))) x ≤ 5 / 8

The θ=4 conditional CDF at v=1/9 is at most 5/8 on the positive region.

The witness for θ=2

noncomputable def Verification.N18Schur.qStar : ℝ

The witness point x* = 1 + 2/q* with q* = -9/4 - log 4.

Equations

• Verification.N18Schur.qStar = -(9 / 4) - Real.log 4

noncomputable def Verification.N18Schur.xStar : ℝ

Equations

• Verification.N18Schur.xStar = 1 + 2 / Verification.N18Schur.qStar

theorem Verification.N18Schur.log_four_bounds : 1.386294 < Real.log 4 ∧ Real.log 4 < 1.3863

theorem Verification.N18Schur.qStar_lt : qStar < -3

theorem Verification.N18Schur.xStar_mem : xStar ∈ Set.Ioo 0 1

theorem Verification.N18Schur.xStar_q : 2 / (xStar - 1) = qStar

theorem Verification.N18Schur.S_xStar : S 2 (Real.exp (-(9 / 4))) xStar = 5 / 4 * Real.exp (-(9 / 4))

theorem Verification.N18Schur.log_S_xStar : Real.log (S 2 (Real.exp (-(9 / 4))) xStar) = Real.log (5 / 4) - 9 / 4

theorem Verification.N18Schur.log_five_fourths_bounds : 1 / 5 ≤ Real.log (5 / 4) ∧ Real.log (5 / 4) < 1 / 4

theorem Verification.N18Schur.log_S_xStar_lt : Real.log (S 2 (Real.exp (-(9 / 4))) xStar) < -2

theorem Verification.N18Schur.G_xStar_gt : 5 / 8 < G 2 (Real.exp (-(9 / 4))) xStar

The separation

noncomputable def Verification.N18Schur.v9 : ↑unitInterval

The threshold v=1/9.

Equations

• Verification.N18Schur.v9 = ⟨1 / 9, Verification.N18Schur.v9._proof_1⟩

theorem Verification.N18Schur.v9_exp (θ : ℝ) : θ / (↑v9 - 1) = -(9 * θ / 8)

theorem Verification.N18Schur.hinge_convex : ConvexOn ℝ (Set.Icc 0 1) fun (z : ℝ) => max (z - 5 / 8) 0

theorem Verification.N18Schur.hinge_continuous : Continuous fun (z : ℝ) => max (z - 5 / 8) 0

theorem Verification.N18Schur.four_ae_le : ∀ᵐ (u : ↑unitInterval), (nelsen18 4 ⋯).conditionalCDF u v9 ≤ 5 / 8

For θ=4, the conditional CDF at v=1/9 is at most 5/8 almost everywhere.

theorem Verification.N18Schur.nelsen18_two_not_schurLE_four : ¬(nelsen18 2 ⋯).SchurLE (nelsen18 4 ⋯)

Nelsen 18 is not increasing in the directional Schur order: C₂ ≤_∂S C₄ fails.

theorem Verification.N18Schur.nelsen18_not_schur_monotone : ¬∀ (θ η : ℝ) (hθ : 2 ≤ θ) (hθη : θ ≤ η), (nelsen18 θ hθ).SchurLE (nelsen18 η ⋯)