← Mathematical handbook

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

Equations

• Verification.n20Inv θ u = Real.exp (u ^ (-θ)) - Real.exp 1

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

Equations

• Verification.n20Weight θ u = θ * Real.exp (u ^ (-θ)) * u ^ (-θ - 1)

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

Equations

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

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

Equations

• Verification.n20Density θ x = Verification.n20DensityReal θ ↑(x 0) ↑(x 1)

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

Equations

• Verification.n20Partial θ u v = -Verification.n20PsiDeriv θ⁻¹ (Verification.n20Inv θ u + Verification.n20Inv θ v) * Verification.n20Weight θ u

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

Equations

• Verification.n20RealCDF θ u v = Verification.n20Psi θ⁻¹ (Verification.n20Inv θ u + Verification.n20Inv θ v)

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

theorem Verification.n20Weight_nonneg {θ u : ℝ} (hθ : 0 < θ) (hu : 0 ≤ u) : 0 ≤ n20Weight θ u

theorem Verification.n20Inv_deriv {θ u : ℝ} (hu : u ∈ Set.Ioo 0 1) : HasDerivAt (n20Inv θ) (-n20Weight θ u) u

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

theorem Verification.n20Second_continuousAt {θ t : ℝ} (_hθ : 0 < θ) (ht : 0 ≤ t) : ContinuousAt (n20Second θ⁻¹) t

theorem Verification.n20Partial_deriv {θ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) : HasDerivAt (n20Partial θ u) (n20DensityReal θ u v) v

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

theorem Verification.n20Density_measurable (θ : ℝ) : Measurable (n20Density θ)

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

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

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

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

theorem Verification.n20Density_mtp2 {θ : ℝ} (hθ : 0 < θ) : ProbabilityTheory.IsMTP2 (n20Density θ)

theorem Verification.n20_hasMTP2Density {θ : ℝ} (hθ : 0 < θ) : (nelsen20 θ ⋯).HasMTP2Density

theorem Verification.nelsen20_density_tp2 (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen20 θ hθ).HasMTP2Density