← Mathematical handbook

theorem Verification.plackettF_symm (θ u v : ℝ) : plackettF θ u v = plackettF θ v u

theorem Verification.plackettF_zero {θ v : ℝ} (hθ : 0 < θ) (hv : v ∈ Set.Icc 0 1) : plackettF θ 0 v = 0

theorem Verification.plackettF_one {θ v : ℝ} (hθ : 0 < θ) (hne : θ ≠ 1) (hv : v ∈ Set.Icc 0 1) : plackettF θ 1 v = v

theorem Verification.plackettP_monotone {θ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Icc 0 1) : MonotoneOn (plackettP θ u) (Set.Icc 0 1)

theorem Verification.plackettF_rectangle {θ : ℝ} (hθ : 0 < θ) (hne : θ ≠ 1) (a b c d : ↑unitInterval) (hab : a ≤ b) (hcd : c ≤ d) : 0 ≤ plackettF θ ↑b ↑d - plackettF θ ↑a ↑d - plackettF θ ↑b ↑c + plackettF θ ↑a ↑c

theorem Verification.plackett_isClassical {θ : ℝ} (hθ : 0 < θ) (hne : θ ≠ 1) : ProbabilityTheory.Copula.IsClassical fun (u : Fin 2 → ↑unitInterval) => plackettF θ ↑(u 0) ↑(u 1)

noncomputable def Verification.plackett (θ : ℝ) (hθ : 0 < θ) : ProbabilityTheory.Copula 2

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.plackett_one : plackett 1 ⋯ = ProbabilityTheory.Copula.independence 2

theorem Verification.plackett_cdf {θ : ℝ} (hθ : 0 < θ) (hne : θ ≠ 1) (u v : ↑unitInterval) : (plackett θ hθ).cdf ![u, v] = (1 + (θ - 1) * (↑u + ↑v) - √((1 + (θ - 1) * (↑u + ↑v)) ^ 2 - 4 * θ * (θ - 1) * ↑u * ↑v)) / (2 * (θ - 1))