← Mathematical handbook

noncomputable def Verification.n22Base (t : ℝ) : ℝ

Equations

• Verification.n22Base t = 1 - Real.sin (min t (Real.pi / 2))

theorem Verification.n22Core_antitone : AntitoneOn (fun (t : ℝ) => 1 - Real.sin t) (Set.Icc 0 (Real.pi / 2))

theorem Verification.n22Core_convex : ConvexOn ℝ (Set.Icc 0 (Real.pi / 2)) fun (t : ℝ) => 1 - Real.sin t

theorem Verification.n22Base_convex : ConvexOn ℝ (Set.Ici 0) n22Base

noncomputable def Verification.n22BaseGenerator : ProbabilityTheory.Copula.BivariateGenerator

Equations

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

noncomputable def Verification.n22Generator (θ : ℝ) (hθ : 0 < θ) (hθ1 : θ ≤ 1) : ProbabilityTheory.Copula.BivariateGenerator

Equations

• Verification.n22Generator θ hθ hθ1 = Verification.n22BaseGenerator.innerPower θ⁻¹ ⋯

noncomputable def Verification.nelsen22 (θ : ℝ) (hθ : θ ∈ Set.Icc 0 1) : ProbabilityTheory.Copula 2

Equations

• Verification.nelsen22 θ hθ = if hz : θ = 0 then ProbabilityTheory.Copula.independence 2 else (Verification.n22Generator θ ⋯ ⋯).copula

theorem Verification.nelsen22_zero : nelsen22 0 ⋯ = ProbabilityTheory.Copula.independence 2

theorem Verification.nelsen22_cdf {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) (u v : ↑unitInterval) : (nelsen22 θ ⋯).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else (1 - Real.sin (min (Real.arcsin (1 - ↑u ^ θ) + Real.arcsin (1 - ↑v ^ θ)) (Real.pi / 2))) ^ θ⁻¹

theorem Verification.nelsen22_cdf_full {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) (u v : ↑unitInterval) : (nelsen22 θ ⋯).cdf ![u, v] = (1 - Real.sin (min (Real.arcsin (1 - ↑u ^ θ) + Real.arcsin (1 - ↑v ^ θ)) (Real.pi / 2))) ^ θ⁻¹

theorem Verification.nelsen22_cdf_printed {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) (u v : ↑unitInterval) : (nelsen22 θ ⋯).cdf ![u, v] = if -(Real.pi / 2) ≤ Real.arcsin (↑u ^ θ - 1) + Real.arcsin (↑v ^ θ - 1) then (1 + Real.sin (Real.arcsin (↑u ^ θ - 1) + Real.arcsin (↑v ^ θ - 1))) ^ θ⁻¹ else 0