← Mathematical handbook

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

Equations

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

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

Equations

• Verification.n13Weight θ u = θ * (1 - Real.log u) ^ θ / (1 - Real.log u) / u

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

Equations

• Verification.n13Density θ x = Verification.n13Second θ⁻¹ (Verification.n13Inv θ ↑(x 0) + Verification.n13Inv θ ↑(x 1)) * Verification.n13Weight θ ↑(x 0) * Verification.n13Weight θ ↑(x 1)

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

Equations

• Verification.n13Partial θ u v = -Verification.n13PsiDeriv θ⁻¹ (Verification.n13Inv θ u + Verification.n13Inv θ v) * Verification.n13Weight θ u

theorem Verification.n13Density_measurable (θ : ℝ) : Measurable (n13Density θ)

theorem Verification.n13Inv_nonneg {θ : ℝ} (hθ : 0 ≤ θ) (u : ↑unitInterval) : 0 ≤ n13Inv θ ↑u

theorem Verification.n13Weight_nonneg {θ : ℝ} (hθ : 0 ≤ θ) (u : ↑unitInterval) : 0 ≤ n13Weight θ ↑u

theorem Verification.n13Density_nonneg {θ : ℝ} (hθ : 1 ≤ θ) (x : Fin 2 → ↑unitInterval) : 0 ≤ n13Density θ x

theorem Verification.n13Density_mtp2 {θ : ℝ} (hθ : 1 ≤ θ) : ProbabilityTheory.IsMTP2 (n13Density θ)

theorem Verification.n13Inv_deriv {θ u : ℝ} (hu : 0 < u) (ha : 0 < 1 - Real.log u) : HasDerivAt (n13Inv θ) (-n13Weight θ u) u

theorem Verification.n13Partial_deriv {θ u v : ℝ} (hv : 0 < v) (ha : 0 < 1 - Real.log v) (hs : 0 < 1 + (n13Inv θ u + n13Inv θ v)) : HasDerivAt (n13Partial θ u) (n13Second θ⁻¹ (n13Inv θ u + n13Inv θ v) * n13Weight θ u * n13Weight θ v) v

theorem Verification.n13CDF_deriv {θ u v : ℝ} (hu : 0 < u) (ha : 0 < 1 - Real.log u) (hs : 0 < 1 + (n13Inv θ u + n13Inv θ v)) : HasDerivAt (fun (x : ℝ) => n13Psi θ⁻¹ (n13Inv θ x + n13Inv θ v)) (n13Partial θ u v) u