← Mathematical handbook

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

Equations

• Verification.n16Inv θ u = (1 - u) * (1 + θ / u)

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

Equations

• Verification.n16Weight θ u = 1 + θ / u ^ 2

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

Equations

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

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

Equations

• Verification.n16Density θ x = Verification.n16DensityReal θ ↑(x 0) ↑(x 1)

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

Equations

• Verification.n16Partial θ u v = -Verification.n16PsiDeriv θ (Verification.n16Inv θ u + Verification.n16Inv θ v) * Verification.n16Weight θ u

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

Equations

• Verification.n16RealCDF θ u v = Verification.n16Psi θ (Verification.n16Inv θ u + Verification.n16Inv θ v)

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

theorem Verification.n16Weight_pos {θ u : ℝ} (hθ : 0 < θ) : 0 < n16Weight θ u

theorem Verification.n16Inv_deriv {θ u : ℝ} (hu : u ∈ Set.Ioo 0 1) : HasDerivAt (n16Inv θ) (-n16Weight θ u) u

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

theorem Verification.n16Second_continuousAt {θ t : ℝ} (hθ : 0 < θ) : ContinuousAt (n16Second θ) t

theorem Verification.n16Partial_deriv {θ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) : HasDerivAt (n16Partial θ u) (n16DensityReal θ u v) v

theorem Verification.n16RealCDF_deriv {θ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) (_hv : v ∈ Set.Ioo 0 1) : HasDerivAt (fun (x : ℝ) => n16RealCDF θ x v) (n16Partial θ u v) u

theorem Verification.n16Density_measurable (θ : ℝ) : Measurable (n16Density θ)

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

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

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

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

theorem Verification.n16Density_mtp2 {θ : ℝ} (hθ : 3 + 2 * √2 ≤ θ) : ProbabilityTheory.IsMTP2 (n16Density θ)

theorem Verification.n16_hasMTP2Density {θ : ℝ} (hθ : 3 + 2 * √2 ≤ θ) : (nelsen16 θ ⋯).HasMTP2Density