Documentation

Verification.Nelsen16

← Mathematical handbook

noncomputable def Verification.n16Rad (θ t : ℝ) :

Equations

Verification.n16Rad θ t = √((1 - t - θ) ^ 2 + 4 * θ)

Instances For

noncomputable def Verification.n16Psi (θ t : ℝ) :

Equations

Verification.n16Psi θ t = (1 - t - θ + Verification.n16Rad θ t) / 2

Instances For

noncomputable def Verification.n16PsiDeriv (θ t : ℝ) :

Equations

Verification.n16PsiDeriv θ t = -(1 + (1 - t - θ) / Verification.n16Rad θ t) / 2

Instances For

theorem Verification.n16Rad_pos {θ t : ℝ} (hθ : 0 < θ) :

0 < n16Rad θ t

theorem Verification.n16Rad_sq {θ t : ℝ} (hθ : 0 ≤ θ) :

n16Rad θ t ^ 2 = (1 - t - θ) ^ 2 + 4 * θ

theorem Verification.n16Rad_deriv {θ t : ℝ} (hθ : 0 < θ) :

HasDerivAt (n16Rad θ) (-(1 - t - θ) / n16Rad θ t) t

theorem Verification.n16Psi_deriv {θ t : ℝ} (hθ : 0 < θ) :

HasDerivAt (n16Psi θ) (n16PsiDeriv θ t) t

theorem Verification.n16Psi_deriv2 {θ t : ℝ} (hθ : 0 < θ) :

HasDerivAt (n16PsiDeriv θ) (2 * θ / n16Rad θ t ^ 3) t

theorem Verification.n16Psi_convex {θ : ℝ} (hθ : 0 < θ) :

ConvexOn ℝ (Set.Ici 0) (n16Psi θ)

theorem Verification.n16Psi_antitone {θ : ℝ} (hθ : 0 < θ) :

AntitoneOn (n16Psi θ) (Set.Ici 0)

noncomputable def Verification.nelsen16Generator (θ : ℝ) (hθ : 0 < θ) :

ProbabilityTheory.Copula.BivariateGenerator

Equations

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

Instances For

noncomputable def Verification.nelsen16 (θ : ℝ) (hθ : 0 ≤ θ) :

ProbabilityTheory.Copula 2

Equations

Verification.nelsen16 θ hθ = if hz : θ = 0 then ProbabilityTheory.Copula.countermonotonic else (Verification.nelsen16Generator θ ⋯).copula

Instances For

theorem Verification.nelsen16_zero :

nelsen16 0 ⋯ = ProbabilityTheory.Copula.countermonotonic

theorem Verification.nelsen16_cdf (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) :

(nelsen16 θ ⋯).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else have s := ↑u + ↑v - 1 - θ * ((↑u)⁻¹ + (↑v)⁻¹ - 1); (s + √(s ^ 2 + 4 * θ)) / 2

theorem Verification.nelsen16_cdf_full (θ : ℝ) (hθ : 0 ≤ θ) (u v : ↑unitInterval) :

(nelsen16 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else have s := ↑u + ↑v - 1 - θ * ((↑u)⁻¹ + (↑v)⁻¹ - 1); (s + √(s ^ 2 + 4 * θ)) / 2

theorem Verification.nelsen16_cdf_continuous_parameter (u v : ↑unitInterval) :

Continuous fun (θ : ↑(Set.Ici 0)) => (nelsen16 ↑θ ⋯).cdf ![u, v]

theorem Verification.nelsen16_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 ≤ θ a) (ht : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) :

Filter.Tendsto (fun (a : α) => (nelsen16 (θ a) ⋯).cdf ![u, v]) l (nhds (ProbabilityTheory.Copula.countermonotonic.cdf ![u, v]))