Documentation

Verification.Nelsen17Density

← Mathematical handbook

noncomputable def Verification.n17DensityInv (a u : ℝ) :

Equations

Verification.n17DensityInv a u = -Real.log (Verification.n17Ratio a u)

Instances For

noncomputable def Verification.n17Weight (a u : ℝ) :

Equations

Verification.n17Weight a u = a * (1 + u) ^ (a - 1) / ((1 + u) ^ a - 1)

Instances For

noncomputable def Verification.n17DensityReal (a u v : ℝ) :

Equations

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

Instances For

noncomputable def Verification.n17Density (a : ℝ) (x : Fin 2 → ↑unitInterval) :

Equations

Verification.n17Density a x = Verification.n17DensityReal a ↑(x 0) ↑(x 1)

Instances For

noncomputable def Verification.n17Partial (a u v : ℝ) :

Equations

Verification.n17Partial a u v = -Verification.n17PsiDeriv a (Verification.n17DensityInv a u + Verification.n17DensityInv a v) * Verification.n17Weight a u

Instances For

noncomputable def Verification.n17GeneratorCDF (a u v : ℝ) :

Equations

Verification.n17GeneratorCDF a u v = Verification.n17Psi a (Verification.n17DensityInv a u + Verification.n17DensityInv a v)

Instances For

theorem Verification.n17DensityInv_pos {a u : ℝ} (ha : a ≠ 0) (hu : u ∈ Set.Ioo 0 1) :

0 < n17DensityInv a u

theorem Verification.n17Weight_nonneg {a u : ℝ} (ha : a ≠ 0) (hu : 0 < u) :

0 ≤ n17Weight a u

theorem Verification.n17DensityInv_deriv {a u : ℝ} (ha : a ≠ 0) (hu : u ∈ Set.Ioo 0 1) :

HasDerivAt (n17DensityInv a) (-n17Weight a u) u

theorem Verification.n17Weight_continuousAt {a u : ℝ} (ha : a ≠ 0) (hu : u ∈ Set.Ioo 0 1) :

ContinuousAt (n17Weight a) u

theorem Verification.n17Second_continuousAt {a t : ℝ} (ht : 0 ≤ t) :

ContinuousAt (n17Second a) t

theorem Verification.n17Partial_deriv {a u v : ℝ} (ha : a ≠ 0) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) :

HasDerivAt (n17Partial a u) (n17DensityReal a u v) v

theorem Verification.n17GeneratorCDF_deriv {a u v : ℝ} (ha : a ≠ 0) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) :

HasDerivAt (fun (x : ℝ) => n17GeneratorCDF a x v) (n17Partial a u v) u

theorem Verification.n17Density_measurable (a : ℝ) :

Measurable (n17Density a)

theorem Verification.n17DensityReal_nonneg {a : ℝ} (ha : a ≠ 0) (u v : ℝ) :

0 ≤ n17DensityReal a u v

theorem Verification.n17DensityReal_continuousAt {a u v : ℝ} (ha : a ≠ 0) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) :

ContinuousAt (Function.uncurry (n17DensityReal a)) (u, v)

theorem Verification.n17Partial_continuousAt {a u v : ℝ} (ha : a ≠ 0) (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) :

ContinuousAt (fun (x : ℝ) => n17Partial a x v) u

theorem Verification.n17_toMeasure_density {a : ℝ} (ha : a ≠ 0) :

(nelsen17 (-a) ⋯).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (n17Density a x)

theorem Verification.n17Density_mtp2 {α : ℝ} (ha : α ≠ 0) (ha1 : α ≤ 1) :

ProbabilityTheory.IsMTP2 (n17Density α)

theorem Verification.n17_hasMTP2Density {a : ℝ} (ha : a ≠ 0) (ha1 : a ≤ 1) :

(nelsen17 (-a) ⋯).HasMTP2Density

theorem Verification.nelsen17_density_tp2 (θ : ℝ) (hθ : θ ≠ 0) (hθ1 : -1 ≤ θ) :

(nelsen17 θ hθ).HasMTP2Density

theorem Verification.nelsen17_density_tp2_iff (θ : ℝ) (hθ : θ ≠ 0) :

(nelsen17 θ hθ).HasMTP2Density ↔ -1 ≤ θ