← Mathematical handbook

noncomputable def Verification.n22Angle (u v a : ℝ) : ℝ

Equations

• Verification.n22Angle u v a = Real.arcsin (1 - u ^ a) + Real.arcsin (1 - v ^ a)

noncomputable def Verification.n22Body (u v a : ℝ) : ℝ

Equations

• Verification.n22Body u v a = 1 - Real.sin (Verification.n22Angle u v a)

theorem Verification.n22Angle_deriv_zero {u v : ℝ} (hu : 0 < u) (hv : 0 < v) : HasDerivAt (n22Angle u v) (-(Real.log u + Real.log v)) 0

theorem Verification.n22Body_deriv_zero {u v : ℝ} (hu : 0 < u) (hv : 0 < v) : HasDerivAt (n22Body u v) (Real.log u + Real.log v) 0

theorem Verification.nelsen22_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), θ a ∈ Set.Icc 0 1) (ht : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (nelsen22 (θ a) ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.independence 2).cdf ![u, v]))

theorem Verification.nelsen22_tendsto_positive_parameter {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), θ a ∈ Set.Icc 0 1) {η : ℝ} (hη : 0 < η) (hη1 : η ≤ 1) (ht : Filter.Tendsto θ l (nhds η)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (nelsen22 (θ a) ⋯).cdf ![u, v]) l (nhds ((nelsen22 η ⋯).cdf ![u, v]))

theorem Verification.nelsen22_tendsto_parameter {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), θ a ∈ Set.Icc 0 1) {η : ℝ} (hη : η ∈ Set.Icc 0 1) (ht : Filter.Tendsto θ l (nhds η)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (nelsen22 (θ a) ⋯).cdf ![u, v]) l (nhds ((nelsen22 η hη).cdf ![u, v]))