← Mathematical handbook

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

Equations

• Verification.n19Inv θ u = Real.exp (θ / u) - Real.exp θ

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

Equations

• Verification.n19Weight θ u = θ * Real.exp (θ / u) / u ^ 2

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

Equations

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

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

Equations

• Verification.n19Density θ x = Verification.n19DensityReal θ ↑(x 0) ↑(x 1)

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

Equations

• Verification.n19Partial θ u v = -Verification.n19PsiDeriv θ (Verification.n19Inv θ u + Verification.n19Inv θ v) * Verification.n19Weight θ u

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

Equations

• Verification.n19RealCDF θ u v = Verification.n19Psi θ (Verification.n19Inv θ u + Verification.n19Inv θ v)

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

theorem Verification.n19Weight_nonneg {θ u : ℝ} (hθ : 0 < θ) : 0 ≤ n19Weight θ u

theorem Verification.n19Inv_deriv {θ u : ℝ} (hu : u ∈ Set.Ioo 0 1) : HasDerivAt (n19Inv θ) (-n19Weight θ u) u

theorem Verification.n19Weight_continuousAt {θ u : ℝ} (hu : u ∈ Set.Ioo 0 1) : ContinuousAt (n19Weight θ) u

theorem Verification.n19Second_continuousAt {θ t : ℝ} (hθ : 0 < θ) (ht : 0 ≤ t) : ContinuousAt (n19Second θ) t

theorem Verification.n19Partial_deriv {θ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) : HasDerivAt (n19Partial θ u) (n19DensityReal θ u v) v

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

theorem Verification.n19Density_measurable (θ : ℝ) : Measurable (n19Density θ)

theorem Verification.n19DensityReal_nonneg {θ : ℝ} (hθ : 0 < θ) (u v : ℝ) : 0 ≤ n19DensityReal θ u v

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

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

theorem Verification.n19_toMeasure_density {θ : ℝ} (hθ : 0 < θ) : (nelsen19 θ ⋯).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (n19Density θ x)

theorem Verification.n19Density_mtp2 {θ : ℝ} (hθ : 0 < θ) : ProbabilityTheory.IsMTP2 (n19Density θ)

theorem Verification.n19_hasMTP2Density {θ : ℝ} (hθ : 0 < θ) : (nelsen19 θ ⋯).HasMTP2Density

theorem Verification.nelsen19_density_tp2 (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen19 θ hθ).HasMTP2Density