← Mathematical handbook

noncomputable def Verification.joeInv (θ u : ℝ) : ℝ

Equations

• Verification.joeInv θ u = -Real.log (1 - (1 - u) ^ θ)

noncomputable def Verification.joeWeight (θ u : ℝ) : ℝ

Equations

• Verification.joeWeight θ u = θ * (1 - u) ^ (θ - 1) / (1 - (1 - u) ^ θ)

noncomputable def Verification.joeDensityReal (θ u v : ℝ) : ℝ

Equations

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

noncomputable def Verification.joeDensity (θ : ℝ) (x : Fin 2 → ↑unitInterval) : ℝ

Equations

• Verification.joeDensity θ x = Verification.joeDensityReal θ ↑(x 0) ↑(x 1)

noncomputable def Verification.joePartial (θ u v : ℝ) : ℝ

Equations

• Verification.joePartial θ u v = -Verification.joePsiDeriv θ⁻¹ (Verification.joeInv θ u + Verification.joeInv θ v) * Verification.joeWeight θ u

noncomputable def Verification.joeRealCDF (θ u v : ℝ) : ℝ

Equations

• Verification.joeRealCDF θ u v = 1 - (1 - Real.exp (-(Verification.joeInv θ u + Verification.joeInv θ v))) ^ θ⁻¹

theorem Verification.joe_inv_base {θ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) : 0 < 1 - (1 - u) ^ θ ∧ 1 - (1 - u) ^ θ < 1

theorem Verification.joeInv_pos {θ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) : 0 < joeInv θ u

theorem Verification.joeWeight_pos {θ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) : 0 < joeWeight θ u

theorem Verification.joeInv_deriv {θ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) : HasDerivAt (joeInv θ) (-joeWeight θ u) u

theorem Verification.joeWeight_continuousAt {θ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) : ContinuousAt (joeWeight θ) u

theorem Verification.joeSecond_continuousAt {p t : ℝ} (ht : 0 < t) : ContinuousAt (joeSecond p) t

theorem Verification.joePartial_deriv {θ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) : HasDerivAt (joePartial θ u) (joeDensityReal θ u v) v

theorem Verification.joeRealCDF_deriv {θ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) : HasDerivAt (fun (x : ℝ) => joeRealCDF θ x v) (joePartial θ u v) u

theorem Verification.joeDensity_measurable (θ : ℝ) : Measurable (joeDensity θ)

theorem Verification.joeDensityReal_nonneg {θ : ℝ} (hθ : 1 ≤ θ) (u v : ℝ) : 0 ≤ joeDensityReal θ u v

theorem Verification.joeDensityReal_continuousAt {θ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) : ContinuousAt (Function.uncurry (joeDensityReal θ)) (u, v)

theorem Verification.joePartial_continuousAt {θ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) : ContinuousAt (fun (x : ℝ) => joePartial θ x v) u

theorem Verification.joe_toMeasure_density {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.joe θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (joeDensity θ x)

theorem Verification.joeDensity_mtp2 {θ : ℝ} (hθ : 1 ≤ θ) : ProbabilityTheory.IsMTP2 (joeDensity θ)

theorem Verification.joe_hasMTP2Density {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.joe θ hθ).HasMTP2Density