← Mathematical handbook

noncomputable def Verification.n16Root (a k θ : ℝ) : ℝ

Equations

• Verification.n16Root a k θ = (a - θ * k + √((a - θ * k) ^ 2 + 4 * θ)) / 2

theorem Verification.n16Root_properties {a k θ : ℝ} (hθ : 0 ≤ θ) : 0 ≤ n16Root a k θ ∧ n16Root a k θ ^ 2 - (a - θ * k) * n16Root a k θ - θ = 0 ∧ 0 ≤ 2 * n16Root a k θ - (a - θ * k)

theorem Verification.n16Root_bound {a k θ : ℝ} (hθ : 0 ≤ θ) (hk : 0 < k) (ha : a * k ≤ 1) : k * n16Root a k θ ≤ 1

theorem Verification.n16Root_monotone {a k θ η : ℝ} (hθ : 0 ≤ θ) (hθη : θ ≤ η) (hk : 0 < k) (ha : a * k ≤ 1) : n16Root a k θ ≤ n16Root a k η

theorem Verification.n16_inverse_sum_pos {u v : ↑unitInterval} (hu : 0 < ↑u) (hv : 0 < ↑v) : 0 < (↑u)⁻¹ + (↑v)⁻¹ - 1

theorem Verification.n16_sum_bound {u v : ↑unitInterval} (hu : 0 < ↑u) (hv : 0 < ↑v) : (↑u + ↑v - 1) * ((↑u)⁻¹ + (↑v)⁻¹ - 1) ≤ 1

theorem Verification.nelsen16_lowerOrthant_monotone {θ η : ℝ} (hθ : 0 ≤ θ) (hη : 0 ≤ η) (hθη : θ ≤ η) : (nelsen16 θ hθ).LowerOrthantLE (nelsen16 η hη)

theorem Verification.n16Root_scaled_lower {a k θ : ℝ} (hθ : 0 < θ) (hk : 1 ≤ k) (ha : a * k ≤ 1) (ha0 : -1 ≤ a) : 1 - 2 / θ ≤ k * n16Root a k θ

theorem Verification.n16Root_tendsto_atTop {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (z : α), 0 ≤ θ z) (hlim : Filter.Tendsto θ l Filter.atTop) {a k : ℝ} (hk : 1 ≤ k) (ha : a * k ≤ 1) (ha0 : -1 ≤ a) : Filter.Tendsto (fun (z : α) => n16Root a k (θ z)) l (nhds k⁻¹)

theorem Verification.nelsen16_tendsto_atTop {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (z : α), 0 ≤ θ z) (hlim : Filter.Tendsto θ l Filter.atTop) (u v : ↑unitInterval) : Filter.Tendsto (fun (z : α) => (nelsen16 (θ z) ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.clayton 2 1 ⋯).cdf ![u, v]))