← Mathematical handbook

theorem Verification.plackett_den_pos {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : 0 < plackettA θ ↑u ↑v + √(plackettD θ ↑u ↑v)

theorem Verification.plackett_cdf_rationalized {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : (plackett θ hθ).cdf ![u, v] = 2 * θ * ↑u * ↑v / (plackettA θ ↑u ↑v + √(plackettD θ ↑u ↑v))

theorem Verification.plackett_tendsto_parameter {A : Type u_1} {l : Filter A} (θ : A → ℝ) (hθ : ∀ (a : A), 0 < θ a) {η : ℝ} (hη : 0 < η) (ht : Filter.Tendsto θ l (nhds η)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : A) => (plackett (θ a) ⋯).cdf ![u, v]) l (nhds ((plackett η hη).cdf ![u, v]))

theorem Verification.plackettF_zero_parameter (u v : ↑unitInterval) : plackettF 0 ↑u ↑v = ProbabilityTheory.Copula.countermonotonic.cdf ![u, v]

theorem Verification.plackett_tendsto_zero {A : Type u_1} {l : Filter A} (θ : A → ℝ) (hθ : ∀ (a : A), 0 < θ a) (ht : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : A) => (plackett (θ a) ⋯).cdf ![u, v]) l (nhds (ProbabilityTheory.Copula.countermonotonic.cdf ![u, v]))

noncomputable def Verification.plackettNormalized (u v x : ℝ) : ℝ

Equations

• Verification.plackettNormalized u v x = (x + u + v - √((x + u + v) ^ 2 - 4 * (1 + x) * u * v)) / 2

theorem Verification.plackett_cdf_normalized {θ : ℝ} (hθ : 1 < θ) (u v : ↑unitInterval) : (plackett θ ⋯).cdf ![u, v] = plackettNormalized (↑u) (↑v) (θ - 1)⁻¹

theorem Verification.plackett_tendsto_atTop {A : Type u_1} {l : Filter A} (θ : A → ℝ) (hθ : ∀ (a : A), 0 < θ a) (ht : Filter.Tendsto θ l Filter.atTop) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : A) => (plackett (θ a) ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf ![u, v]))