← Mathematical handbook

noncomputable def Verification.n10Half : ↑unitInterval

Equations

• Verification.n10Half = ⟨1 / 2, Verification.n10Half._proof_2⟩

noncomputable def Verification.n10Low : ↑unitInterval

Equations

• Verification.n10Low = ⟨1 / 16, Verification.n10Low._proof_2⟩

noncomputable def Verification.n10High : ↑unitInterval

Equations

• Verification.n10High = ⟨9 / 16, Verification.n10High._proof_2⟩

theorem Verification.nelsen10_crossing_low : (nelsen10 n10Half).cdf ![n10Low, n10Low] < (nelsen10 1).cdf ![n10Low, n10Low]

theorem Verification.nelsen10_crossing_high : (nelsen10 1).cdf ![n10High, n10High] < (nelsen10 n10Half).cdf ![n10High, n10High]

theorem Verification.nelsen10_orthant_incomparable : ¬(nelsen10 n10Half).LowerOrthantLE (nelsen10 1) ∧ ¬(nelsen10 1).LowerOrthantLE (nelsen10 n10Half)

theorem Verification.nelsen10_schur_incomparable : ¬(nelsen10 n10Half).SchurLE (nelsen10 1) ∧ ¬(nelsen10 1).SchurLE (nelsen10 n10Half)

theorem Verification.nelsen10_schurBoth_incomparable : ¬(nelsen10 n10Half).SchurBothLE (nelsen10 1) ∧ ¬(nelsen10 1).SchurBothLE (nelsen10 n10Half)